### DY Fuzzing: Formal Dolev-Yao Models Meet Protocol Fuzz Testing

##### Abstract

Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, i.e. attacks that solely exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is today still out of reach. This leaves open whether widely used protocol implementations are secure. Unfortunately, this blind spot hides numerous attacks, notably recent logical attacks on widely used TLS implementations introduced by implementation bugs. We answer by proposing a novel and effective technique that we call DY model-guided fuzzing, which precludes logical attacks against protocol implementations. The main idea is to consider as possible test cases the set of abstract DY executions of the DY attacker, and use a mutation-based fuzzer to explore this set. The DY fuzzer concretizes each abstract execution to test it on the program under test. This approach enables reasoning at a more structural and security-related level of messages (e.g. decrypt a message and re-encrypt it with a different key) as opposed to random bit-level modifications that are much less likely to produce relevant logical adversarial behaviors. We implement a full-fledged and modular DY protocol fuzzer. We demonstrate its effectiveness by fuzzing three popular TLS implementations, resulting in the discovery of four novel vulnerabilities.

Available format(s)
Category
Cryptographic protocols
Publication info
Preprint.
Keywords
security protocolsfuzzingformal methodsTLSsymbolic verification
Contact author(s)
max @ maxammann org
lucca hirschi @ inria fr
steve kremer @ inria fr
History
2023-01-19: approved
See all versions
Short URL
https://ia.cr/2023/057

CC BY

BibTeX

@misc{cryptoeprint:2023/057,
author = {Max Ammann and Lucca Hirschi and Steve Kremer},
title = {DY Fuzzing: Formal Dolev-Yao Models Meet Protocol Fuzz Testing},
howpublished = {Cryptology ePrint Archive, Paper 2023/057},
year = {2023},
note = {\url{https://eprint.iacr.org/2023/057}},
url = {https://eprint.iacr.org/2023/057}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.