To attend the lecture, prior registration is requested. After the lecture, there will be a Get Together with pizza and drinks.
Catalin Hritcu is a tenured faculty at the Max-Planck-Institute for Security and Privacy (MPI-SP) where he leads the Formally Verified Security group. Catalin is also a member of the Horst-Görtz-Institute for IT Security and CASA PI. Since last year he is also an Adjunct Professor (APL) in the RUB Faculty of Computer Science.
He is interested in formal methods for security (secure compilation, compartmentalization, memory safety, information flow), programming languages (program verification, proof assistants, dependent types, formal semantics, property-based testing), and the design and verification of security-critical systems (compilation chains, reference monitors, tagged architectures, high-assurance crypto).
He was awarded an ERC Starting Grant on formally secure compilation and was also involved in the design of the F* verification system. His research received Distinguished Paper Awards at the Computer Security Foundations (CSF) symposium in 2019 and 2021. Catalin serves as the Steering Committee Chair of the Certified Programs and Proofs (CPP) conference and founded the Principles of Secure Compilation (PriSC) workshop. He served as Track PC Chair for Formal Methods and Programming Languages of the Conference on Computer and Communications Security (CCS) in 2024, PC and Conference Chair of CPP 2020 and 2021, and General Chair of the European Symposium on Security and Privacy (EuroS&P) held in Paris in 2017. Before joining MPI-SP, Catalin was a Tenured Researcher at Inria Paris, a Visiting Researcher at Microsoft Research, and a PostDoc at University of Pennsylvania. He received a PhD from Saarland University and a Habilitation from ENS Paris.
Abstract:
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.
General note: In case of using gender-assigning attributes we include all those who consider themselves in this gender regardless of their own biological sex.