Guardian：SGX enclave中有序性的符号验证
密码学与安全
2021-05-14 v1 硬件体系结构
软件工程
摘要
现代处理器可提供硬件原语，使进程能够隔离运行。这些原语实现了可信执行环境（TEE），程序可在其中运行，其执行的完整性与机密性得到保证。英特尔的Software Guard eXtensions（SGX）即为此类原语的一例，其隔离进程称为enclave（ enclave）。然而，若enclave设计不当，这些保证很容易被规避。其与不可信软件栈的接口可谓攻击者可利用的最大攻击面；例如，与不可信代码的意外交互会使enclave暴露于内存破坏攻击之下。本文中，我们提出一种有序enclave的概念，将其行为划分为若干执行阶段，每阶段对不可信内存的访问、阶段转换及寄存器清理施加一组限制。违反这些限制即表明存在可能被用于针对enclave发起攻击的非预期行为。我们还引入了\Analyser{}：一种利用符号执行依据我们的有序enclave概念对enclave进行验证的工具；在此过程中，它亦搜寻若干典型的内存破坏漏洞。我们讨论了该方法如何能够预防并标记文献中已确认的enclave漏洞。此外，我们评估了该方法在分析若干实际enclave时的表现。\Analyser{}能够识别这些enclave上真实存在的漏洞，并已由其维护者确认并修复。
引用
@article{arxiv.2105.05962,
title = {Guardian: symbolic validation of orderliness in SGX enclaves},
author = {Pedro Antonino and Wojciech Aleksander Wołoszyn and A. W. Roscoe},
journal= {arXiv preprint arXiv:2105.05962},
year = {2021}
}