Morello Cerise: proving secure encapsulation (work in progress)
summary
Formal encapsulation for Morello is approached by combining T-Cherry properties (Isabelle-proven whole-architecture bounds on capability behavior) with the Lis simplifier and an Iris-style program logic for known code, and proofs encoded in Coq translation of the T statements. The team adapts the full Morello semantics (100k+ lines after conversion) to handle tagged capabilities and compression, builds a verification pipeline that switches between reasoning about unknown adversary code and simplified known code, and partially verifies a monotonic accumulator example; full proof completion remains work in progress.
AI-written summary · about
chapters (7)
- 0:00Morello Cerise project
- 1:09Ser program logic
- 2:32Adapting Ser to Morello
- 4:16T Cherry properties
- 6:02L and T Cherry proof
- 7:47Progress and remaining work
- 8:57Q&A
related talks
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
15mIncremental Certified Programming
01h 05mVerifying Infinitely Many Programs at Once
18mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C
21mMechanised Hypersafety Proofs about Structured Data