“Proving – manually or automatically – that security properties are preserved by compilers.”
Modern programming languages provide helpful high-level abstractions and mechanisms (e.g. types, module, automatic memory management) that enforce good programming practices and are crucial when writing correct and secure code. However, the security guarantees provided by such abstractions are not preserved when a compiler translates a source program into object code. Formally secure compilation is an emerging research field concerned with the design and the implementation of compilers that preserve source-level security properties at the object level.
Bibliograpy
- A recent survey on Secure Compilation
- Matteo Busi and Letterio Galletta. “A Brief Tour of Formally Secure Compilation.” ITASEC 2019. [paper]
- Extended abstracts about ongoing work
- Matteo Busi, Job Noorman, Jo Van Bulck, Letterio Galletta, Pierpaolo Degano, Jan Tobias Mühlberg, Frank Piessens. “Securing Interruptible Enclaves”. To appear PriSC 2020.
- Matteo Busi, Pierpaolo Degano, and Letterio Galletta. “Translation Validation for Security Properties.” PriSC 2019. [extended abstract]
- Talks