CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
summary
CompCertELF is a Coq-verified C-to-ELF toolchain that adds a verified assembler and supports verified separate compilation by proving commutativity between source linking and ELF linking using syntactic equivalences =_p and =_r. It extends Stack-Aware CompCert with RealAsm → relocatable programs, heavy proofs around symbol table generation and memory injection, about 23,000 lines of Coq added. Generated ELF executables run about 8.4% slower and are ~74% larger on average, currently covering a subset of 32-bit x86 and limited ELF features.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:25Motivation: Verified C Compilers Generating Object Files • Production C compilers generate object files (e.g. ELF files)
- 1:22Motivation: Verified Separate Compilation to Object Files
- 3:45Background: (Stack-Aware) CompCert
- 4:32CompCertELF: An Overview • Extends Stack-Aware CompCert with a verified assembler
- 6:06A Running Example
- 7:06Symbol Table Generation: An Example
- 7:58Symbol Table Generation: The Verification
- 10:30Problem: Linking of sets v.s. Linking of sections counter
- 11:41Overview of Commutativity for CompCertELF
- 12:27Restore Commutativity for Symbol Table Generation
- 13:37Transition from ep to . counter
- 14:53Limitations
- 15:30Evaluation: Specifications and Proofs
- 15:55Evaluation: Performance
- 16:18Evaluation: File Sizes
- 16:29Conclusion
related talks
15mMy Journey in Secure Compilation
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
28mMemory simulations, security and optimization in a verified compiler
19mMELF: Multivariant Executables for a Heterogeneous World
24m(Ab)using Compiler Tools
29mA CompCert backend with symbolic encryption
58mFast Cryptographic Code via Partial Evaluation