SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
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 invalid...