SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
[Kryptografia i bezpieczeństwo] Autorzy: Shixin Song, Davide Davoli, Elias Storme i 4 więcej
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 polic…
- Kategoria arxiv
- cs.CR
- Kategoria
- Kryptografia i bezpieczeństwo