Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications

Intel Software Guard Extensions (SGX) is a recent technology from Intel that makes it possible to execute security-critical parts of an application in a so-called SGX enclave, an isolated area of the system that is shielded from all other software (including the OS and/or hypervisor). SGX was designed with the objective of making it relatively straightforward to take a single module of an existing C application, and put that module in an enclave. The SGX SDK includes tooling to semi-automatically generate wrappers for an enclaved C module. The wrapped enclave can then easily be linked to the legacy application that uses the module. However, when the enclaved module and the surrounding application share a part of the heap and exchange pointers (a very common case in C programs), the generation of these wrappers requires programmer annotations and is error-prone - it is easy to introduce security vulnerabilities or program crashes. This paper proposes a separation logic based language for specifying the interface of the enclaved C module, and shows how such an interface specification can be used to automatically generate secure wrappers that avoid these vulnerabilities and crashes.