Formally Verified Security

Projekt 1: ERC SECOMP: Formally Secure Compilation

Website: https://secure-compilation.github.io

Beschreibung: In den heutigen Computersystemen gibt es zahlreiche schwerwiegende Schwachstellen auf niedriger Ebene, die es Cyber-Angreifern ermöglichen, aus der Ferne die volle Kontrolle zu erlangen. Dies geschieht zum großen Teil deshalb, weil unsere Programmiersprachen, Kompilierungsketten und Architekturen in einer Ära knapper Hardware-Ressourcen entwickelt wurden und zu oft Sicherheit gegen Effizienz eintauschen. Die Semantik von Mainstream-Niedersprachen wie C ist von Natur aus unsicher, und selbst bei sichereren Sprachen garantiert die Herstellung von Sicherheit in Bezug auf eine Semantik auf hoher Ebene nicht die Abwesenheit von Angriffen auf niedriger Ebene. Eine sichere Kompilierung unter Verwendung der grobkörnigen Schutzmechanismen, die von den gängigen Hardware-Architekturen bereitgestellt werden, wäre für die meisten praktischen Szenarien zu ineffizient.

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.

Wichtige Publikationen:

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.

Projekt 2: F*: Verification Language for Effectful Programs

Website: https://www.fstar-lang.org

Beschreibung: F* (ausgesprochen F-Stern) ist eine universell einsetzbare funktionale Programmiersprache mit Effekten, die auf die Programmverifikation abzielen. Sie vereinigt die Automatisierung eines SMT-gestützten deduktiven Verifikationswerkzeugs mit der Ausdruckskraft eines auf abhängigen Typen basierenden Prüfassistenten. Nach der Verifizierung können F*-Programme in effizienten OCaml-, F#-, C-, WASM- oder ASM-Code extrahiert werden. Dies ermöglicht die Verifizierung der funktionalen Korrektheit und Sicherheit von realistischen Anwendungen. Der wichtigste laufende Anwendungsfall von F* ist die Erstellung eines verifizierten Drop-in-Ersatzes für den gesamten HTTPS-Stack in Project Everest. Dazu gehören verifizierte Implementierungen von TLS 1.2 und 1.3 sowie der zugrunde liegenden kryptographischen Primitive.

Das Typensystem von F* umfasst abhängige Typen, monadische Effekte, Verfeinerungstypen und eine Berechnung der schwächsten Vorbedingung. Zusammen ermöglichen es diese Merkmale, präzise und kompakte Spezifikationen für Programme auszudrücken. Der F*-Typenprüfer zielt darauf ab, mit einer Kombination aus SMT-Lösungsverfahren und interaktiven Beweisen nachzuweisen, dass Programme ihre Spezifikationen erfüllen.

Wichtige Publikationen:

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.