Today's computer systems are distressingly insecure. The correct semantics of mainstream low-level languages like C is inherently insecure, and even for safer languages, establishing security with respect to a high-level semantics does not prevent devastating low-level attacks. All the abstraction and security guarantees of the source language are currently lost when interacting with lower-level code, for instance when using low-level libraries. For a concrete example, all modern languages provide a notion of structured control flow and an invoked procedure is expected to return to the right place. However, today's compiler chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently enforce this abstraction: linked low-level code can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction.

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, verification, systems, and hardware architectures in order to devise secure compiler chains that eliminate many of today's low-level vulnerabilities. Secure compilation aims to protect high-level language abstractions in compiled code, even against adversarial low-level contexts, and to allow sound reasoning about security in the source language. The emerging secure compilation community aims to achieve this by:

1. Identifying and formalizing compiler security properties and attacker models. What are the properties we want secure compilers to have, and under what attacker models? Should a secure compiler preserve observational equivalence of programs? Should it preserve some class of security properties of the source programs? Should it guarantee invariants on the run-time state of the compiled program (like for instance well-formedness of the call-stack)? And what are realistic attacker models? Can attackers only interact with compiled programs by providing input and reading output? Or can they link arbitrary target level code to the program? Well-studied notions like fully abstraction compilation provide partial answers: a fully abstract compiler chain preserves observational equivalence under an attacker model where attackers are target level contexts. But this can be too hard to enforce: for instance in cases where target level contexts can measure time, this would imply resistance against timing side-channel attacks.
2. Efficient enforcement mechanisms. The main reason today's compiler chains are not secure is that providing a secure semantics and enforcing abstractions in low-level compiled code can be very inefficient. In order to overcome this problem, the secure compilation community is investigating various efficient security enforcement mechanisms: from the use of static checking of low-level code to rule out linking with ill-behaved attackers, to software rewriting (e.g. software fault isolation), dynamic monitoring, and randomization. One key enabler is that hardware support to aid security is steadily increasing.
3. Developing effective formal verification techniques. Secure compilation properties like full abstraction are much harder to prove than compiler correctness. Intuitively, in order to show full abstraction one has to be able to back-translate any low-level context attacking the compiled code to an equivalent high-level context that can attack the original source code. This back-translation is, however, nontrivial, and while several proof techniques have been proposed (e.g. based on logical relations, bisimulation, game semantics, multi-language semantics, embedded interpreters, etc), scaling these techniques to realistic secure compilers is a challenging research problem. This challenge becomes even more pronounced if one expects a strong level of assurance, as provided by formal verification using a proof assistant.

This Dagstuhl Seminar will take a broad and inclusive view of secure compilation and will provide a forum for discussion on the topic. The goal is to identify interesting research directions and open challenges by bringing together people interested in working on building secure compilers, on developing proof techniques and verification tools, and on designing security mechanisms.

Creative Commons BY 3.0 DE

Amal Ahmed, Deepak Garg, Catalin Hritcu, and Frank Piessens

• Amal Ahmed (Northeastern University - Boston, US) [dblp]
• Gilles Barthe (IMDEA Software - Madrid, ES) [dblp]
• Nick Benton (Facebook - London, GB) [dblp]
• Frédéric Besson (INRIA - Rennes, FR) [dblp]
• Pramod Bhatotia (University of Edinburgh, GB) [dblp]
• Lars Birkedal (Aarhus University, DK) [dblp]
• Roberto Blanco (INRIA - Paris, FR) [dblp]
• William Bowman (Northeastern University - Boston, US) [dblp]
• Stefan Brunthaler (Universität der Bundeswehr - München, DE) [dblp]
• David Chisnall (University of Cambridge, GB) [dblp]
• John T. Criswell (University of Rochester, US) [dblp]
• Dominique Devriese (KU Leuven, BE) [dblp]
• Derek Dreyer (MPI-SWS - Saarbrücken, DE) [dblp]
• Akram El-Korashy (MPI-SWS - Saarbrücken, DE) [dblp]
• Cédric Fournet (Microsoft Research UK - Cambridge, GB) [dblp]
• Deepak Garg (MPI-SWS - Saarbrücken, DE) [dblp]
• Chris Hawblitzel (Microsoft Research - Redmond, US) [dblp]
• Catalin Hritcu (INRIA - Paris, FR) [dblp]
• Chung-Kil Hur (Seoul National University, KR) [dblp]
• Limin Jia (Carnegie Mellon University - Pittsburgh, US) [dblp]
• Gabriele Keller (UNSW - Sydney, AU) [dblp]
• Vincent Laporte (IMDEA Software - Madrid, ES) [dblp]
• Xavier Leroy (INRIA - Paris, FR) [dblp]
• Toby Murray (The University of Melbourne, AU) [dblp]
• Magnus Myreen (Chalmers University of Technology - Göteborg, SE) [dblp]
• Santosh Nagarakatte (Rutgers University - Piscataway, US) [dblp]
• Kedar Namjoshi (Nokia Bell Labs - Murray Hill, US) [dblp]
• David A. Naumann (Stevens Institute of Technology, US) [dblp]
• Max S. New (Northeastern University - Boston, US) [dblp]
• Scott Owens (University of Kent - Canterbury, GB) [dblp]
• Zoe Paraskevopoulou (Princeton University, US) [dblp]
• Marco Patrignani (Universität des Saarlandes, DE) [dblp]
• Daniel Patterson (Northeastern University - Boston, US) [dblp]
• Frank Piessens (KU Leuven, BE) [dblp]
• Tamara Rezk (INRIA Sophia Antipolis, FR) [dblp]
• Christine Rizkallah (UNSW - Sydney, AU) [dblp]
• Peter Sewell (University of Cambridge, GB) [dblp]
• Deian Stefan (University of California - San Diego, US) [dblp]
• Andrew Tolmach (Portland State University, US) [dblp]
• Stelios Tsampas (KU Leuven, BE)
• Neline van Ginkel (KU Leuven, BE) [dblp]
• Stephanie Weirich (University of Pennsylvania - Philadelphia, US) [dblp]
• Steve Zdancewic (University of Pennsylvania - Philadelphia, US) [dblp]