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

Intel SGX offers hardware mechanisms to isolate code and data running within enclaves from the rest of the platform. This enables security verification on a relatively small software TCB, but the task still involves complex low-level code.

Relying on the Everest verification toolchain, we use F* for developing specifications, code, and proofs; and then safely compile F* code to standalone C code. However, this does not account for all code running within the enclave, which also includes trusted C and assembly code for bootstrapping and for core libraries. Besides, we cannot expect all enclave applications to be rewritten in F*, so we also compile legacy C++ defensively, using variants of /guard that dynamically enforce their safety at runtime.

To reason about enclave security, we thus compose different sorts of code and verification styles, from fine-grained statically-verified F* to dynamically-monitored C++ and custom SGX instructions.

This involves two related program semantics: most of the verification is conducted within F* using the target semantics of Kremlin—a fragment of C with a structured memory—whereas SGX features and dynamic checks embedded by defensive C++ compilers require lower-level X64 code, for which we use the verified assembly language for Everest (VALE) and its embedding in F*.

Presentation (Gollamudi-Prisc-2018.pdf)4.67MiB
extended abstract (prisc18-paper1.pdf)352KiB

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

13:30 - 15:30
Session 2PriSC at Hershey
Chair(s): David Naumann Stevens Institute of Technology
13:30
30m
Talk
Building Secure SGX Enclaves using F*, C/C++ and X64
PriSC
Anitha Gollamudi , Cédric Fournet Microsoft Research
File Attached
14:00
30m
Talk
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
30m
Talk
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
30m
Talk
Secure Compilation in a Production Environment
PriSC
File Attached