Fully Composable and Adequate Verified Compilation with Direct Refinements betwe...
summary
Claims a Kripke Memory Relation (called NGP) that is transitive and absorbs per-pass rely/guarantee conditions so a single direct refinement relates Clight source states to assembly states without exposing intermediate semantics. Demonstrates vertical and horizontal composition, semantic adequacy, and protection of private memory on an example client/server with pointer passing and secret key 42 (return address and stack frames protected). Applies to the CompCert full chain and ships artifacts.
AI-written summary · about
chapters (8)
- 0:00Verified compilation intro
- 1:03Whole-program limits
- 2:51Vertical refinement challenges
- 5:40Refinement guarantees
- 7:44Transitive memory protection
- 13:02Conert’s implementation
- 13:43Key insights
- 14:28Future work
related talks
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
17mA Formally Verified Foundation for Compositional Heterogeneous Coherence
25mComposing Secure Compilers
28mMemory simulations, security and optimization in a verified compiler
17mDenotation-based Compositional Compiler Verification
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
15mMy Journey in Secure Compilation
17mOvercoming Restraint: Composing Verification of Foreign Functions with Cogent