Um an der Vorlesung teilnehmen zu können, wird um eine vorherige Anmeldung gebeten. Nach der Vorlesung wird es ein Get Together mit Pizza und Getränken geben.
Catalin Hritcu ist Tenured Faculty am Max-Planck-Institut für Sicherheit und Privatsphäre, wo er die Gruppe für formale Sicherheitsverifizierung leitet. Zudem ist Hritcu Mitglied des Horst-Görtz-Institutes für IT-Sicherheit und CASA PI. Außerdem ist er seit Mai 2024 auch APL Professor an der Fakultät für Informatik.
Er interessiert sich für formale Methoden für die Sicherheit (z.B. sichere Kompilierung, Kompartimentierung, Speichersicherheit, Informationsfluss), Programmiersprachen (z.B. Programmverifikation, Beweisassistenten, abhängige Typen, formale Semantik, eigenschaftsbasiertes Testen) und den Entwurf und die Verifikation von sicherheitskritischen Systemen (z.B. Kompilierungsketten, Referenzmonitore, getaggte Architekturen, hochsichere Krypto).
Hritcu wurde mit einem ERC Starting Grant für formal sichere Kompilierung ausgezeichnet und war auch an der Entwicklung des F*-Verifikationssystems beteiligt. Seine Forschung wurde auf dem Symposium Computer Security Foundations (CSF) in den Jahren 2019 und 2021 mit dem Distinguished Paper Award ausgezeichnet. Catalin ist Vorsitzender des Lenkungsausschusses der Konferenz Certified Programs and Proofs (CPP) und hat den Workshop Principles of Secure Compilation (PriSC) gegründet. Er war Track PC Chair für formale Methoden und Programmiersprachen der Conference on Computer and Communications Security (CCS) 2024, PC und Conference Chair der CPP 2020 und 2021 und General Chair des European Symposium on Security and Privacy (EuroS&P), das 2017 in Paris stattfand. Bevor er zum MPI-SP kam, war Hritcu Tenured Researcher bei Inria Paris, Visiting Researcher bei Microsoft Research und PostDoc an der University of Pennsylvania. Er hat an der Universität des Saarlandes promoviert und sich an der ENS Paris habilitiert.
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.
Allgemeiner Hinweis: Mit einer möglichen Nennung von geschlechtszuweisenden Attributen implizieren wir alle, die sich diesem Geschlecht zugehörig fühlen, unabhängig vom biologischen Geschlecht.