Guardian: symbolic validation of orderliness in SGX enclaves

TL;DR

This paper introduces a symbolic validation method for SGX enclaves called Guardian, which enforces phased behavior restrictions to prevent memory corruption and other vulnerabilities, improving enclave security.

Contribution

It proposes the concept of orderly enclaves with phased restrictions and presents exttt{Analyser}, a symbolic execution tool for validation and vulnerability detection.

Findings

exttt{Analyser} successfully identified real vulnerabilities in practical enclaves.

The approach effectively flags potential memory corruption vulnerabilities.

Orderly enclave design enhances enclave security against common attack vectors.

Abstract

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.