超越善与恶：形式化隔离编译的安全保证

隔离是一种良好的安全工程实践。通过将大型软件系统拆分为以最小权限运行的相互不信任的组件，并将其交互限制为符合明确定义的接口，我们可以限制由控制流劫持等低级攻击造成的损害。当用于防御此类攻击时，隔离通常由编译器与低级隔离机制协作实现。然而，这种隔离编译所提供的形式化保证却鲜有研究。我们提出一种新的安全属性，即安全隔离编译（SCC），其形式化刻画了隔离编译所提供的保证并澄清了其攻击者模型。我们从已牢固确立的完全抽象编译概念出发重构该属性，进而识别并解除三个使标准完全抽象不适用于隔离的重要限制。与完全抽象的联系使我们能够通过调整既有证明技术来证明 SCC；我们以一个从带过程的简单不安全命令式语言到隔离抽象机的编译器为例说明了这一点。