Auswahl des Bereichs
Die Analyse beginnt bei einem gewählten Bereich der Binärdatei — dem Code, der die untersuchte Protokollrolle implementiert.
Demo
Ein geführter Durchlauf mit Basic Access Control
Basic Access Control ist das Protokoll, mit dem ein elektronischer Reisepass ein Lesegerät authentifiziert, bevor er Daten freigibt. Es ist klein genug, um es vollständig nachzuvollziehen, und interessant genug, um bekannte Datenschutzprobleme aufzuweisen. Diese Demonstration lässt CryptoBAP darüber laufen — vom Bereich der Binärdatei bis zum Urteil des Verifizierers.
Was Sie sehen werden
Dem Durchlauf folgen
Heben und Instrumentieren
Der Bereich wird nach BIR übersetzt und mit einem Leakage-Contract instrumentiert. Die Beobachtungen des Angreifers werden so Teil der Programmsemantik.
Spuren sammeln
Die symbolische Ausführung durchläuft jeden Pfad des Bereichs und zeichnet die dabei erzeugten Ereignisse und Beobachtungen auf.
Das Urteil lesen
Das extrahierte Sapic+-Modell geht an DeepSec, das über Spuräquivalenz entscheidet — jene Eigenschaft, auf der Unverkettbarkeit beruht.
Weiter
Tiefer einsteigen
Die Methodik lesen
Die vollständige Architektur, die Leakage-Contracts und der Korrektheitsbeweis dahinter.
Ergebnisse reproduzieren
Zu jedem Paper gehört ein Artefakt-Branch mit den in der Evaluation verwendeten Beispielen.
Ein reales Ziel ansehen
Dieselbe Pipeline, angewendet auf eine Closed-Source-Desktopanwendung.