Memory simulations, security and optimization in a verified compiler
summary
CompCert receives three new, machine-checked transformations: implemented and proved stack canaries and pointer authentication as security inserts, and a tail-call elimination that replaces recursive calls with a loop. Proofs use the compiler’s proof assistant framework and simulation lemmas over a memory model; correctness for canaries and tail-call conversion follows by memory injections and extensions. Pointer authentication works when applied late (it currently does not commute with injections) and the proofs succeed.
AI-written summary · about
chapters (9)
- 0:00Verified compiler ComCERT
- 1:57Formal compiler verification
- 3:00Correctness theorem and traces
- 6:32Memory model and state
- 9:23Undefined behavior and transforms
- 13:46Security countermeasures
- 17:57Stack canaries verification
- 19:21Tail call elimination
- 21:26Conclusion and future
related talks
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
15mMy Journey in Secure Compilation
26mSecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn
23mCorrect Compilation of Concurrent C Code
19mFormally Verifying Optimizations with Block Simulations
34mFormally verified hardening of C programs against hardware fault injection
29mA CompCert backend with symbolic encryption
21mWeak Memory Demands Model-based Compiler Testing