Compiling Sandboxes: Formally Verified Software Fault Isolation
Compiling Sandboxes: Formally Verified Software Fault Isolation
复制标题
编译沙箱：经过正式验证的软件故障隔离
DOI：
10.1007/978-3-030-17184-1_18
复制
发表时间：
2019
影响因子：
--
通讯作者：
Pierre Wilke
中科院分区：
文献类型：
--
作者：
Frédéric Besson;Sandrine Blazy;Alexandre Dang;T. Jensen;Pierre Wilke
软件故障隔离（Software Fault Isolation，SFI）是一种增强安全性的程序转换，用于检测不受信任的二进制模块，使其在专用的隔离地址空间（称为沙箱）内运行。为了确保不受信任的模块无法逃脱其沙箱，现有的方法（如Google的Native Client）依赖于二进制验证器来检查所有内存访问是否在沙箱内。而不是依赖于后验验证，我们设计，实现和证明正确的程序插装阶段的一部分，正式验证编译器CompCert，强制沙箱的安全属性先验。这消除了对二进制验证器的需要，而是利用编译器的可靠性证明来证明沙箱转换的安全性。的技术贡献是一个新的沙盒转换，具有良好定义的C语义，并支持任意函数指针，和一个正式验证的C编译器，实现SFI。实验表明，我们的正式验证技术是一个有竞争力的方式实现SFI。
Software Fault Isolation (SFI) is a security-enhancing program transformation for instrumenting an untrusted binary module so that it runs inside a dedicated isolated address space, called a sandbox. To ensure that the untrusted module cannot escape its sandbox, existing approaches such as Google’s Native Client rely on a binary verifier to check that all memory accesses are within the sandbox. Instead of relying on a posteriori verification, we design, implement and prove correct a program instrumentation phase as part of the formally verified compiler CompCert that enforces a sandboxing security property a priori. This eliminates the need for a binary verifier and, instead, leverages the soundness proof of the compiler to prove the security of the sandboxing transformation. The technical contributions are a novel sandboxing transformation that has a well-defined C semantics and which supports arbitrary function pointers, and a formally verified C compiler that implements SFI. Experiments show that our formally verified technique is a competitive way of implementing SFI.