Automatically Generating Secure Wrappers For Sgx Enclaves From Separation Logic Specifications
PROGRAMMING LANGUAGES AND SYSTEMS (APLAS 2017)(2017)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要