TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 21481

Secure Compilation

( 28. Nov – 03. Dec, 2021 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/21481

Organisatoren

Kontakt


Programm

Motivation

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, systems, verification, and hardware architectures to devise compilation chains that eliminate security vulnerabilities, and allow sound reasoning about security properties in the source language. For example, all modern languages define valid control flows, e.g., calls must always return to the instruction after the calling point, and many security-critical analyses such as data flow analysis rely on programs adhering to these valid control flows. However, today's compilation chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently prevent violations of source-level control flows by co-linked low-level code, which can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction. Other problems arise because languages fail to specify security policies, such as data confidentiality, and the compilation chains thus fail to enforce them, especially against powerful attacks like side-channels. Yet other problems arise because enforcing source-level abstractions requires runtime checks with noticeable overhead, so compilation chains often forego security properties in favor of efficient code.

The emerging secure compilation field aims to address such problems by:

  1. Identifying precise security goals and attacker models. Since there are many interesting security goals and many different kind of attacks to defend against, secure compilation is very diverse. Secure compilation chains may focus on providing (some degree of) type and memory safety for unsafe low-level languages like C and C++, or on providing mitigations that make exploiting security vulnerabilities more difficult. Other secure compilation chains use compartmentalization to limit the damage of an attack to only those components that encounter undefined behavior, or to enforce secure interoperability between code written in a safer language (like Java, C#, ML, Haskell, or Rust) and the malicious or compromised code it links against. Yet another kind of secure compilation tries to ensure that compilation and execution on a real machine does not introduce side-channel attacks.
  2. Designing secure languages. Better designed programming languages and new language features can enable secure compilation in various ways. New languages can provide safer semantics, and updates to the semantics of old unsafe languages can turn some undefined behaviors into guaranteed errors. Components or modules in the source language can be used as units of compartmentalization in the compilation chain. The source language can also make it easier to specify the intended security properties. For instance, explicitly annotating secret data that external observers or other components should not be able to obtain (maybe indirectly through side channels) may give the compilation chain the freedom to more efficiently handle any data that is not influenced by secrets.
  3. Devising efficient enforcement and mitigation mechanisms. An important reason for the insecurity of today’s compilation chains is that enforcing security can incur prohibitive overhead or significant compatibility issues. To overcome these problems, the secure compilation community is investigating various efficient security enforcement mechanisms such as statically checking low-level code, compiler optimizations, software rewriting (e.g. software fault isolation), dynamic monitoring, and randomization. Another key enabler is the emergence of new hardware features that enable efficient security enforcement: access checks on pointer dereferencing (e.g. Intel MPX, Hardbound, WatchdogLite, Oracle SSM, SPARC ADI, or HWASAN), protected enclaves (e.g. Intel SGX, ARM TrustZone, Sanctum, or Sancus), capability machines (e.g. CHERI), or micro-policy machines (e.g. Draper PUMP, Dover CoreGuard). The question is how these features can be used to offer various security features in source languages efficiently.
  4. Developing effective verification techniques for secure compilation chains. Criteria for secure compilation are generally harder to prove than compiler correctness. As an example, showing full abstraction, a common criterion for secure compilation, requires translating any low-level context attacking the compiled code to an equivalent high-level context that can attack the original source code. Another example is preservation of secret independent timing even in the presence of side-channels, as required for “constant-time” cryptographic implementations, which requires more complex simulation proofs than for compiler correctness. Finally, scaling such proofs up to even a simple compilation chain for a realistic language is a serious challenge that requires serious proof engineering in a proof assistant.

This seminar strives to take a broad and inclusive view of secure compilation and to provide a forum for discussion on the topic. The goal is to identify interesting research directions and open challenges by bringing together people working on building secure compilation chains, designing security enforcement and attack-mitigation mechanisms in both software and hardware, and on developing formal verification techniques for secure compilation.

Copyright David Chisnall, Deepak Garg, Catalin Hritcu, and Mathias Payer

Summary

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, systems, verification, and hardware architectures to devise compilation chains that eliminate security vulnerabilities, and allow sound reasoning about security properties in the source language. For example, all modern languages define valid control flows, e.g., calls must always return to the instruction after the calling point, and many security-critical analyses such as data flow analysis rely on programs adhering to these valid control flows. However, today's compilation chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently prevent violations of source-level control flows by co-linked low-level code, which can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction. Other problems arise because languages fail to specify security policies, such as data confidentiality, and the compilation chains thus fail to enforce them, especially against powerful attacks such as those based on side channels. Yet other problems arise because enforcing source-level abstractions requires runtime checks with noticeable overhead, so compilation chains often forego security properties in favor of efficient code. The emerging field of secure compilation aims to address such problems by:

  1. Identifying precise security goals and attacker models.
    Since there are many interesting security goals and many different kind of attacks to defend against, secure compilation is very diverse. Secure compilation chains may focus on providing (some degree of) type and memory safety for unsafe low-level languages like C and C++, or on providing mitigations that make exploiting security vulnerabilities more difficult. Other secure compilation chains use compartmentalization to limit the damage of an attack to only those components that encounter undefined behavior, or to enforce secure interoperability between code written in a safer language (like Java, C#, ML, Haskell, or Rust) and the malicious or compromised code it links against. Yet another kind of secure compilation tries to ensure that compilation and execution on a real machine does not introduce side-channel attacks.
  2. Designing secure languages.
    Better designed programming languages and new language features can enable secure compilation in various ways. New languages can provide safer semantics, and updates to the semantics of old unsafe languages can turn some undefined behaviors into guaranteed errors. Components or modules in the source language can be used as units of compartmentalization in the compilation chain. The source language can also make it easier to specify the intended security properties. For instance, explicitly annotating secret data that external observers or other components should not be able to obtain (maybe indirectly through side channels) may give the compilation chain the freedom to more efficiently handle any data that it can deduce is not influenced by secrets.
  3. Devising efficient enforcement and mitigation mechanisms.
    An important reason for the insecurity of today's compilation chains is that enforcing security can incur prohibitive overhead or significant compatibility issues. To overcome these problems, the secure compilation community is investigating various efficient security enforcement mechanisms such as statically checking low-level code, compiler optimizations, software rewriting (e.g. software fault isolation), dynamic monitoring, and randomization. Another key enabler is the emergence of new hardware features that enable efficient security enforcement: access checks on pointer dereferencing (e.g. Intel MPX, Hardbound, WatchdogLite, Oracle SSM, SPARC ADI, or HWASAN), protected enclaves (e.g. Intel SGX, ARM TrustZone, Sanctum, or Sancus), capability machines (e.g. CHERI, Arm Morello), or micro-policy machines (e.g. Draper PUMP, Dover CoreGuard). The question is how such features can enable various security features in source languages efficiently, i.e., how hardware extensions can provide enforcement mechanisms for security properties.
  4. Developing effective verification techniques for secure compilation chains
    Criteria for secure compilation are generally harder to prove than compiler correctness. As an example, showing full abstraction, a common criterion for secure compilation, requires translating any low-level context attacking the compiled code to an equivalent high-level context that can attack the original source code. Another example is preservation of secret independent timing even in the presence of side-channels, as required for ``constant-time'' cryptographic implementations, which can require more complex simulation proofs than for compiler correctness. Finally, scaling such proofs up to even a simple compilation chain for a realistic language is a serious challenge that requires serious proof engineering in a proof assistant.

The Secure Compilation Dagstuhl Seminar 21481 attracted a large number of excellent researchers with diverse backgrounds. The 42 participants (12 on site, 30 remote) represented the programming languages, formal verification, compilers, security, systems, and hardware communities, which led to many interesting points of view and enriching discussions. Due to COVID-19 pandemic-related travel restrictions and uncertainties, many of the participants had to participate remotely using a combination of video conferencing, instant messaging, and ad-hoc gatherings. Despite this mixed environment, discussions thrived. Some of these conversations were ignited by the 5 plenary discussions and the 28 talks contributed by the participants. The contributed talks spanned a very broad range of topics: formalizing ISA security guarantees, hardware-software contracts, detection and mitigation of (micro-architectural) side-channel attacks, securing trusted execution environments, memory safety, hardware-assisted testing, sampled bug detection, formal verification techniques for low-level languages and secure compilation chains, machine-checked proofs, stack safety, integrating hardware-safety guarantees, effective compartmentalization and its enforcement, cross-language attacks, security challenges of software supply chains, capability machines, (over-)aggressive compiler optimizations, concurrency, new programming language abstractions, compositional correct/secure compilation, component safety, compositional verification, contextual and secure refinement, hardening WebAssembly, secure interoperability, (not) forking compilers, interrupts, hardware design, and many more. 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 second edition and the positive feedback received afterwards, we believe that this Dagstuhl Seminar should be repeated in the future, when hopefully all the participants will be able to attend onsite. One important aspect that could still be improved in future editions is spurring more participation from the systems and hardware communities, especially people working at the intersection of these areas and security or formal verification.

Copyright David Chisnall, Deepak Garg, Catalin Hritcu, and Mathias Payer

Teilnehmer
Vor Ort
  • Roberto Blanco (MPI-SP - Bochum, DE) [dblp]
  • Stefan Brunthaler (Universität der Bundeswehr - München, DE) [dblp]
  • Matteo Busi (University of Pisa, IT)
  • Dominique Devriese (KU Leuven, BE) [dblp]
  • Akram El-Korashy (MPI-SWS - Saarbrücken, DE) [dblp]
  • Deepak Garg (MPI-SWS - Saarbrücken, DE) [dblp]
  • Anitha Gollamudi (Yale University - New Haven, US)
  • Marco Guarnieri (IMDEA Software - Madrid, ES) [dblp]
  • Catalin Hritcu (MPI-SP - Bochum, DE) [dblp]
  • Marco Patrignani (CISPA - Saarbrücken, DE) [dblp]
  • Jan Reineke (Universität des Saarlandes - Saarbrücken, DE) [dblp]
  • Shweta Shinde (ETH Zürich, CH)
  • Jeremy Thibault (MPI-SP - Bochum, DE)
  • Thomas Van Strydonck (KU Leuven, BE)
  • Ingrid Verbauwhede (KU Leuven, BE) [dblp]
Remote:
  • Amal Ahmed (Northeastern University - Boston, US) [dblp]
  • Arthur Azevedo de Amorim (Boston University, US) [dblp]
  • Gilles Barthe (MPI-SP - Bochum, DE) [dblp]
  • Joseph Bialek (Microsoft - Redmond, US)
  • Sandrine Blazy (University & IRISA - Rennes, FR) [dblp]
  • Nathan Burow (MIT Lincoln Laboratory - Lexington, US) [dblp]
  • David Chisnall (Microsoft Research - Cambridge, GB) [dblp]
  • Mads Dam (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
  • Ergys Dona (EPFL Lausanne, CH)
  • Cédric Fournet (Microsoft Research - Cambridge, GB) [dblp]
  • Tal Garfinkel (Corepoint Systems - Penn Valley, US) [dblp]
  • Chung-Kil Hur (Seoul National University, KR) [dblp]
  • Jérémie Koenig (Yale University - New Haven, US)
  • Per Larsen (Immunant - Irvine, US) [dblp]
  • Amit Levy (Princeton University, US) [dblp]
  • Toby Murray (The University of Melbourne, AU) [dblp]
  • Andrew Myers (Cornell University - Ithaca, US) [dblp]
  • Santosh Nagarakatte (Rutgers University - Piscataway, US) [dblp]
  • Elisabeth Oswald (Alpen-Adria-Universität Klagenfurt, AT) [dblp]
  • Zoe Paraskevopoulou (Northeastern University - Boston, US) [dblp]
  • Mathias Payer (EPFL - Lausanne, CH) [dblp]
  • Andreas Rossberg (Dfinity - Zürich, CH) [dblp]
  • Kostya Serebryany (Google - Mountain View, US) [dblp]
  • Peter Sewell (University of Cambridge, GB) [dblp]
  • Zhong Shao (Yale University - New Haven, US) [dblp]
  • Deian Stefan (University of California - San Diego, US) [dblp]
  • G. Gary Tan (Pennsylvania State University - University Park, US) [dblp]
  • Nikos Vasilakis (MIT - Cambridge, US)
  • Marco Vassena (CISPA - Saarbrücken, DE) [dblp]
  • Drew Zagieboylo (Cornell University - Ithaca, US)

Verwandte Seminare
  • Dagstuhl-Seminar 18201: Secure Compilation (2018-05-13 - 2018-05-18) (Details)

Klassifikation
  • programming languages / compiler
  • security / cryptology
  • semantics / formal methods

Schlagworte
  • secure compilation
  • low-level attacks
  • source-level reasoning
  • attacker models
  • full abstraction
  • hyperproperties
  • enforcement mechanisms
  • compartmentalization
  • security architectures
  • side-channels