SECOMP: Formally Secure Compilation of Compartmentalized C Programs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910767610068992 |
|---|---|
| author | Thibault, Jérémy Blanco, Roberto Lee, Dongjae Argo, Sven de Amorim, Arthur Azevedo Georges, Aïna Linn Hritcu, Catalin Tolmach, Andrew |
| author_facet | Thibault, Jérémy Blanco, Roberto Lee, Dongjae Argo, Sven de Amorim, Arthur Azevedo Georges, Aïna Linn Hritcu, Catalin Tolmach, Andrew |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_16277 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | SECOMP: Formally Secure Compilation of Compartmentalized C Programs Thibault, Jérémy Blanco, Roberto Lee, Dongjae Argo, Sven de Amorim, Arthur Azevedo Georges, Aïna Linn Hritcu, Catalin Tolmach, Andrew Programming Languages Cryptography and Security 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. |
| title | SECOMP: Formally Secure Compilation of Compartmentalized C Programs |
| topic | Programming Languages Cryptography and Security |
| url | https://arxiv.org/abs/2401.16277 |