SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI

Developed a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security; presented SCHERI, a new processor design within this framework; and formally proved that SCHERI provides end-to-end secure speculation guarantees under the constant-time policy.