[AI-announce] Invitation: Inaugural lecture Catalin Hritcu, April 30

[Schab, Charlotte]

Dear all,

the Faculty of Computer Science cordially invites you to Prof. Dr. Catalin Hritcu's inaugural lecture "My Group's Journey in Secure Compilation"

When? April 30, 4-5 pm lecture, afterwards get together with pizza and drinks
Where? Building MC, Open Space
Registration: https://terminplaner6.dfn.de/de/b/2168e90c4da44102ad0b2c9ede6a1f4f-1168574

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.


We are looking forward to welcoming many of you!

Best wishes
Charlotte


Charlotte Schab, M.Sc.
RUHR-UNIVERSITÄT BOCHUM
FAKULTÄT FÜR INFORMATIK
Marketing und PR | Marketing and PR

Phone:                 +49-(0)234 / 32-19251
Pers. Email:        charlotte.schab at rub.de<mailto:charlotte.schab at rub.de>
Internet:             www.informatik.rub.de<http://www.informatik.rub.de/>

Universitätsstraße 150, D-44801 Bochum
MC, 1st floor, room 62

-------------- nächster Teil --------------
Ein Dateianhang mit HTML-Daten wurde abgetrennt...
URL: <http://lists.ruhr-uni-bochum.de/pipermail/ai-announce/attachments/20250402/41f0de9e/attachment.htm>