Portable Software Fault Isolation
Portable Software Fault Isolation
复制标题
便携式软件故障隔离
DOI：
10.1109/csf.2014.10
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
A. Appel
中科院分区：
文献类型：
--
作者：
Joshua A. Kroll;Gordon Stewart;A. Appel
我们提出了一种用于架构可移植软件故障隔离 (SFI) 的新技术，以及 Coq 证明助手中的原型实现。与依赖于汇编级程序分析的传统 SFI 不同，我们使用编译器中间语言（Comp Cert C 编译器的 Cminor 语言）来分析和重写程序。但与传统的 SFI 一样，编译器仍然处于可信计算基础之外。通过将我们的程序转换器与经过验证的 Comp Cert 后端组合在一起，并利用 Comp Cert 正式证明的安全程序行为保留，我们可以获得满足 Comp Cert 支持的任何架构（当前：Power PC、ARM 和 x86-32）的 SFI 内存安全策略的二进制模块。这允许在多个架构中使用相同的 SFI 分析，从而大大简化了部署值得信赖的 SFI 系统中最困难的部分。
We present a new technique for architecture portable software fault isolation (SFI), together with a prototype implementation in the Coq proof assistant. Unlike traditional SFI, which relies on analysis of assembly-level programs, we analyze and rewrite programs in a compiler intermediate language, the Cminor language of the Comp Cert C compiler. But like traditional SFI, the compiler remains outside of the trusted computing base. By composing our program transformer with the verified back-end of Comp Cert and leveraging Comp Cert's formally proved preservation of the behavior of safe programs, we can obtain binary modules that satisfy the SFI memory safety policy for any of Comp Cert's supported architectures (currently: Power PC, ARM, and x86-32). This allows the same SFI analysis to be used across multiple architectures, greatly simplifying the most difficult part of deploying trustworthy SFI systems.