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.
Authors
- Jonathan Woodruff (ORCID: https://orcid.org/0000-0003-3971-2681)
- Robert N. M. Watson (ORCID: https://orcid.org/0000-0001-8139-8783)
- Peter G. Neumann (ORCID: https://orcid.org/0009-0008-1197-8000)
- Jessica Clarke (ORCID: https://orcid.org/0000-0001-8157-5567)
- Peter Rugg (ORCID: https://orcid.org/0009-0000-2976-0474)
- Alexandre Joannou (ORCID: https://orcid.org/0000-0002-3161-2638)
- Simon W. Moore (ORCID: https://orcid.org/0000-0002-2806-495X)
- Brooks Davis (ORCID: https://orcid.org/0009-0006-6256-0419)
- Franz A. Fuchs (ORCID: https://orcid.org/0000-0002-1402-7138)
- John Baldwin
Institutions
- SRI International (US)
- University of Cambridge (GB)
- Menlo School (US)
- Ashland (United States) (US)
Publication Details
- Published
- 2024-11-18
- DOI
- https://doi.org/10.1109/iccd63220.2024.00063
- Citations
- 3
- Primary Topic
- History of Science and Medicine
- Type
- article
- Field-Weighted Citation Impact
- 18.13
Funders
- Defense Advanced Research Projects Agency
- Engineering and Physical Sciences Research Council
- Air Force Research Laboratory