My Journey in Secure Compilation

on YouTube ↗15m

" summary

Provides a machine-checked compiler pipeline that enforces compartmentalization and limits undefined behavior to compromised compartments, implemented as SECOMP—an extension of CompCert that preserves 19 verified passes and disables only cross-compartment inlining/tail-call optimizations. Proof effort adds about 19,000 lines (a 13.6% change to CompCert) and reuses ~130,000 lines of Coq; back ends target RISC-V and a CHERI capability backend, with enforcement options including SFI, micropolicies, and capability machines, and yields full-abstraction–like secure compilation guarantees.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 0:23Security in compilation
3. 1:48Source versus target execution
4. 3:15Source semantics compromise
5. 5:49Enforcement and proof strategies
6. 6:30ComCERT extension
7. 7:54CHERI hardware acceleration
8. 8:59Compiler correctness proof
9. 10:42Secure compilation challenges
10. 12:51Backend verification
11. 13:32Q&A

" related talks

• 28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...Aina Linn Georges, Cătălin Hriţcu, Arthur Azevedo de Amorim, Andrew Tolmach, Jérémy Thibault, Roberto Blanco · PriSC 2023
• 50mCompCert: a journey through the landscape of mechanized semantics for verified co...Sandrine Blazy · CPP 2023
• 29mA CompCert backend with symbolic encryptionpaulo torrini, sylvain bulmay · PriSC 2022
• 28mMemory simulations, security and optimization in a verified compilerDavid Monniaux · CPP 2024
• 16mMitigating Transient-Execution Attacks with CHERI CompartmentsFranz Fuchs · RISC-V Summit Europe 2023
• 24mA CompCert Compiler that Preserves Cryptographic Constant-timeRemi Hutin · PriSC 2020
• 25mComposing Secure CompilersMarco Patrignani, arthur amoren, mattis uh cruz, mata skruzzle · PriSC 2022
• 16mReconciling Optimization With Secure CompilationAlbert Cohen, Arnaud de Grandmaison, Karine Heydemann, Son Tuan Vu, Christophe Guillon · OOPSLA 2021