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.
- Model-Based Grey-Box Fuzzing. D. Greve. 19th High Confidence Software and Systems Conference (HCSS), April 2019.
- Trapezoidal Generalization over Linear Constraints. D. Greve, A. Gacek. 15th International Workshop on the ACL2 Theorem Prover and Its Applications, November 2018.
- FuzzM: A Model-Based Approach to Grey-Box Fuzzing. R. Coppa, G. Foudree, D. Greve. Technical Report. 2018.
- Trapezoidal Generalization of Lustre with Uninterpreted Functions. D. Greve, J. Backes. Technical Report. 2017.
- Generalization Correctness. D. Greve. 14th International Workshop on the ACL2 Theorem Prover and Its Applications, May 2017.