Formal verification of cryptographic protocols typically relies on symbolic models that abstract away compiled code and microarchitectural side channels, leaving a gap between verified specifications and deployed executables. We present a toolchain that extracts protocol-relevant models from real binaries and analyzes them under explicit leakage contracts for constant-time and Spectre-PHT-style speculative observations. Starting from a selected binary region, we lift machine code to an intermediate representation, instrument it with leakage contracts, symbolically execute it to obtain event/observation traces, and translate these traces into Sapic for analysis with Tamarin, ProVerif, and DeepSec. As case studies, we extract models of WhatsApp Desktop's session-management and double-ratchet components from its binary and analyze forward secrecy and post-compromise security under a state-cloning compromise. For side-channel analysis, we study the Basic Access Control (BAC) protocol used in e-passports and WhatsApp's session establishment. Under our observation models, we identify an instruction-cache side channel in WhatsApp Desktop enabling social-graph inference, and we reproduce known unlinkability issues in BAC under microarchitectural observations.

翻译：密码协议的形式化验证通常依赖符号模型，这些模型抽象掉了编译后的代码和微架构侧信道，从而在验证规范与实际可执行代码之间留下了鸿沟。我们提出了一套工具链，能够从实际二进制文件中提取协议相关模型，并在显式泄漏合约（包括常量时间和Spectre-PHT风格的推测性观察）下对其进行分析。从选定的二进制区域出发，我们将机器码提升为中间表示，用泄漏合约对其进行插桩，通过符号执行获取事件/观察轨迹，并将这些轨迹转化为适用于Tamarin、ProVerif和DeepSec分析的Sapic语言。作为案例研究，我们从WhatsApp Desktop二进制文件中提取其会话管理和双棘轮组件的模型，并分析状态克隆妥协条件下的前向安全性与后向安全性。针对侧信道分析，我们研究了电子护照中使用的初级访问控制协议以及WhatsApp的会话建立过程。在我们的观察模型下，我们在WhatsApp Desktop中识别出可导致社交图谱推断的指令缓存侧信道，并复现了微架构观察条件下BAC协议已知的不可链接性问题。