How it works
CryptoBAP is an end-to-end toolchain. It lifts machine code to an intermediate representation, instruments it with leakage contracts, symbolically executes it to obtain event and observation traces, and translates those traces into Sapic+ for analysis with Tamarin, ProVerif and DeepSec.
Pipeline
Each stage has a defined input and output, so the chain can be inspected — or re-targeted — at any point.
The selected region of the target binary is disassembled and recovered as assembly code, including for closed-source executables.
Assembly is lifted into BIR, a verified binary intermediate representation, giving a machine-checked semantics for the code under analysis.
The BIR program is instrumented with a leakage contract that makes the attacker’s observations explicit — constant-time, or Spectre-PHT-style speculation.
The instrumented program is executed symbolically to collect event and observation traces, resolving indirect jumps and summarising bounded loops.
Traces are simplified using live-variable analysis and translated into a Sapic+ process, a model of every execution path through the region.
The resulting model is discharged to established protocol verifiers, covering both trace properties and observational equivalence.
Leakage contracts
A leakage contract states exactly what an attacker observes while the program runs. Changing the contract changes the threat model without changing the binary or the protocol model.
The attacker observes the sequence of control-flow decisions and the addresses of memory accesses. This captures classic cache and branch-timing channels: any secret-dependent branch or secret-derived address becomes visible.
The attacker additionally observes execution along mispredicted conditional branches. This captures speculative leakage, where the transient path touches data the architectural path never would.
Back ends
Unbounded verification of trace properties, with support for stateful protocols and equational theories.
Automated analysis in the applied pi-calculus for secrecy, authentication and observational equivalence.
Decision of trace equivalence for a bounded number of sessions — the tool of choice for unlinkability and privacy.
Foundations
Real protocol stacks are not written in a single language. CryptoBAP builds on a symbolic execution semantics that supports parallel composition of labelled transition systems over different atomic types. By treating the Dolev–Yao model itself as a symbolic abstraction, the approach removes the need to translate between bitstrings and Dolev–Yao terms at every language boundary.
Evaluation
An instruction-cache side channel in WhatsApp Desktop enabling social-graph inference.
Unlinkability issues in the BAC e-passport protocol reproduced under microarchitectural observations.
Forward secrecy verified, and a known clone attack on post-compromise security identified, from models extracted out of the binary.
Security properties verified for WireGuard, TinySSH, RPC-enc, RPC, NSL, CSur, simple Hash and simple XOR.
The CCS 2023 platform targets ARMv8 and RISC-V machine code and verifies weak secrecy and authentication; the CCS 2026 work adds leakage contracts and side-channel analysis.