Automated Side-Channel Analysis of Cryptographic Protocol Implementations

TL;DR

The paper tackles the challenge of securing cryptographic protocols not only at the specification level but also within their real-world implementations by extracting machine-code–level models and incorporating hardware leakage into the analysis. It extends CryptoBap with leakage contracts, couples binary program analysis to a Sapic^+ protocol model, and integrates with DeepSec to assess side-channel resilience, all without requiring source code. The authors demonstrate their framework by deriving the first formal model of WhatsApp from its binary, verifying forward secrecy, exposing a post-compromise security vulnerability to a clone attacker, and uncovering a novel privacy attack via instruction-cache leakage on session establishment; they also validate a known unlinkability break in BAC. The work highlights a new paradigm where side-channel considerations become a first-class part of protocol verification, with practical implications for real-world systems and a path for automated, scalable analysis across complex, closed-source applications. Overall, the methodology bridges binary-level protocol extraction with leakage-aware verification to reveal implementation-level vulnerabilities invisible to spec-based methods, enabling more robust, end-to-end security assessments of cryptographic protocols in practice.

Abstract

We extract the first formal model of WhatsApp from its implementation by combining binary-level analysis (via CryptoBap) with reverse engineering (via Ghidra) to handle this large closed-source application. Using this model, we prove forward secrecy, identify a known clone-attack against post-compromise security and discover functional gaps between WhatsApp's implementation and its specification. We further introduce a methodology to analyze cryptographic protocol implementations for their resilience to side-channel attacks. This is achieved by extending the CryptoBap framework to integrate hardware leakage contracts into the protocol model, which we then pass to the state-of-the-art protocol prover, DeepSec. This enables a detailed security analysis against both functional bugs and microarchitectural side-channel attacks. Using this methodology, we identify a privacy attack in WhatsApp that allows a side-channel attacker to learn the victim's contacts and confirm a known unlinkability attack on the BAC protocol used in electronic passports. Key contributions include (1) the first formal model of WhatsApp, extracted from its binary, (2) a framework to integrate side-channel leakage contracts into protocol models for the first time, and (3) revealing critical vulnerabilities invisible to specification-based methods.

Figures (8)

• Figure 1: $\mathbf{{\color{RoyalBlue}{BIR}}}$'s syntax
• Figure 2: A fragment of the syntax of $\mathsf{{\color{RedOrange}{\textsc{Sapic}^+}}}$ process calculus. In this figure, $e, t_1,t_2 \in \mathcal{T}$, $n \in \mathcal{N}_\texttt{priv}$, $x \in \mathcal{V}$.
• Figure 3: The Spectre V1 example instrumented via $\mathcal{M}_{\mathit{ct}}$ and $\mathcal{M}_{\mathit{spec}}$. We marked shadow observations with $\star$.
• Figure 4: Organization of our approach for cryptographic protocols side-channel analysis.
• Figure 5: Running example. The assembly snippet corresponds to the highlighted C code.

Theorems & Definitions (1)

• Definition 1: Conditional non-interference (CNI)