IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2024 > Secure compilation at scale: from C to CHERI
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

martes 8 de octubre de 2024

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)

Roberto Blanco, Postdoc, Max Planck Institute for Security and Privacy and the CASA cluster of excellence in Bochum (Germany)

Secure compilation at scale: from C to CHERI

Abstract:

Virtually all computer programs are written in high-level languages. A suitable source language can impose certain desirable properties (like memory or type safety), or it can facilitate reasoning about a program satisfying a given spec (formally or informally). However, there is a deep gulf between programs as they are written and executed: compiled to low-level representations, and running in an untrusted medium where source-level guarantees dissolve. And whereas the correctness of compilation is a well-understood problem with proven solutions, its security considerations are much less clear. In particular, what security guarantees should a compiler provide, and how can we specify them formally? Can we implement them efficiently and verify them with reasonable effort? And can we hope to achieve all this for practical programming languages, compilers and hardware? In this talk I will present our answers to these questions through SECOMP, a fully verified secure compiler that builds security on top of the CompCert C verified compiler. These include a flexible compartment model for CompCert C, security definitions and scalable proof techniques for them, and low-level enforcement based on CHERI-style capability machines.