Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
summary
This work extends recomposition with blame-aware recomposition and an overlay semantics that treats cross-compartment observations (like code-size or allocation-pattern probes) as undefined behavior, allowing low-level contexts to see code yet still replay traces. It targets a programmable tagged-architecture backend, adds a custom compartmentalized allocator to hide layout, and proves a three-way simulation / main recomposition lemma. Implementation is mostly working; large-vector proof obligations and some performance tuning remain.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:22Memory safety and compartmentalization
- 2:28Formal verification of secure backends
- 4:58Limitations of recomposition proofs
- 8:27Recomposition fails at low-level
- 10:14Blame-aware recomposition
- 13:28Lightweight protections
- 14:33Application to micro-p backend
- 15:13Conclusion
related talks
31mBlame-Preserving Secure Compilation
20mFully Composable and Adequate Verified Compilation with Direct Refinements betwe...
08mShort Talk: Generalising secure compilation criteria
15mMy Journey in Secure Compilation
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
25mComposing Secure Compilers
27mUniversally Composable Security for Program Partitioning
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations