SECOMP: Formally Secure Compilation of Compartmentalized C Programs
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要