Pandora: Principled Symbolic Validation of Intel SGX Enclave Runtimes
Fritz Alder, Lesly-Ann Daniel, David Oswald, Frank Piessens, Jo Van Bulck
IEEE Symposium on Security and Privacy 2024 · Day 3 · Continental Ballroom 5
Intel Software Guard Extensions (**SGX**) are designed to provide a "fortress inside the process," allowing sensitive code and data to execute in isolation from the rest of the system, even a compromised operating system or hypervisor. However, as highlighted by speaker Yan Bu from the diset research group at KU Leuven, SGX has been a frequent target for attacks over the past decade, with many vulnerabilities stemming from its software interface – the "weakest point" where the untrusted world interacts with the trusted enclave. This talk introduces **Pandora**, a novel symbolic execution tool specifically designed to validate the security of Intel SGX **shielding runtimes**.
AI review
Pandora delivers a critical, principled symbolic execution framework for validating Intel SGX shielding runtimes, a previously underexplored attack surface. Its novel binary extraction and pluggable detection uncovered over 200 systemic vulnerabilities, providing an indispensable tool for securing foundational TEEs. This research sets a new standard for automated, deep security analysis in complex hardware-backed environments.