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
Times are displayed in time zone: Tijuana, Baja California change

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