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编译器。