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!