Guardian: symbolic validation of orderliness in SGX enclaves
This work addresses security vulnerabilities in SGX enclaves for developers and users of trusted execution environments, representing an incremental improvement by applying symbolic execution to a known bottleneck.
The paper tackles the problem of ensuring security in Intel SGX enclaves by proposing the concept of an 'orderly enclave' with execution phases and restrictions, and introduces a symbolic execution tool called Analyser to validate enclaves against this notion and detect vulnerabilities. The result includes the identification of real vulnerabilities in practical enclaves that were acknowledged and fixed by maintainers.
Modern processors can offer hardware primitives that allow a process to run in isolation. These primitives implement a trusted execution environment (TEE) in which a program can run such that the integrity and confidentiality of its execution are guaranteed. Intel's Software Guard eXtensions (SGX) is an example of such primitives and its isolated processes are called \emph{enclaves}. These guarantees, however, can be easily thwarted if the enclave has not been properly designed. Its interface with the untrusted software stack is arguably the largest attack surface that adversaries can exploit; unintended interactions with untrusted code can expose the enclave to memory corruption attacks, for instance. In this paper, we propose a notion of an \emph{orderly} enclave which splits its behaviour into several execution phases each of which imposes a set of restrictions on accesses to untrusted memory, phase transitions and registers sanitisation. A violation to these restrictions indicates an undesired behaviour which could be harnessed to perpetrate attacks against the enclave. We also introduce \Analyser{}: a tool that uses symbolic execution to carry out the validation of an enclave against our notion of an orderly enclave; in this process, it also looks for some typical memory-corruption vulnerabilities. We discuss how our approach can prevent and flag enclave vulnerabilities that have been identified in the literature. Moreover, we have evaluated how our approach fares in the analysis of some practical enclaves. \Analyser{} was able to identify real vulnerabilities on these enclaves which have been acknowledged and fixed by their maintainers.