SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
Researchers formally prove existing CHERI speculation proposals leak secrets and present SCHERI, a processor design with end-to-end Spectre-resistant constant-time guarantees.
The paper builds a formal framework reasoning jointly about capability safety, speculative execution, and information-flow security on CHERI architectures. It demonstrates that existing secure-speculation proposals fail to preserve constant-time confidentiality guarantees and can transiently leak isolated secrets. The authors present SCHERI, a new processor design formally proven to provide end-to-end secure speculation for the constant-time policy, resilient to Spectre attacks.
- Formal framework unifies capability safety, speculation, and information-flow security
- Existing CHERI speculation proposals shown to transiently leak secrets
- SCHERI provably guarantees secure speculation under constant-time policy
- Provides design guidance for future Spectre-resilient capability processors
Full article141 words · extracted from arxiv.org · click to collapse
Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leakage, software can be written in a constant-time fashion. Modern processors, however, rely heavily on speculative execution, which can invalidate the constant-time guarantees and leak isolated secrets transiently. In this work, we show that providing secure speculation for CHERI is non-trivial, and that existing proposals fail to preserve the confidentiality guarantees. We develop a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security, and use it to demonstrate potential leaks. We then present SCHERI, a new processor design within this framework, and formally prove that it provides end-to-end secure speculation guarantees for the constant-time policy. Our results provide formal foundations and practical guidance for building future capability-based processors, which are resilient to Spectre attacks for constant-time programs.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.17399