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.

翻译：我们通过结合二进制级分析（经由CryptoBap）与逆向工程（经由Ghidra）处理这一大型闭源应用程序，首次从WhatsApp的实现中提取出其形式化模型。利用该模型，我们证明了前向保密性，识别出针对后妥协安全性的已知克隆攻击，并发现了WhatsApp实现与其规范之间的功能差距。我们进一步提出了一种分析密码协议实现以评估其抵抗侧信道攻击能力的方法论。这是通过扩展CryptoBap框架，将硬件泄漏契约集成到协议模型中实现的，随后我们将该模型传递给最先进的协议证明器DeepSec。这使得能够针对功能缺陷和微架构侧信道攻击进行详细的安全分析。应用此方法论，我们在WhatsApp中发现了一种隐私攻击，允许侧信道攻击者获取受害者的联系人信息，并证实了电子护照中使用的BAC协议上已知的不可链接性攻击。关键贡献包括：（1）首次从二进制文件中提取的WhatsApp形式化模型；（2）首次将侧信道泄漏契约集成到协议模型中的框架；（3）揭示了基于规范方法无法发现的关键漏洞。