Reactive System Fuzzing

Abstract:

Reactive systems, such as communication protocols, that continuously interact with execution environments, form the foundation of critical software infrastructure. Any bugs or vulnerabilities within these systems may lead to severe consequences. Reactive systems, therefore, must be continuously and automatically secured against vulnerabilities. Unlike transformational systems such as compilers and parsers, which have been the subject of extensive research, suitable techniques for automated testing of reactive systems are still severely lacking. Developers of reactive systems traditionally rely on model checking for validation. Although model checking is a verification technique, it is primarily used for bug finding in practice. While effective, the scalability and usability problems of model checking limit its widespread adoption.

In this thesis, we develop automated testing techniques that are effective, scalable, and usable for finding bugs in reactive systems. Greybox fuzzing, known for its low barrier to entry, is a promising technique in this regard. Unfortunately, greybox fuzzing is traditionally designed to test transformational systems automatically. In testing reactive systems, the key challenge lies in their statefulness: sending the same input messages twice might yield a different response every time. To address this, we develop a new technical method that synergizes the concepts of model checking with advances in greybox fuzzing. Our technical method seeks to achieve bug-finding capabilities close to model checking while still maintaining the usability and scalability of greybox fuzzing.

We have used this method to address the statefulness problem in different contexts. Specifically, we advance greybox fuzzing to detect violations of stateful properties, those expressed in Linear-time Temporal Logic (LTL), going far beyond simple oracles such as crashes and memory safety errors. Furthermore, we leverage the capability of Large Language Models (LLMs) to address the long-standing challenge of state identification while testing protocol implementations. To handle distributed systems, we introduce a greybox-fuzzing technique, where we leverage Lamport timelines to visualize the states of distributed systems and build a reactive fuzzer to adaptively inject inputs based on observed states. To account for the complex execution environments of reactive systems, we develop an automated method via greybox fuzzing to capture the effects of different environmental states, offering a practical alternative to traditional environment modeling.

The body of work represents a practical advance in automated validation of reactive systems and a conceptual advance in greybox fuzzing. Until now, our released open-sourced tools have discovered nearly 200 vulnerabilities in widely-used reactive systems, more than 50 of which are security-critical vulnerabilities registered as CVEs at the US National Vulnerability Database. This makes a step forward toward more secure and reliable reactive systems.