Funktionsweise
CryptoBAP ist eine durchgängige Werkzeugkette. Sie hebt Maschinencode in eine Zwischendarstellung, instrumentiert ihn mit Leakage-Contracts, führt ihn symbolisch aus, um Ereignis- und Beobachtungsspuren zu gewinnen, und übersetzt diese Spuren nach Sapic+ zur Analyse mit Tamarin, ProVerif und DeepSec.
Pipeline
Jede Stufe hat definierte Ein- und Ausgaben. Die Kette lässt sich daher an jeder Stelle prüfen — oder auf ein anderes Ziel umstellen.
Der ausgewählte Bereich der Zielbinärdatei wird disassembliert und als Assemblercode rekonstruiert — auch bei Closed-Source-Programmen.
Der Assemblercode wird nach BIR gehoben, einer verifizierten binären Zwischendarstellung. Damit erhält der untersuchte Code eine maschinengeprüfte Semantik.
Das BIR-Programm wird mit einem Leakage-Contract instrumentiert, der die Beobachtungen des Angreifers explizit macht — Constant-Time oder Spekulation nach Spectre-PHT.
Das instrumentierte Programm wird symbolisch ausgeführt, um Ereignis- und Beobachtungsspuren zu sammeln. Indirekte Sprünge werden aufgelöst, beschränkte Schleifen zusammengefasst.
Die Spuren werden mittels Lebendigkeitsanalyse vereinfacht und in einen Sapic+-Prozess übersetzt — ein Modell sämtlicher Ausführungspfade des Bereichs.
Das entstandene Modell wird an etablierte Protokollverifizierer übergeben, die Spureigenschaften ebenso abdecken wie beobachtbare Äquivalenz.
Leakage-Contracts
Ein Leakage-Contract legt genau fest, was ein Angreifer während der Programmausführung beobachtet. Ein Wechsel des Contracts verändert das Bedrohungsmodell, ohne die Binärdatei oder das Protokollmodell anzutasten.
Der Angreifer beobachtet die Folge der Kontrollflussentscheidungen sowie die Adressen der Speicherzugriffe. Damit sind klassische Cache- und Branch-Timing-Kanäle erfasst: Jede geheimnisabhängige Verzweigung und jede aus einem Geheimnis abgeleitete Adresse wird sichtbar.
Zusätzlich beobachtet der Angreifer die Ausführung entlang fehlspekulierter bedingter Sprünge. Damit ist spekulative Leckage erfasst, bei der der transiente Pfad Daten berührt, die der architekturale Pfad nie anfassen würde.
Backends
Unbeschränkte Verifikation von Spureigenschaften, mit Unterstützung für zustandsbehaftete Protokolle und Gleichungstheorien.
Automatisierte Analyse im angewandten Pi-Kalkül für Geheimhaltung, Authentifizierung und beobachtbare Äquivalenz.
Entscheidung der Spuräquivalenz für eine beschränkte Anzahl von Sitzungen — das Werkzeug der Wahl für Unverkettbarkeit und Privatsphäre.
Grundlagen
Reale Protokollstacks sind nicht in einer einzigen Sprache geschrieben. CryptoBAP baut auf einer symbolischen Ausführungssemantik auf, die die Parallelkomposition beschrifteter Transitionssysteme über verschiedene atomare Typen hinweg erlaubt. Indem das Dolev-Yao-Modell selbst als symbolische Abstraktion behandelt wird, entfällt die Übersetzung zwischen Bitstrings und Dolev-Yao-Termen an jeder Sprachgrenze.
Evaluation
Ein Instruktions-Cache-Seitenkanal in WhatsApp Desktop, der Rückschlüsse auf den Sozialgraphen ermöglicht.
Unter mikroarchitektureller Beobachtung reproduzierte Unverkettbarkeitsprobleme im Reisepass-Protokoll BAC.
Verifizierte Forward Secrecy sowie ein identifizierter bekannter Klon-Angriff auf die Post-Compromise Security — auf Basis von Modellen, die aus der Binärdatei extrahiert wurden.
Verifizierte Sicherheitseigenschaften für WireGuard, TinySSH, RPC-enc, RPC, NSL, CSur, Simple Hash und Simple XOR.
Die Plattform aus CCS 2023 adressiert ARMv8- und RISC-V-Maschinencode und verifiziert schwache Geheimhaltung und Authentifizierung; die Arbeit für CCS 2026 ergänzt Leakage-Contracts und Seitenkanalanalyse.