Efficient Formally Secure Compilation to a Tagged Architecture
SECOMP is a research project aimed at building the first efficient formally secure compilation chains for realistic programming languages (see project description below). The project encompasses a core team at MPI-SP and several external collaborators. Cătălin Hriţcu and the core team at MPI-SP were generously funded for 5 years (until the end of 2021) by an ERC Starting Grant.
Team
The core SECOMP team is located at MPI-SP in Bochum, Germany, and currently includes Cătălin Hriţcu, several students, and one postdoc. The project also includes excellent external collaborators and we are looking forward to work with additional world-class researchers with an interest in secure compilation (see the PriSC workshop @ POPL and a series of Dagstuhl Seminars on secure compilation (2018, 2021)).
Core team at MPI-SP as of end of 2021
- Cătălin Hriţcu (SECOMP PI, Tenured Faculty)
- Carmine Abate (PhD Student)
- Cezar-Constantin Andrici (PhD Student)
- Jérémy Thibault (PhD Student)
- Roberto Blanco (PostDoc)
- Théo Winterhalter (PostDoc)
External collaborators
- Arthur Azevedo de Amorim (PostDoc, Carnegie Mellon University)
- Deepak Garg (Tenured Faculty, MPI-SWS)
- Éric Tanter (Visiting Professor, University of Chile)
- Andrew Tolmach (Professor, Portland State University)
- Benjamin C. Pierce (Professor, University of Pennsylvania)
- Akram El-Korashy (PhD Student, MPI-SWS)
- Marco Patrignani (Visiting Assistant Professor, Stanford University and CISPA)
- Nikhil Swamy (Senior Researcher, Microsoft Research)
- Ștefan Ciobâcă (Associate Professor, University of Iași)
Past members
- Adrien Durier (PostDoc at Inria Paris and MPI-SP)
- Kenji Maillard (PhD Student)
- Danel Ahman (PostDoc)
- Marco Stronati (PostDoc)
- Guido Martínez (PhD Student at CIFASIS-CONICET and UNR)
- Guglielmo Fachini (Research Engineer)
- Yannis Juglaret (Student at Inria and Paris 7)
- Boris Eng (Research Intern at Inria, undergraduate student at Paris 8)
- Ana Nora Evans (Visiting Researcher at Inria, PhD Student at University of Virginia)
- Florian Groult (Research Intern/Engineer, Orléans University)
- Victor Dumitrescu (Research Engineer)
- Théo Laurent (Research Intern at Inria, ENS Paris)
- Clément Pit-Claudel (Research Intern at Inria, MIT)
- Amal Ahmed (Visiting Professor at Inria, Northeastern University)
- William J. Bowman (Research Intern at Inria, Northeastern University)
- Aaron Weiss (Visiting Researcher at Inria, Northeastern University)
- Jake Silverman (Visiting Researcher at Inria, Cornell University)
- Elizabeth Labrada (Research Intern, University of Chile)
SECOMP Project
Description
Severe low-level vulnerabilities abound in today’s computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilation chains, and hardware architectures were designed in an era of scarce hardware resources and too often trade off security for efficiency. Mainstream programming languages like C are currently insecure, since any undefined behavior (e.g., a buffer overflow) can compromise the security of the whole application. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient and inconvenient for most practical scenarios.
This line of research is aimed at leveraging emerging hardware capabilities for fine-grained compartmentalization and memory safety to build the first efficient secure compilation chains for realistic programming languages, in particular for C. Such compilation chains enforce that compartmentalized applications are compiled securely, so every component in C is protected from other C components compromised by undefined behavior. To achieve such security without sacrificing efficiency, we compile to a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules.
At the conclusion of the project, we have achieved and in some ways exceeded our most important objective. We have built a secure compilation chain for C components based on the CompCert formally verified C compiler, as well as several smaller prototype compilation chains targeting a tagged architecture and software-fault isolation. We used a combination of machine-checked proofs and property-based testing in the Coq proof assistant to provide high confidence that our compilation chains achieve an unprecedented level of security.
Github Repos
- https://github.com/secure-compilation/CompCert
- https://github.com/secure-compilation/when-good-components-go-bad
- https://github.com/secure-compilation/when-good-components-go-bad/tree/memory-sharing
- https://github.com/secure-compilation/exploring-robust-property-preservation
- https://github.com/secure-compilation/different_traces
- https://github.com/FStarLang/FStar
- https://github.com/SSProve/ssprove
- https://github.com/QuickChick
- https://github.com/arthuraa/memory-safe-language
Chatting
Most Relevant Publications
Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Cătălin Hriţcu, and Andrew Tolmach. SECOMP: Formally Secure Compilation of Compartmentalized C Programs. Draft, January 2024.
- Coq development
- An extended abstract about this work was presented at PriSC’23
Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, and Théo Winterhalter. Securing Verified IO Programs Against Unverified Code in F*. PACMPL, 8(POPL):74:1–74:34, January 2024.
- F* development
- An extended abstract about this work was presented at PriSC’23
Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce, and Andrew Tolmach. Formalizing Stack Safety as a Security Property. In 36th IEEE Computer Security Foundations Symposium (CSF), July 2023.
Carmine Abate. A Formal Framework for Correct and Secure Compilation PhD Thesis, Ruhr University Bochum, October 2022.
Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Deepak Garg, and Cătălin Hriţcu. SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation. In 35th IEEE Computer Security Foundations Symposium (CSF), August 2022.
Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault. An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation. ACM Transactions on Programming Languages and Systems (TOPLAS). Volume 43, Issue 4, pages 1-48. ACM, December 2021.
- Coq development
- A short version appeared at In 29th European Symposium on Programming (ESOP) and was Nominated for EATCS Award for the best ETAPS 2020 paper in theoretical computer science.
Carmine Abate, Matteo Busi, and Stelios Tsampas. Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly. In 19th Asian Symposium on Programming Languages and Systems (APLAS). October 2021.
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hriţcu, Kenji Maillard, and Bas Spitters. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. In 34th IEEE Computer Security Foundations Symposium (CSF), pages 608–622. June 2021. Distinguished Paper Award.
Cătălin Hriţcu. The Quest for Formally Secure Compartmentalizing Compilation Habilitation Thesis, ENS Paris, January 2019.
Carmine Abate, Roberto Blanco, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, and Jérémy Thibault. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 32nd IEEE Computer Security Foundations Symposium (CSF), June 2019. Distinguished Paper Award.
- Coq development
- A previous extended abstract was called Robust hyperproperty preservation for secure compilation
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hriţcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. In 25th ACM Conference on Computer and Communications Security (CCS), October 2018.
- Coq proofs
- A previous extended abstract was called Formally secure compilation of unsafe low-level components
Arthur Azevedo de Amorim, Cătălin Hriţcu, and Benjamin C. Pierce. The Meaning of Memory Safety. In 7th International Conference on Principles of Security and Trust (POST), pages 79–105, April 2018.
Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In 29th IEEE Symposium on Computer Security Foundations (CSF), pages 45-60. IEEE Computer Society Press, July 2016.
Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. Technical Report, arXiv:1510.00697, October 2015.
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 36th IEEE Symposium on Security and Privacy (Oakland S&P), pages 813-830. IEEE Computer Society, May 2015.
Udit Dhawan, Cătălin Hriţcu, Nikos Vasilakis, Raphael Rubin, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce, and André DeHon. Architectural Support for Software-Defined Metadata Processing. In 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 487-502. ACM, March 2015.
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. Journal of Computer Security (JCS); Special Issue on Verified Information Flow Security, 24(6):689–734, December 2016. (arXiv:1509.06503; supersedes POPL 2014 paper with the same name.)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Cătălin Hriţcu, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Verified Low-Level Programming Embedded in F*. In 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), PACMPL, 1(ICFP):17:1–17:29, September 2017.
Talks on SECOMP
- CASA Summer School 2023: slides (2023-08-14)
- MPI-SP Scientific Advisory Board visit: slides (2023-05-11)
- MPI-SWS Research Symposium: slides (2023-03-10)
- Dagstuhl Seminar 21481 on Secure Compilation: slides (2021-12-01)
- Invited Talk at HotSpot Workshop: slides and video (2020-09-07)
- CS @ Max Planck Open House: slides and video (2020-04-03)
- Formal Methods Working Group of GDR Security: slides (2020-01-30)
- Chalmers Security Seminar: slides (2019-12-05)
- EPFL IC Colloquium: slides (2019-09-26)
- CSF 2019: slides (2019-06-27)
- MPI-SWS, Saarbrücken: slides (2019-05-23)
- CASA-MPI Distinguished Lecture at Ruhr University Bochm: slides (2019-05-13)
- Habilitation defense, Inria Paris: slides (2019-01-29)
- PriSC @ POPL’19: slides (2019-01-13)
- CCS 2018: slides and video (2018-10-18)
- Working Formal Methods Symposium (FROM 2018): slides (2018-06-20)
- Dagstuhl Seminar on Secure Compilation: slides1 slides2 (2018-05-14)
- IRIF, Paris 7: slides (2018-02-26)
- SoSySec seminar: Software and Systems Security at IRISA: slides; video (2018-02-05)
- PriSC’18 in LA: slides (2018-01-13)
- Infoiasi: slides (2017-12-18)
- ESOP PC Workshop: slides (2017-12-15)
- Université Clermont Auvergne: slides and video (2017-04-06)
- LRI VALS seminar at University Paris-Sud: slides (2017-03-17)
- CEA List seminar: slides (2016-12-13)
- Microsoft Research Redmond security seminar: slides (2016-11-03)
- Inria Gallium seminar: slides (2016-09-02)
- Secure compilation meeting (informal) at Inria Paris: slides (2016-08-17)
- ERC Starting Grant interview: slides (2016-05-31)
- Inria Prosecco Seminar: slides (2016-03-02)
- MPI-SWS Colloquium: slides (2016-02-22)
Course on Secure Compilation
- Formally Secure Compartmentalizing Compilation course at International School on Foundations of Security Analysis and Design (FOSAD) in Bertinoro, Italy (2018-08-27)
Related Projects
Micro-Policies was a project aimed at showing how a rich set of micro-policies – instruction-level security monitoring mechanisms based on fine-grained metadata tags – can be described as instances of a common dynamic monitoring framework, formalized and reasoned about with unified verification tools, and efficiently implemented using programmable metadata-propagation hardware. This project was a collaboration between Inria Paris, University of Pennsylvania, MIT, Portland State University, and Draper Labs (who have built a RISC-V processor extended with support for micro-policies). Micro-policies will be the main enabler for efficient secure compilation in SECOMP.
CRASH/SAFE was a DARPA-funded project (2011-2014) that has undertaken the clean-slate co-design of a secure network host including novel hardware, operating system, programming language, and the systematic testing and verification of key components. This large effort (≈40 people team) brought together academia (University of Pennsylvania, Harvard University, Northeastern University) and industry (BAE Systems). The hardware mechanism we use for enforcing micro-policies originated in CRASH/SAFE, where it was mainly used for information-flow control.