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

Institutions

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

Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Safe Speculation for CHERI

Jonathan Woodruff, Robert N. M. Watson, Peter G. Neumann, Jessica Clarke et al.
3 citations
History of Science and Medicine
18.13
article

Safe Speculation for CHERI

Jonathan Woodruff, Robert N. M. Watson, Peter G. Neumann, Jessica Clarke, Peter Rugg, Alexandre Joannou, Simon W. Moore, Brooks Davis, Franz A. Fuchs, John Baldwin
article en
3 citations

Abstract

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.

SRI International (US), University of Cambridge (GB), Menlo School (US), Ashland (United States) (US)
Defense Advanced Research Projects Agency, Engineering and Physical Sciences Research Council, Air Force Research Laboratory
Openalex Percentile: Top 1%
History of Science and Medicine
18.13
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.