Secure Compilation (Dagstuhl Seminar 18201)

Authors Amal Ahmed, Deepak Garg, Catalin Hritcu, Frank Piessens and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 7.17 MB
  • 30 pages

Document Identifiers

Author Details

Amal Ahmed
Deepak Garg
Catalin Hritcu
Frank Piessens
and all authors of the abstracts in this report

Cite AsGet BibTex

Amal Ahmed, Deepak Garg, Catalin Hritcu, and Frank Piessens. Secure Compilation (Dagstuhl Seminar 18201). In Dagstuhl Reports, Volume 8, Issue 5, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Secure compilation is an emerging field that puts together advances in security, programming languages, verification, systems, and hardware architectures in order to devise secure compilation chains that eliminate many of today's vulnerabilities. Secure compilation aims to protect a source language's abstractions in compiled code, even against low-level attacks. 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. The emerging secure compilation community aims to address such problems by devising formal security criteria, efficient enforcement mechanisms, and effective proof techniques. 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 developing proof techniques and verification tools, and on designing security mechanisms.
  • secure compilation
  • low-level attacks
  • source-level reasoning
  • attacker models
  • full abstraction
  • hyperproperties
  • enforcement mechanisms
  • compartmentalization
  • security architectures
  • side-channels


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail