Secure speculation design improves software isolation with CHERI
SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
Cryptography and SecurityHardware Architecture
Summary
Speculative execution in modern processors can accidentally reveal secret information, even when software is designed to keep things secret. The authors show that securing speculation on CHERI, a special processor architecture that keeps software parts well-isolated, is difficult and past solutions did not fully protect secrets. They created a new method and processor design called SCHERI that formally guarantees secure speculation while maintaining these secrecy rules. This means software running on SCHERI can better protect secrets from attacks that exploit processor tricks.
What this means in practice
- •For processor architects: Design new processors that enforce secure speculation with formal guarantees against Spectre-like leaks in capability-based environments.
- •For security-focused operating system developers: Build OS components that rely on CHERI and SCHERI to maintain secret confidentiality despite speculative execution vulnerabilities.
Authors
Shixin Song, Davide Davoli, Elias Storme, Marton Bognar, Dominique Devriese, Frank Piessens, Tamara Rezk
Abstract
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.