CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

(2023) CryptoBap: A Binary Analysis Platform for Cryptographic Protocols.

Text cryptobap-full.pdf - Accepted Version Download (1MB)

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 WireGaurd, a modern VPN protocol.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Hamed Nemati (HM) Robert Künnemann (RK)
Conference:	CCS ACM Conference on Computer and Communications Security
Depositing User:	Hamed Nemati
Date Deposited:	29 Aug 2023 05:55
Last Modified:	18 Sep 2023 08:07
Primary Research Area:	NRA1: Trustworthy Information Processing
URI:	https://publications.cispa.saarland/id/eprint/4016

Actions

Actions (login required)

View Item