The specification is not the artefact
Compilers, hand-written assembly and closed-source vendors all stand between a verified design and the code that actually ships.
Binary analysis platform
Verify the binary, not just the specification.
Formal verification of cryptographic protocols usually stops at the symbolic model — abstracting away compiled code and the microarchitecture it runs on. CryptoBAP closes that gap: it extracts protocol-relevant models directly from real binaries and analyses them under explicit leakage contracts.
Peer-reviewed at ACM CCS and IEEE CSF. Open source under AGPL-3.0.
The problem
A verified protocol can still leak.
Symbolic models describe what a protocol is supposed to do. Deployed executables do something more: they branch on secrets, index memory with them, and speculate past their own bounds. Those behaviours never appear in the specification, so a proof about the specification says nothing about them.
Microarchitecture is an attacker surface
Cache state and speculative execution turn secret-dependent control flow into observable signal, entirely outside the symbolic model.
Manual auditing does not scale
Real protocol stacks span thousands of instructions across many languages. Finding leakage by hand is neither exhaustive nor repeatable.
The approach
From machine code to a machine-checked proof.
Starting from a selected binary region, CryptoBAP runs a six-stage toolchain that ends in an off-the-shelf protocol verifier — with no manual model written at any point.
01
Reverse-engineer
Ghidra
02
Transpile to BIR
HolBA
03
Instrument
Scam-V
04
Symbolically execute
Crypto-aware engine
05
Extract the model
Sapic+
06
Verify
Tamarin · ProVerif · DeepSec
Capabilities
What the platform gives you.
Verified lifting
Machine code is transpiled into BIR, a verified binary intermediate representation, using the HolBA framework built on HOL4.
Leakage contracts
Programs are instrumented with explicit attacker-observation models — constant-time and Spectre-PHT-style speculation — via the Scam-V platform.
Crypto-aware symbolic execution
Execution resolves indirect jumps and handles bounded loops through automated loop summarisation, covering every path of the region under analysis.
Automatic model extraction
Event and observation traces are translated into Sapic+, ready for analysis without a hand-written protocol model.
Three back-end provers
The extracted model feeds Tamarin, ProVerif and DeepSec, so trace properties and equivalence properties are both in reach.
Proven sound
The translation from binary to symbolic model is accompanied by a soundness argument, so verdicts on the model carry back to the code.
Results
Findings in software people actually run.
The toolchain has been applied to closed-source desktop software, modern VPN and SSH implementations, and standardised e-passport protocols.
WhatsApp Desktop
An instruction-cache side channel enabling social-graph inference
Models of the session-management and double-ratchet components were extracted straight from the binary. Under the observation model, instruction-cache behaviour distinguishes whether a conversation with a given contact already exists.
BAC · e-passports
Known unlinkability issues reproduced under microarchitectural observations
The Basic Access Control protocol was analysed with leakage contracts enabled, reproducing unlinkability failures that a purely symbolic analysis of the specification does not surface.
Protocol properties
Forward secrecy verified, a clone attack recovered
Using the extracted models, forward secrecy was verified and a known clone attack on post-compromise security was identified under a state-cloning compromise.
Case studies
Verified or analysed with CryptoBAP:
- WhatsApp Desktop
- WireGuard
- TinySSH
- BAC (e-passport)
- RPC-enc
- RPC
- NSL
- CSur
- Simple Hash
- Simple XOR
See it run end to end.
A guided walkthrough analyses the Basic Access Control protocol, from binary region to verifier verdict.