Die Spezifikation ist nicht das Artefakt
Compiler, handgeschriebener Assemblercode und Closed-Source-Anbieter stehen zwischen einem verifizierten Entwurf und dem Code, der tatsächlich ausgeliefert wird.
Binäranalyse-Plattform
Die Binärdatei verifizieren, nicht nur die Spezifikation.
Die formale Verifikation kryptografischer Protokolle endet meist beim symbolischen Modell — kompilierter Code und die zugrunde liegende Mikroarchitektur werden wegabstrahiert. CryptoBAP schließt diese Lücke: Die Plattform extrahiert protokollrelevante Modelle direkt aus realen Binärdateien und analysiert sie unter expliziten Leakage-Contracts.
Begutachtet auf der ACM CCS und der IEEE CSF. Open Source unter AGPL-3.0.
Das Problem
Auch ein verifiziertes Protokoll kann lecken.
Symbolische Modelle beschreiben, was ein Protokoll tun soll. Ausgelieferte Programme tun mehr: Sie verzweigen abhängig von Geheimnissen, adressieren damit den Speicher und spekulieren über ihre eigenen Grenzen hinaus. Diese Verhaltensweisen tauchen in der Spezifikation nie auf — ein Beweis über die Spezifikation sagt daher nichts über sie aus.
Mikroarchitektur ist Angriffsfläche
Cache-Zustände und spekulative Ausführung machen geheimnisabhängigen Kontrollfluss beobachtbar — vollständig außerhalb des symbolischen Modells.
Manuelle Audits skalieren nicht
Reale Protokollstacks umfassen Tausende Instruktionen über mehrere Sprachen hinweg. Leckagen von Hand zu suchen ist weder vollständig noch reproduzierbar.
Der Ansatz
Vom Maschinencode zum maschinengeprüften Beweis.
Ausgehend von einem ausgewählten Bereich der Binärdatei durchläuft CryptoBAP eine sechsstufige Werkzeugkette, an deren Ende ein etablierter Protokollverifizierer steht — ohne dass an irgendeiner Stelle ein Modell von Hand geschrieben wird.
01
Reverse Engineering
Ghidra
02
Übersetzung nach BIR
HolBA
03
Instrumentierung
Scam-V
04
Symbolische Ausführung
Krypto-bewusste Engine
05
Modellextraktion
Sapic+
06
Verifikation
Tamarin · ProVerif · DeepSec
Fähigkeiten
Was die Plattform leistet.
Verifiziertes Lifting
Maschinencode wird mit dem auf HOL4 aufbauenden HolBA-Framework nach BIR übersetzt — einer verifizierten binären Zwischendarstellung.
Leakage-Contracts
Programme werden über die Scam-V-Plattform mit expliziten Angreifer-Beobachtungsmodellen instrumentiert: Constant-Time sowie Spekulation nach Spectre-PHT.
Krypto-bewusste symbolische Ausführung
Die Ausführung löst indirekte Sprünge auf und behandelt beschränkte Schleifen durch automatische Schleifen-Summarisierung — über sämtliche Pfade des untersuchten Bereichs.
Automatische Modellextraktion
Ereignis- und Beobachtungsspuren werden nach Sapic+ übersetzt und sind ohne handgeschriebenes Protokollmodell analysierbar.
Drei Backend-Beweiser
Das extrahierte Modell speist Tamarin, ProVerif und DeepSec — damit sind sowohl Spur- als auch Äquivalenzeigenschaften erreichbar.
Nachweislich korrekt
Die Übersetzung von der Binärdatei zum symbolischen Modell ist von einem Korrektheitsbeweis begleitet: Aussagen über das Modell übertragen sich zurück auf den Code.
Ergebnisse
Befunde in Software, die wirklich eingesetzt wird.
Die Werkzeugkette wurde auf Closed-Source-Desktopsoftware, moderne VPN- und SSH-Implementierungen sowie standardisierte Reisepass-Protokolle angewendet.
WhatsApp Desktop
Ein Instruktions-Cache-Seitenkanal, der Rückschlüsse auf den Sozialgraphen erlaubt
Modelle der Sitzungsverwaltung und der Double-Ratchet-Komponenten wurden direkt aus der Binärdatei extrahiert. Unter dem Beobachtungsmodell unterscheidet das Verhalten des Instruktions-Caches, ob bereits eine Konversation mit einem bestimmten Kontakt besteht.
BAC · Elektronische Reisepässe
Bekannte Unverkettbarkeitsprobleme unter mikroarchitektureller Beobachtung reproduziert
Das Protokoll Basic Access Control wurde mit aktivierten Leakage-Contracts analysiert. Dabei traten Verletzungen der Unverkettbarkeit zutage, die eine rein symbolische Analyse der Spezifikation nicht sichtbar macht.
Protokolleigenschaften
Forward Secrecy verifiziert, Klon-Angriff nachgewiesen
Anhand der extrahierten Modelle wurde Forward Secrecy verifiziert und ein bekannter Klon-Angriff auf die Post-Compromise Security unter einem State-Cloning-Kompromiss identifiziert.
Fallstudien
Mit CryptoBAP verifiziert oder analysiert:
- WhatsApp Desktop
- WireGuard
- TinySSH
- BAC (Reisepass)
- RPC-enc
- RPC
- NSL
- CSur
- Simple Hash
- Simple XOR
Sehen Sie den vollständigen Durchlauf.
Eine geführte Demonstration analysiert das Protokoll Basic Access Control — vom Bereich der Binärdatei bis zum Urteil des Verifizierers.