@inproceedings{gollamudi2018building,
author = {Gollamudi, Anitha and Fournet, Cédric},
title = {Building Secure SGX Enclaves using F*, C/C++ and X64},
booktitle = {PRISC’18},
year = {2018},
month = {January},
abstract = {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∗.},
url = {http://approjects.co.za/?big=en-us/research/publication/building-secure-sgx-enclaves-using-f-c-c-x64/},
edition = {PRISC’18},
}