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

prisc-2018
13:30 - 15:30: PriSC 2018 - Session 2 at Hershey
Chair(s): David NaumannStevens Institute of Technology
prisc-2018151584660000013:30 - 14:00
Talk
File Attached
prisc-2018151584840000014:00 - 14:30
Talk
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
prisc-2018151585020000014:30 - 15:00
Talk
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
prisc-2018151585200000015:00 - 15:30
Talk
File Attached