Sat 13 Jan 2018 14:30 - 15:00 at Hershey - Session 2 Chair(s): David Naumann

We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion goes beyond recent proposals, which protect the trace properties of a single component against an adversarial context, to model dynamic compromise in a system of mutually distrustful components. Each component is protected from all the others until it receives an input that triggers an undefined behavior, causing it to become compromised and attack the remaining uncompromised components. To illustrate this model, we demonstrate a secure compilation chain for an unsafe language with buffers, procedures, and components, compiled to a simple RISC abstract machine with built-in compartmentalization. The protection guarantees offered by this abstract machine can be achieved at the machine-code level using either software fault isolation or tag-based reference monitoring. We are working on machine-checked proofs showing that this compiler satisfies our secure compilation criterion.

Conference Day
Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

13:30 - 15:30
Session 2PriSC at Hershey
Chair(s): David NaumannStevens Institute of Technology
13:30
30m
Talk
Building Secure SGX Enclaves using F*, C/C++ and X64
PriSC
File Attached
14:00
30m
Talk
Robust Hyperproperty Preservation for Secure Compilation
PriSC
Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniSaarland University, CISPA, Marco Stronati, David SwaseyMPI-SWS
Pre-print File Attached
14:30
30m
Talk
Formally Secure Compilation of Unsafe Low-Level Components
PriSC
Guglielmo FachiniInria Paris, Cătălin HriţcuInria Paris, Marco Stronati, Ana Nora EvansUniversity of Virginia, USA, Théo Laurent, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Benjamin C. PierceUniversity of Pennsylvania, Andrew TolmachPortland State University
Pre-print File Attached
15:00
30m
Talk
Secure Compilation in a Production Environment
PriSC
File Attached