Session
Schedule FOSDEM 2022
Hardware-Aided Trusted Computing

Symbolic Validation of SGX enclaves using Guardian

Avoid known enclave vulnerabilities by automatically checking for orderliness​
D.trusted-hardware
<p>The confidentiality and integrity guarantees offered by Intel SGX enclaves can be easily thwarted if the enclave has not been properly designed. Its interface with the untrusted software stack is a perhaps the largest attack surface that adversaries can exploit; unintended interactions with untrusted code can expose the enclave to memory corruption attacks, for instance.</p> <p>We have proposed a notion, called orderliness, that embodies good practice set out by academic papers and the principles of the Intel SGX SDK’s programming model. It is concerned especially with these interactions between the trusted and untrusted worlds. This notion underpins Guardian: an open-source tool that we have created to help enclave developers check their enclaves are orderly before they are deployed. It automatically validates enclaves and reports violations to our notion of orderliness. These violations help find parts of their code that may need changing – they should usually point to an attack primitive.</p> <p>We have found some security issues in enclaves that had been extensively vetted by other researchers – one of which was crafted by Intel engineers.</p>
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 in such a way 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 enclaves. These guarantees, however, can be easily undermined if the enclave has not been properly designed. We propose a notion of an orderly enclave that splits the enclave’s behaviour into the following execution phases: entry, secure, ocall, and exit. Each of them imposes a set of restrictions that enforce a particular policy of access to untrusted memory and, in some cases, sanitisation conditions. A violation of these policies and conditions might indicate an undesired interaction with untrusted data/code or a lack of sanitisation, both of which can be harnessed to perpetrate attacks against the enclave. We also introduce Guardian: an open-source 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 other typical attack primitives. 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 enclave samples. In this process, Guardian identified some previously undetected security issues in some of these samples. These were subsequently acknowledged and fixed by the corresponding maintainers.

Additional information

Type devroom

More sessions

2/5/22
Hardware-Aided Trusted Computing
D.trusted-hardware
<p>A brief introduction to the room and to the sessions.</p>
2/5/22
Hardware-Aided Trusted Computing
Shunda Zhang
D.trusted-hardware
<p>Intel SGX provided a mechanism to better isolate user-level software from attackers. However, attackers will still use various methods to attack SGX and user’s Enclaves. And user’s code inside Enclave may also have bugs, which can be leveraged by the attackers. We are from intel SGX SDK team, we have conducted security analysis and pen-test for SGX Enclave (based on SGX SDK) during the past 10+ years. We want to summarize some past exploits we encountered in our daily work and what's the ...
2/5/22
Hardware-Aided Trusted Computing
Dmitrii Kuvaiskii
D.trusted-hardware
<p>Gramine (formerly called "Graphene") is a lightweight library OS, designed to run a single Linux application in an isolated environment. Currently, Gramine runs on Linux and Intel SGX enclaves on Linux platforms. With Intel SGX support, Gramine can secure a critical application in a hardware-encrypted memory region and protect the application from a malicious system stack with minimal porting effort ("lift and shift" approach).</p> <p>Several major events happened to the Gramine project in ...
2/5/22
Hardware-Aided Trusted Computing
Nick Vidal
D.trusted-hardware
<p>The Enarx project reached a huge milestone: its first official release, featuring WebAssembly runtime. WebAssembly and Confidential Computing are a great match because WebAssembly offers developers a wide range of language choices, it works across silicon architectures, and it provides a sandboxed environment. This presentation will highlight the benefits of WebAssembly to Confidential Computing and showcase some demos.</p>
2/5/22
Hardware-Aided Trusted Computing
Fritz Alder
D.trusted-hardware
<p>Short break.</p>
2/5/22
Hardware-Aided Trusted Computing
Guilhem Bryant
D.trusted-hardware
<p>Veracruz is a framework for designing and deploying privacy-preserving computations amongst a group of mutually mistrusting individuals. Veracruz uses strong isolation technologies, such as AWS Nitro Enclaves, Arm CCA Realms, and the high-assurance seL4 hypervisor, to provide a safe, neutral ground, within which a sandboxed WebAssembly program executes. Recent enhancements to Veracruz have made it possible to support larger, more complex privacy-preserving computations: we have adopted the ...
2/5/22
Hardware-Aided Trusted Computing
Fritz Alder
D.trusted-hardware
<p>Lunch break</p>