Undefined behavior is endemic in the C programming language: buffer overflows, use after frees, double frees, invalid type casts, various concurrency bugs, etc, cause mainstream C compilers to produce code that can behave completely arbitrarily. This leads to devastating security vulnerabilities that are often remotely exploitable, and both Microsoft and Chrome report that around 70% of their high severity security bugs are caused by memory safety issues.

We study how compartmentalization can mitigate this problem by restricting the scope of undefined behavior both (a) spatially to just the compartments that encounter undefined behavior, and (b) temporally by still providing protection to each compartment up to the point in time when it encounters undefined behavior. While our past work has focused on formally secure compilation of compartmentalized code for toy languages with buffers and procedures, in this talk we report on our ongoing work on scaling up these ideas to a realistic C compiler, based on CompCert. While in prior work we used SFI or a tagged architecture to enforce compartmentalization at the lowest level, in this talk we will focus on a new secure compilation backend targeting a variant of the CHERI capability machine.

When completed, our work will show that compartmentalized code in a mainstream programming language can be compiled by a realistic compiler with machine-checked security guarantees. This will be a milestone for secure compilation. Proving secure compilation even for toy compilers can be a daunting task, with careful paper proofs often spanning hundreds of pages. We believe that scaling such proofs to realistic compilers has to rely on proof assistants like Coq for ensuring that the proofs are correct, even if building such machine-checked proofs requires serious proof-engineering work. The good news is that proof assistants do not only check proofs, but also allow proofs to be built interactively, refactored, simplified, maintained, and evolved together with the compilation chain.