Paper 2023/057

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

Max Ammann, Independent Researcher, Trail of Bits
Lucca Hirschi, Inria Nancy Grand-Est, Université de Lorraine, France, LORIA
Steve Kremer, Inria Nancy Grand-Est, Université de Lorraine, France, LORIA
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, e.g. attacks that exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, formally define and 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 such implementations are secure. Unfortunately, this blind spot hides numerous attacks, such as 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 novel 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 represented as formal terms (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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Minor revision. IEEE Security & Privacy 2024
Keywords
security protocolsfuzzingformal methodsTLSsymbolic verification
Contact author(s)
max @ maxammann org
lucca hirschi @ inria fr
steve kremer @ inria fr
History
2023-12-01: last of 2 revisions
2023-01-18: received
See all versions
Short URL
https://ia.cr/2023/057
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/057,
      author = {Max Ammann and Lucca Hirschi and Steve Kremer},
      title = {DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic 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.