Implementing a Capability Machine Model into Iris
summary
Mechanization of a core capability-machine model into Iris, with an embedding of a machine language and a mechanized logical relation that solves the world circularity using Iris invariants plus a collection of state-transition systems (Sigma) that track temporary vs permanent memory. The development models local vs global capabilities and the calling convention that revokes temporaries from the stack, proves the fundamental theorem and capability-safety proofs, produces about 25k LOC, and removes explicit step-indexing so there is no step-index in final definition.
AI-written summary · about
chapters (5)
related talks
17mProving capability safety in the presence of indirect sentries
25mCapabilities, Effects, Ownership, and Behaviors
29mEfficient, Provable Local Capability Revocation using Uninitialized Capabilities
21mIris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…)
16mCerisier: A Program Logic for Attestation in a Capability Machine
27mLe Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed
36mObject Capabilities
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)