A binary analysis platform for cryptographic protocols

Abstract

This thesis advances the formal verification of cryptographic protocol implementations at the binary level by tackling issues related to low-level programming languages, multi-language interactions, and microarchitectural side-channel vulnerabilities. we present cryptobap, a framework for verifying security properties directly on the machine code of protocol implementations, supporting both armv8 and risc-v architectures. cryptobap performs crypto-aware symbolic execution on binary code to extract high-level models that represent all possible execution paths, handling complex control-flow constructs like indirect jumps and bounded loops through fully automated loop summarization. these models are then verified using protocol verification tools such as proverif, tamarin, cryptoverif, and deepsec. to support verification across systems built from multiple programming languages, we introduce a symbolic semantics that unifies languages operating on different atomic types. this semantics enables the modular composition of labeled transition systems and uses dolev-yao terms as symbolic abstractions of base-level types like bitstrings, allowing components to interoperate without the need for explicit translation layers. this approach makes it possible to analyze and verify security properties in complex, heterogeneous software systems. we also extend cryptobap to assess resilience against side-channel attacks by incorporating leakage models into the symbolic analysis. this allows us to reason not only about functional correctness but also about side-channel resistance. our methodology has been applied to a range of case studies, including the basic access control protocol utilized in e-passports, tinyssh, an implementation of ssh, wireguard, a modern vpn protocol, and whatsapp, the most popular messaging app. using this methodology, on whatsapp desktop, we identified a privacy attack that allows a side-channel attacker to learn the victim’s contacts, a post-compromise security violation by a clone attacker, and functional gaps between its implementation and specification.

In dieser Arbeit widmen wir uns der formalen Verifizierung von Implementierungen kryptografischer Protokolle auf Binärcode-Ebene. Dabei adressieren wir Herausforderungen im Zusammenhang mit Low-Level-Programmiersprachen, der Interaktion zwischen Sprachen sowie mikroarchitekturellen Seitenkanalangriffen. Wir stellen CryptoBap vor – ein Framework zur Verifizierung von Sicherheitseigenschaften direkt auf dem Maschinencode. CryptoBap unterstützt ARMv8 und RISCV. Es führt eine kryptobewusste symbolische Ausführung auf Binärcode-Ebene durch, um Modelle zu extrahieren, die alle Ausführungspfade abbilden. Dabei werden auch komplexe Kontrollflusskonstrukte wie indirekte Sprünge und begrenzte Schleifen durch eine vollständig automatisierte Schleifenzusammenfassung behandelt. Diese Modelle werden anschließend mit ProVerif, Tamarin, CryptoVerif und DeepSec überprüft. Um die Verifizierung über Systeme hinweg zu ermöglichen, die aus mehreren Sprachen bestehen, führen wir eine symbolische Semantik ein, die Sprachen vereinheitlicht, die auf unterschiedlichen atomaren Typen operieren. Sie ermöglicht die modulare Zusammensetzung von beschrifteten Übergangssystemen und verwendet Dolev- Yao-Terme als symbolische Abstraktionen von Basistypen wie Bitstrings. So können Komponenten ohne Übersetzungsschichten zusammenarbeiten, was die Analyse und Verifizierung in heterogene Softwaresysteme erlaubt. Zur Bewertung der Widerstandsfähigkeit gegen Seitenkanalangriffe erweitern wir CryptoBap um Leckagemodelle, die in die symbolische Analyse integriert werden. Damit können wir sowohl funktionale Korrektheit als auch Resistenz gegenüber Seitenkanalangriffen bewerten. Unsere Methodik haben wir auf mehrere Fallstudien angewandt: das Basic Access Control-Protokoll in elektronischen Reisepässen, TinySSH (eine SSH-Implementierung), WireGuard (ein modernes VPN-Protokoll) und WhatsApp. Dabei haben wir bei Whats- App Desktop einen Datenschutzangriff identifiziert, bei dem ein Seitenkanalangreifer die Kontakte des Opfers ausspähen kann. Außerdem fanden wir eine Sicherheitsverletzung nach einer Kompromittierung durch einen Klonangriff sowie funktionale Diskrepanzen zwischen Implementierung und Spezifikation.