BesFS：带机械化安全性证明的飞地 POSIX 文件系统
密码学与安全
2019-09-23 v2
摘要
Intel SGX 等新型可信计算原语已表明，在商用可信处理器上于飞地（enclave）中运行用户级应用而无需信任庞大操作系统是可行的。然而，操作系统仍可通过篡改系统调用返回值来破坏飞地的完整性。事实上，已有研究表明，一类称为 Iago 攻击的此类攻击可在飞地程序中实现任意逻辑执行。现有飞地系统具有非常大的 TCB（可信计算基），并在系统调用接口处实施难以验证完备性的临时检查。为此，我们提出 BesFS——首个可证明保护飞地完整性以抵御完全恶意操作系统的文件系统接口。我们在 4625 行 Coq 证明脚本中证明了 167 个引理与 2 个关键定理，直接证明了 BesFS 规范的安全性性质。BesFS 包含 15 个具有组合安全性的 API，且足以支持我们所测试的 31 个真实应用。BesFS 以对 TCB 最小的影响集成到现有支持 SGX 的应用中。BesFS 可作为手工编写 API 检查的参考实现。
引用
@article{arxiv.1807.00477,
title = {BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof},
author = {Shweta Shinde and Shengyi Wang and Pinghai Yuan and Aquinas Hobor and Abhik Roychoudhury and Prateek Saxena},
journal= {arXiv preprint arXiv:1807.00477},
year = {2019}
}
备注
Camera-ready version of the paper to appear at USENIX Security Symposium 2020