Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
summary
Proves that an encapsulated C-style component running on Arm Morello maintains a mod-64 accumulator invariant against arbitrary untrusted code, by mechanising a full-scale Morello ISA model and a logical relation. Combines Cerise-style Iris reasoning for known code, Allaris symbolic-simplification for concrete proofs, and T‑CHERI properties ported from Isabelle into a 100,000+ line Rock model (hand-translated assumptions). Delivers a mechanised fundamental theorem and a verified accumulator example; artifacts are reusable.
AI-written summary · about
chapters (12)
- 0:00Morello-Cerise introduction
- 1:02Cherry capabilities
- 2:46Encapsulation with Cherry
- 5:57Sealed capabilities demo
- 7:04Proving encapsulation
- 8:49Scaling to Morello
- 11:17Terry and Allaris tools
- 12:44Logical relation for unknown code
- 15:55Proof structure challenges
- 16:39Conclusion and future work
- 18:02Q&A: Code re-entry
- 19:47Q&A: Trace properties
related talks
16mCerisier: A Program Logic for Attestation in a Capability Machine
17mProving capability safety in the presence of indirect sentries
12mLibrary-based Compartmentalisation on CHERI
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)
01h 05mKeynote: Can we reason about the security of concurrent systems code?
16mMitigating Transient-Execution Attacks with CHERI Compartments
24mSecure Calling Conventions for CHERI Capability Machines in Practice (Work in P...