Automated binary analysis for cryptographic code
CryptoBAP extracts protocol-relevant models from real binaries and analyzes them under explicit leakage contracts for constant-time and Spectre-style speculative observations. The pipeline lifts machine code to a verified intermediate representation, instruments it with attacker-observations, symbolically executes it to obtain observation traces, and translates those traces into Sapic+ models for automated analysis.
Key capabilities
- Verified lifting of binaries using HolBA framework
- Observation instrumentation (constant-time and speculative models) using Scam-V platform
- Crypto-aware symbolic execution of program-under-analysis
- Automatic Sapic+ model extraction for DeepSec/Tamarin/ProVerif analysis
- Concrete case studies on real, closed-source software (WhatsApp Desktop, WireGuard, Tinyssh, BAC, RPC-enc, RPC, NSL, CSur, simple Hash, and simple XOR)