Formally Secure Compilation of Unsafe Low-Level Components
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.
slides (2018-01-13-Secure-Compilation-PriSC.pdf) | 1.47MiB |
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
13:30 - 15:30 | |||
13:30 30mTalk | Building Secure SGX Enclaves using F*, C/C++ and X64 PriSC File Attached | ||
14:00 30mTalk | Robust Hyperproperty Preservation for Secure Compilation PriSC Deepak Garg Max Planck Institute for Software Systems, Cătălin Hriţcu Inria Paris, Marco Patrignani Saarland University, CISPA, Marco Stronati , David Swasey MPI-SWS Pre-print File Attached | ||
14:30 30mTalk | Formally Secure Compilation of Unsafe Low-Level Components PriSC Guglielmo Fachini Inria Paris, Cătălin Hriţcu Inria Paris, Marco Stronati , Ana Nora Evans University of Virginia, USA, Théo Laurent , Arthur Azevedo de Amorim Carnegie Mellon University, USA, Benjamin C. Pierce University of Pennsylvania, Andrew Tolmach Portland State University Pre-print File Attached | ||
15:00 30mTalk | Secure Compilation in a Production Environment PriSC Vijay D'Silva Google File Attached |