超越善与恶：区划编纂的安全保障形式化
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation
摘要：
划分是一种很好的安全工程实践。通过将一个大型软件系统分解为相互不信任的组件，这些组件以最小的权限运行，限制它们的交互以符合定义良好的接口，我们可以限制低级攻击（如控制流劫持）造成的损害。当用于防御此类攻击时，划分通常由编译器和低级划分机制协作实现。然而，令人惊讶的是，对这种划分汇编所提供的正式保证很少进行调查。我们提出了一个新的安全属性，安全划分编译（SCC），正式特征划分编译提供的保证，并澄清其攻击者模型。我们重建我们的财产从完善的概念完全抽象编译，然后确定和解除三个重要的限制，使标准的完全抽象不适合划分。连接到充分的抽象，使我们能够证明SCC适应既定的证明技术，我们说明了这一点与编译器从一个简单的不安全的命令式语言的程序划分的抽象机。
英文摘要：
Compartmentalization is good security-engineering practice. By breaking a large software system into mutually distrustful components that run with minimal privileges, restricting their interactions to conform to well-defined interfaces, we can limit the damage caused by low-level attacks such as control-flow hijacking. When used to defend against such attacks, compartmentalization is often implemented cooperatively by a compiler and a low-level compartmentalization mechanism. However, the formal guarantees provided by such compartmentalizing compilation have seen surprisingly little investigation. We propose a new security property, secure compartmentalizing compilation (SCC), that formally characterizes the guarantees provided by compartmentalizing compilation and clarifies its attacker model. We reconstruct our property by starting from the well-established notion of fully abstract compilation, then identifying and lifting three important limitations that make standard full abstraction unsuitable for compartmentalization. The connection to full abstraction allows us to prove SCC by adapting established proof techniques; we illustrate this with a compiler from a simple unsafe imperative language with procedures to a compartmentalized abstract machine.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
