https://www.dagstuhl.de/18201

13. – 18. Mai 2018, Dagstuhl-Seminar 18201

Secure Compilation

Organisatoren

Amal Ahmed (Northeastern University – Boston, US)
Deepak Garg (MPI-SWS – Saarbrücken, DE)
Catalin Hritcu (INRIA – Paris, FR)
Frank Piessens (KU Leuven, BE)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team

Dokumente

Dagstuhl Report, Volume 8, Issue 5 Dagstuhl Report
Motivationstext
Teilnehmerliste
Gemeinsame Dokumente
Programm des Dagstuhl-Seminars [pdf]

Summary

Today's computer systems are distressingly insecure. The semantics of mainstream low-level languages like C and 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. In particular, 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 compilation 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 low-level attacks, 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 secure compilation criteria and attacker models. What are the properties we want secure compilers to have, and under what attacker models? Should a secure compilation chain 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 low-level code to the program? Well-studied notions like fully abstract compilation provide partial answers: a fully abstract compiler chain preserves observational equivalence under an attacker model where attackers are target-level contexts. Even where this is the desired end-to-end security goal, it can still be too hard to enforce, for instance in cases where target level contexts can measure time.
  2. Efficient enforcement mechanisms. The main reason today's compiler chains are not secure is that 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 contexts, to software rewriting (e.g., software fault isolation), dynamic monitoring, and randomization. One key enabler is that hardware support for security is steadily increasing.
  3. Developing effective formal verification techniques. Secure compilation properties like full abstraction are generally 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, bisimulations, 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.

The Secure Compilation Dagstuhl Seminar 18201 attracted a large number of excellent researchers with diverse backgrounds. The 45 participants represented the programming languages, formal verification, security, and systems communities, which led to many interesting points of view and enriching discussions. Some of these discussions were ignited by the "guided discussions" on the 3 aspects above and by the 35 talks contributed by the participants. The contributed talks spanned a very large number of topics: investigating various secure compilation criteria and attacker models, building prototype secure compilation chains, proposing different enforcement techniques, studying the relation to verified compilation and compositional compiler correctness, specifying and restricting undefined behavior, protecting against side-channels, studying intermediate representations, performing translation validation, securing multi-language interoperability, controlling information-flow, compartmentalizing software, enforcing memory safety, compiling constant-time cryptography, securing compiler optimizations, designing more secure (domain-specific) languages, enforcing security policies, formally specifying the semantics of realistic languages and ISAs, compartmentalization, capability machines, tagged architectures, integrating with existing compilation chains like LLVM, making exploits more difficult by diversification, multi-language interoperability, etc. Talks were interspersed with lively discussions, since by default each speaker could only use half of the time for presenting and had to use the other half for answering questions and engaging with the audience.

Given the high interest spurred by this first edition and the positive feedback received afterwards, we believe that this Dagstuhl Seminar should be repeated in the future. Particular aspects that could still be improved in future editions is focusing more on secure compilation and spurring more participation from the practical security and systems communities.

License
  Creative Commons BY 3.0 Unported license
  Amal Ahmed, Deepak Garg, Catalin Hritcu, and Frank Piessens

Classification

  • Hardware
  • Programming Languages / Compiler
  • Security / Cryptology

Keywords

  • Secure compilation
  • Low-level attacks and defenses
  • Security architectures
  • Compiler verification
  • Full abstraction

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.