Efficient, Provable Local Capability Revocation using Uninitialized Capabilities
summary
Proposes uninitialized capabilities that give write-only access to an uninitialized stack region and require overwriting before any read, implemented with three new instructions loadu/storeu/promoteu. Proves a universal capability-safety contract using a step-indexed logical relation mechanized in Iris, and uses that to verify a new, faster calling convention (assembly implementation ~300 lines vs ~400 with full stack clearing) and a proof-of-concept CHERI/Morello implementation.
AI-written summary · about
chapters (20)
- 0:00Introduction: Capability Machines
- 0:47Introduction: Local Capabilities
- 1:03Introduction: The Challenge
- 2:21Contributions
- 3:22Overview
- 4:26Machine Capabilities
- 5:49A Simple Scenario: Revisited
- 7:32The Lattice of Permission
- 8:03A Simple Scenario: Now with a Stack
- 9:39Uninitialized Capabilities
- 10:24The Extended Lattice of Permissions
- 11:00Operations
- 13:22An Efficient Calling Convention
- 15:45Approach
- 17:02A Capability Machine Language
- 19:23The Logical Relation
- 21:40The World in Iris
- 24:44The Fundamental Theorem of Logical Relations
- 25:55The Awkward Example
- 28:38Conclusion
related talks
17mProving capability safety in the presence of indirect sentries
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr...
27mLe Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in P...
36mObject Capabilities
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)