Safe Speculation for Cheri

We present an architectural Capability Speculation Contract (CSC) for CHERI implementations, test for violations in the CHERI-Toooba microarchitecture, and develop and evaluate a conforming implementation. The CHERI capability instruction-set extension promises proven architectural guarantees for memory safety and pointer provenance. However, superscalar and out-of-order CHERI implementations will need to contend with microarchitectural transient-execution side-channel attacks. To ensure the safety of all CHERI implementations, we articulate CSC: a universal architectural speculation contract for the CHERI architecture that maintains key capability invariants in speculation. We then develop tests against sub-classes of CSC, and discover violations in CHERI-Toooba that lead to a new class of transient-execution attacks, Meltdown-CF (Capability Forgery) for which we develop a user-mode exploit that allows reads of secret data. We then develop strategies to fully enforce CSC in CHERI-Toooba. We find that simplistic, strong enforcement in-curs a low performance overhead of only 3.43% in SPECint2006 benchmarks, with promise for more optimal designs in the future. Our architectural recommendations to mitigate Meltdown-CF have been accepted by the upstream CHERI architecture and are included in current CHERI-RISC-V drafts for ratification.

Keywords

33 Built Environment and Design

Journal Title

2024 IEEE 42nd International Conference on Computer Design (ICCD)

Conference Name

2024 IEEE 42nd International Conference on Computer Design (ICCD)

Journal ISSN

1063-6404

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Publisher DOI

https://doi.org/10.1109/iccd63220.2024.00063

Rights and licensing

Except where otherwised noted, this item's license is described as Attribution 4.0 International

Sponsorship

EPSRC (via Queen's University Of Belfast) (R1098ECI)

This project was supported by the NCSC under the UK RISE Initiative. This work was supported in part by the Engineering and Physical Sciences Research Council EP/S030867/1. The authors gratefully acknowledge support from Arm Limited. This work was sponsored by the Air Force Research Laboratory (AFRL) and by the Defense Advanced Research Projects Agency (DARPA) under Contracts No. FA8750-24-C-B047 (``DEC''), HR0011-18-C-0016 (``ECATS''), and HR0011-22-C-0110 (``ETC''). Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL) or the Defense Advanced Research Projects Agency (DARPA). Distribution Statement A: Approved for public release: distribution is unlimited. For the purpose of open access, the author(s) has applied a Creative Commons Attribution (CC BY) license to any Accepted Manuscript version arising.

Collections

University of Cambridge Research Outputs (Articles and Conferences)