Formally Verified Security
- Catalin Hritcu (Tenured Faculty)
- Carmine Abate (PhD Student)
- Jérémy Thibault (PhD Student)
- Roberto Blanco (Postdoctoral Researcher)
- Adrien Durier (Postdoctoral Researcher)
- Théo Winterhalter (Postdoctoral Researcher)
- Cezar Constantin Andrici (Research Engineer / Intern)
Dieses Projekt zielt darauf ab, aufkommende Hardware-Fähigkeiten für einen feinkörnigen Schutz zu nutzen, um die ersten effizienten sicheren Kompilierungsketten für realistische Low-Level-Programmiersprachen (die Sprache C und Low* eine sichere Teilmenge von C, die zur Verifizierung in F* eingebettet ist) zu erstellen. Diese Kompilierungsketten bieten eine sichere Semantik für alle Programme und stellen sicher, dass High-Level-Abstraktionen nicht verletzt werden können, selbst wenn sie mit nicht vertrauenswürdigem Low-Level-Code interagieren. Um dieses Sicherheitsniveau ohne Effizienzeinbußen zu erreichen, zielen unsere sicheren Kompilierungsketten auf eine getaggte Architektur ab, die jedem Wort ein Metadaten-Tag zuordnet und Tags nach softwaredefinierten Regeln effizient propagiert und überprüft. Wir verwenden eigentumsbasierte Tests und formale Verifizierung, um ein hohes Maß an Vertrauen zu schaffen, dass unsere Kompilierungsketten tatsächlich sicher sind. Formal konstruieren wir in Coq maschinengeprüfte Beweise für verschiedene neue Sicherheitskriterien, die als die Erhaltung von Eigentumsklassen auch gegen einen kontradiktorischen Kontext definiert sind. Diese strengen Kriterien ergänzen die Compiler-Korrektheit und stellen sicher, dass kein Maschinencode-Angreifer sicher kompilierten Komponenten mehr Schaden zufügen kann als eine Komponente bereits in Bezug auf eine sichere Semantik auf Quellcode-Ebene.
- Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault. Trace-Relating Compiler Correctness and Secure Compilation. arXiv:1907.05320. July 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.
- 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.
- Dijkstra Monads for All (Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019.
- Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy), In PACMPL, volume 2, 2018.
- Dependent Types and Multi-Monadic Effects in F* (Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, Santiago Zanella-Béguelin), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016.