Good programming languages provide helpful abstractions for writing more secure code: from structured control flow, procedures, and modules, to types, interfaces, and specifications. However, such abstractions are not enforced when compiling a program and linking it with low-level code (such as a library or a legacy application), which can be buggy, vulnerable, compromised, or even malicious, and which can void all security guarantees of the compiled code. To make things worse, most realistic programming languages have unsafe features that can lead to “undefined behavior”, which causes compilers to produce code that can behave completely arbitrarily. Such undefined behavior is endemic in languages like C, where buffer overflows, use after frees, double frees, invalid type casts, various concurrency bugs, etc., lead to devastating security vulnerabilities that are often remotely exploitable.

We study how compartmentalization can mitigate these two secure compilation problems: (1) by protecting secure source programs from linked adversarial low-level code and (2) for vulnerable source programs by restricting the scope of undefined behavior both spatially to just the compartments that encounter undefined behavior, and temporally by still providing protection to each compartment up to the point in time when it encounters undefined behavior.

In particular, this talk will report on our journey that recently resulted in SECOMP, a compiler for compartmentalized C code that comes with machine-checked secure compilation proofs restricting the scope of undefined behavior. It will focus on the main challenges our research has overcome: (A) defining formally what it means for a compilation chain to be secure in the two settings above, which led to the discovery of a wide range of secure compilation criteria that provide good alternatives to full abstraction; (B) enforcing water-tight protection using low-level compartmentalization mechanisms such as software fault isolation, programmable tagged architectures, and capability machines; and (C) devising scalable proof techniques and using them to provide the first machine-checked secure compilation guarantees similar to full abstraction for a realistic programming language.

Cătălin Hrițcu is a tenured faculty member and head of the Formally Verified Security group at the Max Planck Institute for Security and Privacy (MPI-SP) in Bochum, Germany. He is particularly interested in formal methods for security (secure compilation, compartmentalization, memory safety, security protocols, information flow), programming languages (program verification, proof assistants, dependent types, formal semantics, mechanized metatheory, property-based testing), and the design and verification of security-critical systems (reference monitors, secure compilation chains, tagged architectures). He was awarded an ERC Starting Grant on formally secure compilation, and is also involved in the design of the F* verification system. Catalin received a PhD from Saarland University, a Habilitation from ENS Paris, and was previously also a Tenured Researcher at Inria Paris, a Postdoctoral Research Associate at University of Pennsylvania, and a Visiting Researcher at Microsoft Research Redmond.