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.
Conference DaySun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:15 - 10:00
|What is Secure Compilation? Part I|
Marco PatrignaniMPI-SWS, GermanyLink to publication
10:30 - 12:00
|What is Secure Compilation? Part II (Short talk)|
Cătălin HriţcuInria ParisLink to publication
|Can relational logic facilitate secure compilation? (Short talk)|
David NaumannStevens Institute of TechnologyFile Attached
|Full Abstraction for Language Design (Short talk)|
Gabriel SchererNortheastern UniversityFile Attached
|Cogent: Where we Stand and What Comes Next (Short talk)|
Christine RizkallahUniversity of Pennsylvania, USAFile Attached
|Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities|
14:00 - 15:30
|Linking Types: Secure compilation of multi-language programs|
Daniel PattersonNortheastern UniversityFile Attached
|Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing|
Dominique DevrieseiMinds - Distrinet, KU LeuvenFile Attached