Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges and interactions. In this paper we introduce SECOMP, a compiler for compartmentalized C code that comes with machine-checked proofs guaranteeing that the scope of undefined behavior is restricted to the compartments that encounter it and become dynamically compromised. These guarantees are formalized as the preservation of safety properties against adversarial contexts, a secure compilation criterion similar to full abstraction, and this is the first time such a strong criterion is proven for a mainstream programming language. To achieve this we extend the languages of the CompCert verified C compiler with isolated compartments that can only interact via procedure calls and returns, as specified by cross-compartment interfaces. We adapt the passes and optimizations of CompCert as well as their correctness proofs to this compartment-aware setting. We then use compiler correctness as an ingredient in a larger secure compilation proof that involves several proof engineering novelties, needed to scale formally secure compilation up to a C compiler.

翻译：C语言中的未定义行为常导致严重的安全漏洞。一种实用的缓解措施是隔离化，它允许开发者将大型程序组织成互不信任的隔离区，各隔离区具有明确定义的特权与交互规范。本文提出SECOMP——一个针对隔离化C代码的编译器，并附带机器验证证明，确保未定义行为的影响范围仅限于遭遇该行为并动态受损的隔离区内部。这些保证被形式化为在对抗性环境下安全属性的保持，这是一种类似于完全抽象的强安全编译准则，也是首次在主流编程语言中实现并证明如此严格的标准。为实现这一目标，我们在CompCert验证C编译器的语言框架中扩展了隔离区机制，各隔离区仅能通过过程调用与返回进行交互，其交互方式由跨隔离区接口规范定义。我们调整了CompCert的编译阶段与优化策略及其正确性证明，使其适应这种具备隔离区感知的编译环境。随后，我们将编译器正确性作为构建更宏大的安全编译证明的关键组成部分，其中涉及多项验证工程创新，这些创新是实现C语言编译器形式化安全编译规模化所必需的。