Full Report
wolfSSL is a TLS implementation written in C. The author of this post had previously written a protocol fuzzer called tlspuffin, which they decided to target wolfSSL with since several bugs had been discovered in it this year, it had a coverage metric to ensure the tool worked as expected. The fuzzer is agnostic to any particular protocol, with SSH and other protocols supported. To fuzz wolfSSL, writing had to be created, since the tool is written in Rust. The goal of the fuzzer was to find strange states! The author claims that standard fuzzers wouldn't find this either. The first bug is within the function AddSessionToCache, which is called when a client receives a new session ticket from the server. Whenever a new session ticket arrives, the client will reuse a previously stored cache entry. The ticket is 700 bytes, meaning it is given its own heap allocation with XMALLOC. There is a strange logic bug here though. When a cache entry is used, this allocation leads to the initialization of cacheTicBuff again. But, as ticBuff is already initialized, cacheSession->ticketLenAlloc is 0. Practically, we have a confused state where a value doesn't get properly initialized. This improper initialization leads to a crash down the road because of an invalid free. To find this vulnerability, the fuzzer created a very large session token. Additionally, since this is an issue with the cache, about 30 prior connections had to be made in order to discover this vulnerability. The next vulnerability is a multi-step buffer overflow. By resuming a TLS session with two maliciously crafted hellos, the bug occurs when parsing cipher suites. The core issue of the bug is that the list of cipher suites has a maximum size, but this is not respected when copying data into the buffer. Fuzzing for memory corruption vulnerabilities isn't new. What's hard though? Formally verifying if a protocol has logic flaws in it from the specification. The author decided to tackle this problem by using the Dolev-Yao model. Messages are modeled symbolically using a term algebra. The model allows for MitM attacks and other malicious scenarios as well. The author introduces the concept of Dolev-Yao Traces in order to test out logical issues. By representing the protocol in the Dolev-Yao format, arbitrary execution flows can be emulated quickly. They give an example of a flaw in the Needham-Schroder protocol to demonstrate how this can find bugs. The author didn't find any bugs with the changes this time but is hopeful for the future. One interesting feature is finding security violations that aren't memory corruption bugs such as authentication bypasses and protocol downgrades. Overall, good post on fuzzing and a different approach to it!
Analysis Summary
# Research: Keeping the wolves out of wolfSSL
## Metadata
- Authors: Max Ammann
- Institution: Trail of Bits (with prior association to LORIA, INRIA)
- Publication: The Trail of Bits Blog
- Date: January 12, 2023
## Abstract
This research details the successful application of a novel protocol fuzzer, **tlspuffin**, against the `wolfSSL` TLS implementation. The fuzzing campaign uncovered four vulnerabilities (leading to denial of service, and potentially remote code execution in one case) by focusing on finding "strange states" within the protocol logic, an approach hypothesized to be more effective than traditional bit-level fuzzing for logic flaws. Furthermore, the author outlines a conceptual shift towards using the **Dolev-Yao model** to formally explore protocol logic flaws that are not necessarily memory corruption issues.
## Research Objective
The primary objective was twofold: first, to validate the effectiveness of the custom protocol fuzzer, `tlspuffin`, by successfully targeting the popular `wolfSSL` library and rediscovering known vulnerabilities while finding new ones; and second, to explore and demonstrate a methodology based on the Dolev-Yao model for formally checking protocol logic specifications for flaws beyond simple memory corruption.
## Methodology
### Approach
1. **Protocol Fuzzing:** Utilizing a custom fuzzer, `tlspuffin`, implemented in Rust, to generate complex sequences of protocol messages specifically designed to drive `wolfSSL` into unusual states, particularly related to session caching and session resumption parsing.
2. **Formal Verification Exploration:** Investigating the application of the Dolev-Yao symbolic model, represented via term algebra, to emulate arbitrary execution flows and test for logical security violations (e.g., authentication bypasses, protocol downgrades), using the Needham-Schroder protocol as a demonstration case.
### Dataset/Environment
The study targeted multiple versions of the **wolfSSL** library (a C-based TLS implementation). The fuzzing environment required writing Rust bindings to interface with the C library.
### Tools & Technologies
* **tlspuffin:** A protocol-agnostic fuzzer, inspired by formal protocol verification concepts, written in Rust.
* **Dolev-Yao Model:** Employed conceptually to structure the exploration of protocol logic flaws using symbolic message representation (term algebra).
## Key Findings
### Primary Results
1. **Discovery of Four New Vulnerabilities in wolfSSL:** The fuzzer successfully identified four vulnerabilities resulting in Denial of Service (DoS):
* **CVE-2022-38153 (DOSC):** Found by creating a very large session token, leading to an improper initialization state in `AddSessionToCache` (a logic flaw resulting in an invalid free after $\sim 30$ prior connections).
* **CVE-2022-38152 (DOSS):** A NULL-pointer dereference DoS crash in servers using `wolfSSL_clear` incorrectly during session resumption.
* **CVE-2022-39173 (BUF):** A multi-step buffer overflow caused by parsing cipher suites when pretending to resume a session with overlapping cipher suite lists, potentially leading to RCE on some architectures.
* **CVE-2022-42905 (HEAP):** A buffer over-read during TLS record header parsing.
2. **High Efficiency:** The fuzzer discovered the impact-heavy vulnerabilities in less than one hour on average.
3. **Successful Use as an Oracle:** The tool successfully rediscovered known vulnerabilities in `wolfSSL` from early 2022, confirming its efficacy.
### Supporting Evidence
* The context-specific nature of the found bugs (e.g., requiring $\sim 30$ prior connections for CVE-2022-38153) suggests that standard bit-level fuzzers would likely have missed these state-dependent logic flaws.
* A separate memory leak bug caused by misuse of the `wolfSSL` API was also identified and addressed via documentation updates.
### Novel Contributions
* Demonstration of the first vulnerabilities found by **tlspuffin**, proving its capability against real-world cryptographic implementations.
* Advancement towards a **Dolev-Yao model-guided fuzzer**, moving beyond memory corruption to address deeper logical flaws in protocols.
* Identification of a new class of attack traces targeting state management (like session caching) rather than simple corrupted inputs.
## Technical Details
### Vulnerability Example: CVE-2022-38153 (Improper Session Cache Initialization)
This bug occurs in `AddSessionToCache` when a client processes a new session ticket. A large (700-byte) ticket triggers a heap allocation (`XMALLOC`). Upon reusing a cache entry, the allocation mechanism re-initializes `cacheTicBuff`; however, because the ticket length (`cacheSession->ticketLenAlloc`) was set to 0 due to corrupted state from the initial allocation reuse, the subsequent logic leads to an invalid free operation, causing a crash.
### Dolev-Yao Approach
The Dolev-Yao model provides a framework where messages are treated symbolically. By leveraging "Dolev-Yao Traces," the author can rapidly emulate complex, malicious execution flows, including Man-in-the-Middle (MitM) scenarios, to test logical invariants of the protocol specification itself, independent of the C implementation details.
## Practical Implications
### For Security Practitioners
The research validates the approach of using state-aware, protocol-aware fuzzers ($\text{tlspuffin}$) to target complex cryptographic libraries like `wolfSSL`. Practitioners should be aware that logic flaws related to persistent state (e.g., session caching) require specialized testing beyond standard memory corruption fuzzing.
### For Defenders
Defenders utilizing libraries like `wolfSSL` benefit directly from the patches released for the four identified CVEs. Furthermore, the vulnerability related to using `wolfSSL_clear` instead of the proper free/new sequence highlights the importance of strictly adhering to API usage guidelines.
### For Researchers
The work demonstrates a viable path for protocol verification that bridges the gap between theoretical security models (Dolev-Yao) and practical, automated testing (fuzzing), suggesting avenues for future research into verifying properties like authentication correctness automatically.
## Limitations
The success of the Dolev-Yao exploration shown was conceptual/demonstrative (using Needham-Schroder), and the primary findings came from the functional fuzzing campaign against `wolfSSL`. The paper does not confirm that the Dolev-Yao methodology *itself* found bugs in `wolfSSL` during this cycle, but rather that the fuzzer succeeded where simpler methods might fail.
## Comparison to Prior Work
This work explicitly builds upon prior formal verification techniques (Dolev-Yao) but implements them in a novel, automated **fuzzing** context rather than purely static analysis. This contrasts with classical bit-level fuzzers, which struggle to generate the complex message sequences necessary to reach the deeply nested logic flaws discovered in `wolfSSL`.
## Future Work
The author expresses intent to extend `tlspuffin` to support additional critical protocols such as **QUIC, OpenVPN, and WireGuard**, further proving the tool's protocol-agnostic design. Further work is planned to mature the Dolev-Yao integration to automatically detect non-memory corruption security violations like authentication bypasses.
## References
* CVE-2022-38152, CVE-2022-38153, CVE-2022-39173, CVE-2022-42905
* Prior known vulnerabilities in wolfSSL (CVE-2022-25640, CVE-2022-25638)
* The Dolev–Yao model (Wikipedia reference)