The puffin fuzzer is the reference implementation for the Dolev-Yao fuzzing approach (eprint publicly accessible here). It aims at fuzzing cryptographic protocol implementations. For now, it is shipped with harnesses for several TLS implementations (OpenSSL, BoringSSL, LibreSSL, and wolfSSL) and preliminary versions of a harness for OpenSSH. We built puffin so that new protocols and protocol implementations can be added. Internally, puffin uses the library LibAFL to drive the fuzzing loop.

We sometimes use tlspuffin instead of puffin to name the fuzzer and this project. This is because the first protocol we implemented was TLS. However, puffin and DY fuzzing in general are not limited to the TLS protocol.

Please refer to the up-to-date user manual. We also provide a quickstart guide for a fast setup.

Licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or https://opensource.org/blog/license/mit)

at your option. Note that tlspuffin also contains code/modification from external projects. See THIRD_PARTY for more details.

We welcome any external contributions through pull requests, see for example the list of "good first issues".
Please refer to the up-to-date developer documentation. Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and 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 (shown in green in the Figure below), 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 are concerned with finding implementation-level logical attacks in large cryptographic protocol code bases. For this, we build on fuzz testing. However, state-of-the-art fuzzers (shown on the left in the Figure) cannot capture the class of logical attacks for two main reasons. First, they fail to effectively capture the DY attacker, particularly the ability of structural modifications on the term representation of messages in DY models (e.g., re-signing a message with some adversarial-controlled key), a prerequisite to capture logical attacks. We emphasize that logical attacks may trigger protocol or memory vulnerabilities. Second, they cannot detect protocol vulnerabilities, which are security violations at the protocol level, e.g., for the attacks that trigger protocol vulnerabilities, which are not memory-related, such as an authentication bypass.

We answer in [1] by proposing a novel and effective technique called 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 (shown in the middle of the Figure). 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) instead of random bit-level modifications that are much less likely to produce relevant logical adversarial behaviors.

tlspuffin is our reference implementation of such a DY fuzzer. It is built modularly so that new protocols and Programs Under Test (PUTs) can be integrated and tested. We have already integrated the TLS protocol and the OpenSSL, BoringSSL, WolfSSL, and LibreSSL PUTs. tlspuffin has already found 8 CVEs (see table below), including five new ones (including a critical one) that were all acknowledged and patched. Interestingly and as a witness to the claims above, those five newly found bugs are not currently found by state-of-the-art fuzzers [1].

Some features:

• Uses the LibAFL fuzzing framework
• Fuzzer which is inspired by the Dolev-Yao models used in protocol verification
• Domain specific mutators for Protocol Fuzzing!
• Supported Libraries Under Test:
  • OpenSSL 1.0.1f, 1.0.2u, 1.1.1k
  • LibreSSL 3.3.3
  • wolfSSL 5.1.0 - 5.4.0
  • BoringSSL (last commit tested 368d0d87d0bd00f8227f74ce18e8e4384eaf6afa)
    • Disclaimer : there is a bug will building in debug mode with asan (set lto=true in Cargo.toml to circumvent)
• Reproducible for each LUT. We use sources from fresh git clone of vendor libraries.
• 70% Test Coverage
• Written in Rust!

• Tom Gouville - Loria, Inria
• Lucca Hirschi - Loria, Inria
• Steve Kremer - Loria, Inria
• Michael Mera - Loria, Inria
• Max Ammann

This project is partially funded by the ANR JCJC project ProtoFuzz. We are still looking to hire motivated students/postdocs/engineers in Nancy, France as part of this project.

[1] M. Ammann, L. Hirschi and S. Kremer, "DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing," in 2024 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2024 pp. 99-99.

[2] DY Fuzzing Poster