Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed
summary
Introduces directed capabilities that add one extra bit and a single arithmetic bounds check to CHERI-style machines, enabling a calling convention that requires no memory clearing and statically forbids dangling stack pointers. Provides a unary logical relation for integrity and a binary logical relation for temporal confidentiality, proves full abstraction of an overlay semantics to the base machine, and mechanizes all results in Coq (Iris), showing the convention is sound and implementable with low overhead.
AI-written summary · about
chapters (14)
- 0:00Capability machines intro
- 2:10Attacker model and memory safety
- 3:13Cherry capability machines
- 4:36Temporal stack safety
- 6:45Secure stack conventions
- 8:50Stack safety approaches
- 10:16Directed capabilities
- 13:04Key idea behind directed
- 14:10Operational semantics
- 16:39Uninitialized capabilities
- 18:07Returning with directed
- 19:31Hardware feasibility
- 20:53Formalization with Iris
- 21:54Conclusion and future
related talks
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr...
17mProving capability safety in the presence of indirect sentries
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in P...
29mEfficient, Provable Local Capability Revocation using Uninitialized Capabilities
16mCerisier: A Program Logic for Attestation in a Capability Machine
27mA CHERI C Memory Model for Verified Temporal Safety
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
10mCHERI in out-of-order microarchitectures