SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
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.
|PriSC'23 slides (prisc2023-slides.pdf)||3.69MiB|
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30
|Blame-Preserving Secure Compilation|
Marco Patrignani University of Trento, Matthis Kruse CISPA Helmholtz Center for Information SecurityPre-print
|Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed InterfacesRecorded|
PriSCPre-print File Attached
|SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine|
Jérémy Thibault MPI-SP, Arthur Azevedo de Amorim Boston University, Roberto Blanco MPI-SP, Aina Linn Georges Aarhus University, Cătălin Hriţcu MPI-SP, Andrew Tolmach Portland State UniversityPre-print Media Attached File Attached