FuzzM (Fuzzing with Models) is a gray box model-based fuzzing framework that employs Lustre as a modeling and specification language and leverages the JKind model checker as a constraint solver.
Fuzzing is a form of robustness testing in which random, invalid or unusual inputs are applied to a system while monitoring its overall health. Model-based fuzzing is a fuzzing technique that employs a mathematical model of system behavior to guide the fuzzing process and explore behaviors that would otherwise be difficult to reach by chance. Whereas traditional fuzzing frameworks generate tests randomly, our model-based framework deduces tests from a behavioral model using a constraint solver.
The FuzzM framework employs JKind to produce constraint solutions (counterexamples) that exhibit potentially hard to reach model behaviors. Fuzz tests are generated by first generalizing constraint solutions and then sampling the generalized solution space. This generalization/sampling paradigm decouples the solver from the test generation process and provides the bandwidth needed to explore the state space around constraint solutions in search of proximate vulnerabilities in the target system. We say that the constraint solver is used to target known behaviors and the generalizer is used to fuzz for unknown behaviors. This configuration transforms JKind solution streams on the order of 1 vector per second into fuzzing streams on the order of 2000 test vectors per second.
Fuzzing a target system with FuzzM requires the development of a Lustre model and a relay. The model defines the inputs to the system and specifies behaviors, in the form of properties, that the fuzzer is expected to attack. All of the vectors generated by the framework should satisfy at least one of the specified properties. The relay is responsible for interfacing with the target and for re-formatting FuzzM test vectors so that they can be transmitted to the target. A python relay class that knows how to receive vectors from the fuzzer is provided. Extending this class to interface with a specific target is left as an exercise for the reader. Examples of reference models and relays are provided for a simple finite state machine and for a tftp server.
FuzzM should work on modern Linux, Windows and macOS platforms that support Docker. FuzzM installation is simplified through the use of both Docker and Docker Compose.
Instructions on installing Docker can be found here.
Instructions on installing Docker Compose can be found here
Information on building and installing FuzzM can be found here.
Information on using FuzzM can be found here.