License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.11.10.173
URN: urn:nbn:de:0030-drops-159332
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15933/
Chisnall, David ;
Garg, Deepak ;
Hritcu, Catalin ;
Payer, Mathias
Weitere Beteiligte (Hrsg. etc.): David Chisnall and Deepak Garg and Catalin Hritcu and Mathias Payer
Secure Compilation (Dagstuhl Seminar 21481)
Abstract
Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, verification, systems, and hardware architectures in order to devise more secure compilation chains that eliminate many of today’s security vulnerabilities and that allow sound reasoning about security properties in the source language. 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 against 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 today’s languages fail to specify security policies, such as data confidentiality, and the compilation chains thus fail to enforce them, especially against powerful side-channel attacks. The emerging secure compilation community aims to address such problems by identifying precise security goals and attacker models, designing more secure languages, devising efficient enforcement and mitigation mechanisms, and developing effective verification techniques for secure compilation chains.
This seminar strived to take a broad and inclusive view of secure compilation and to provide a forum for discussion on the topic. The goal was to identify interesting research directions and open challenges by bringing together people working on building secure compilation chains, on designing security enforcement and attack-mitigation mechanisms in both software and hardware, and on developing formal verification techniques for secure compilation.
BibTeX - Entry
@Article{chisnall_et_al:DagRep.11.10.173,
author = {Chisnall, David and Garg, Deepak and Hritcu, Catalin and Payer, Mathias},
title = {{Secure Compilation (Dagstuhl Seminar 21481)}},
pages = {173--204},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2022},
volume = {11},
number = {10},
editor = {Chisnall, David and Garg, Deepak and Hritcu, Catalin and Payer, Mathias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15933},
URN = {urn:nbn:de:0030-drops-159332},
doi = {10.4230/DagRep.11.10.173},
annote = {Keywords: secure compilation, low-level attacks, source-level reasoning, attacker models, full abstraction, hyperproperties, enforcement mechanisms, compartmentalization, security architectures, side-channels}
}
|
Keywords: |
|
secure compilation, low-level attacks, source-level reasoning, attacker models, full abstraction, hyperproperties, enforcement mechanisms, compartmentalization, security architectures, side-channels |
|
Collection: |
|
DagRep, Volume 11, Issue 10 |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
11.04.2022 |
