We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGuard, a modern VPN protocol.

翻译：我们提出CryptoBap，一个用于验证密码协议（ARMv8与RISC-V）机器码弱机密性与认证性的平台。首先将协议二进制代码转译为中间表示，再通过密码感知符号执行自动提取表征协议所有执行路径的模型。符号执行采用循环摘要技术解决间接跳转问题并支持有界循环，该过程完全自动化。提取的模型随后通过第三方工具链转换为ProVerif与CryptoVerif可自动验证的模型。本文证明了所提方法的正确性，并利用CryptoBap验证了从玩具示例到真实协议的多项案例研究，包括SSH实现TinySSH及现代VPN协议WireGuard。