CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

TL;DR

CryptoBap is a platform that automates the verification of cryptographic protocols' security properties at the binary level by translating machine code into models suitable for automated analysis, supporting real-world protocols.

Contribution

It introduces a fully automated, crypto-aware symbolic execution framework for binary cryptographic protocols, including indirect jumps and loops, and integrates with existing verification tools.

Findings

Successfully verified TinySSH and WireGuard protocols.

Automated handling of indirect jumps and loops in binary analysis.

Proved soundness of the verification approach.

Abstract

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.