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.
45