本文提出 Pandora，一种面向 Intel SGX 安全飞地运行时的符号执行验证工具。Intel SGX 技术通过硬件级飞地保护应用免受恶意操作系统攻击，但近年来出现了多种针对 SGX 飞地的攻击技术，导致屏蔽运行时（shielding runtime）需要频繁打补丁，验证工作复杂且快速变化。Pandora 的核心创新在于首次实现了对飞地运行时本身的可信、运行时无关的符号执行，它精确模拟被验证的飞地二进制代码，而非依赖抽象模型。Pandora 具备三项原则性基础：攻击者输入的精确污点跟踪（标记来自非可信 OS 的所有数据）、精确的符号飞地内存模型（支持分页、异常和中断等 SGX 特殊机制），以及可插拔的漏洞检测插件（如指针对齐、缓冲区溢出等）。作者在 11 种不同的 SGX 屏蔽运行时上部署了 4 个检测插件，覆盖多种漏洞类型。实验表明，Pandora 能自主发现 200 个新的和 69 个已知的脆弱代码位置。值得注意的是，Pandora 是首个能够对现实世界 SGX 飞地运行时进行大规模生态系统级指针对齐软件缓解措施评估的工具。本文工作对于 SGX 安全性的系统性验证具有重要推动作用。