Secure compilation aims to preserve high-level language abstractions in compiled code, even against adversarial low-level contexts.
The Secure Compilation Meeting (SCM) takes a broad and inclusive view of secure compilation and provides a forum for discussion on the topic. The scope of SCM includes, but is not limited to, efficient enforcement mechanisms (based on static analysis, software rewriting, reference monitors, secure hardware, randomization, etc.), formal security properties (which go beyond compiler correctness, e.g., full abstraction, hyper-property or robust safety preservation, etc.) and effective proof techniques (based on logical relations, bisimulation, multi-language semantics, embedded interpreters, etc.)
The goal is to identify interesting research directions and open challenges by bringing together people working on building secure compilers, developing proof techniques and verification tools for security, and designing security-enhanced architectures.
The meeting’s first edition was held at INRIA, Paris in August, 2016 with 15 participants. The meeting was successful with several in-depth talks and long, synergistic discussions. The next edition will be held on January 15, 2017, co-located with POPL 2017. The scope will be expanded significantly. If you are interested in participating, please register for SCM through the POPL registration site.
List of talks
Call for Participation
SCM will be held on January 15, 2017. To participate, please register through the POPL registration system.
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:15 - 10:00 | |||
09:15 45mTalk | What is Secure Compilation? Part I SCM Marco Patrignani MPI-SWS, Germany Link to publication |
10:30 - 12:00 | |||
10:30 10mTalk | What is Secure Compilation? Part II (Short talk) SCM Cătălin Hriţcu Inria Paris Link to publication | ||
10:40 10mTalk | Can relational logic facilitate secure compilation? (Short talk) SCM David Naumann Stevens Institute of Technology File Attached | ||
10:50 10mTalk | Full Abstraction for Language Design (Short talk) SCM Gabriel Scherer Northeastern University File Attached | ||
11:00 10mTalk | Cogent: Where we Stand and What Comes Next (Short talk) SCM Christine Rizkallah University of Pennsylvania, USA File Attached | ||
11:15 45mTalk | Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities SCM File Attached |
14:00 - 15:30 | |||
14:00 45mTalk | Linking Types: Secure compilation of multi-language programs SCM Daniel Patterson Northeastern University File Attached | ||
14:45 45mTalk | Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing SCM Dominique Devriese iMinds - Distrinet, KU Leuven File Attached |
16:00 - 17:30 | |||
16:00 45mTalk | Software Fault Isolation avec CompCert SCM File Attached | ||
16:45 45mTalk | Security preserving compilation of low-level programs embedded in F* SCM Jonathan Protzenko Microsoft Research File Attached |