Pandora is a symbolic execution tool designed for truthful validation of enclave shielding runtimes across diverse TEE architectures. Built on the fabulous angr framework, Pandora extends it with enclave-aware semantics such as enclave loading, a powerful symbolic memory model to support enclaves in a shared address space, principled taint tracking, human-readable HTML report generation, and a suite of vulnerability detection plugins.
Originally developed for Intel SGX (📄 IEEE S&P'24 paper), Pandora's core infrastructure has since been generalized into a TEE-agnostic base, with support extended to the Sancus (📄 SysTEX'25 paper) and openIPE (📄 EuroS&P'25 paper) enclave architectures.
If you use Pandora, please cite:
@inproceedings{alder2024pandora,
title={Pandora: Principled Symbolic Validation of Intel SGX Enclave Runtimes},
author={Alder, Fritz and Daniel, Lesly-Ann and Oswald, David and Piessens, Frank and Van Bulck, Jo},
booktitle={45th IEEE Symposium on Security and Privacy-IEEE S\&P 2024},
year={2024},
organization={IEEE}
}
This organization has four repositories:
- pandora: The symbolic execution tool for enclave runtimes, written in Python.
- sgx-tracer: A C program to dump SGX enclave memory during its initialization.
- examples: Example enclaves written in C to check common enclave runtimes or test Pandora.
- reports: Artifacts of our research results as reported in our original S&P'24 paper.
