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）的多个案例。