Proving capability safety in the presence of indirect sentries
summary
Extends a CHERI-style miniature machine (SeRiES) with indirect sentries, adapts an Iris-like program logic plus a new logical relation, and produces machine-checked proofs that capability safety still holds when entry capabilities load two worlds. Builds a heap-based calling convention that needs no trampoline code and proves robust local-state encapsulation: a sub-buffer example keeps the private half unchanged despite adversary access, showing the construction actually enforces the claimed guarantees.
AI-written summary · about
chapters (9)
- 0:00Capability safety basics
- 2:35Indirect vs sealed pairs and sentries
- 4:22Indirect sentries mechanics
- 6:51Formal reasoning framework
- 9:17Unknown code execution logic
- 10:23Secure calling convention design
- 12:10Local state encapsulation
- 13:13Summary and future work
- 13:53Q&A
related talks
16mCerisier: A Program Logic for Attestation in a Capability Machine
27mLe Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed
29mEfficient, Provable Local Capability Revocation using Uninitialized Capabilities
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in P...
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
24mImplementing a Capability Machine Model into Iris