Building Secure SGX Enclaves using F*, C/C++ and X64
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*.
|extended abstract (prisc18-paper1.pdf)||352KiB|
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
13:30 - 15:30
Session 2PriSC at Hershey
Chair(s): David Naumann Stevens Institute of Technology
|Building Secure SGX Enclaves using F*, C/C++ and X64|
Anitha Gollamudi , Cédric Fournet Microsoft ResearchFile Attached
|Robust Hyperproperty Preservation for Secure Compilation|
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-SWSPre-print File Attached
|Formally Secure Compilation of Unsafe Low-Level Components|
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 UniversityPre-print File Attached
|Secure Compilation in a Production Environment|
Vijay D'Silva GoogleFile Attached