FuzzM

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. 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.