Summary
CryptoBAP provides an end-to-end toolchain that extracts protocol-relevant models from real binaries and analyzes them under explicit leakage contracts (constant-time and Spectre-style speculative observations). The pipeline lifts machine code to an intermediate representation, instruments it with attacker observations, symbolically executes it to obtain observation traces, and translates these traces into Sapic+ models for analysis with Tamarin, ProVerif, and DeepSec.
Architecture Overview
The pipeline:
- → Reverse-engineer binaries with Ghidra
- → Transpile the reverse-engineered assembly code to BIR using HolBA
- → Instrument the BIR program with leakage contracts utilizing Scam-V
- → Symbolically execute the instrumented program to collect traces and observations
- → Simplify and extract Sapic+ models
- → Analyze the resulting Sapic+ models with DeepSec/Tamarin/ProVerif
Evaluation Highlights
Case studies reproduced privacy and security issues in deployed software. Highlights include:
- Identified an instruction-cache side channel in WhatsApp Desktop enabling social-graph inference.
- Reproduced unlinkability issues in the BAC e-passport protocol under microarchitectural observations.
- Analyzed protocol-level properties, i.e., verified forward secrecy and identified a known clone attack on post-compromise security, using extracted models.
- Verified security properties for cryptographic protocol implementations such as WireGuard, Tinyssh, RPC-enc, RPC, NSL, CSur, simple Hash, and simple XOR.