Model-Based Grey-Box Fuzzing

Presented as part of the 2019 HCSS conference.

Constraint solving technology can be used to generate tests from model-based system requirements. Such tests can be generated automatically and are capable of meeting even stringent MC/DC code coverage criteria required for DO-178C Level A certification. Given that high-quality safety-relevant behavioral tests can be generated from requirements-level models, perhaps a similar approach works for security-relevant testing as well. Fuzz testing is an example of security-relevant testing that employs random, invalid or unusual inputs to search for unknown and potentially exploitable system behaviors. In this talk we will discuss model-based grey-box fuzzing, a fuzzing technique that employs mathematical models of system-level requirements to guide the fuzzing process and constraint solving technology to deduce high-quality tests capable of targeting deep system behaviors that random fuzzing alone would be unlikely to reach.

The talk will provide an overview of model-based fuzzing, demonstrate how it can be used to model a simple system, and compare its performance with several more traditional off-the-self fuzzing solutions. We will also identify some on-going research challenges associated with model-based fuzzing, including expressing and targeting security relevant requirements and measuring the effectiveness of the generated tests.

David Greve is an applied researcher at Collins Aerospace. David is keenly interested in the prospect of developing perfect systems and he specializes in the construction and analysis of mathematically precise computer system models. David was instrumental in formalizing the GWV class of information flow theorems, applying them to the Collins AAMP7 intrinsic partitioning mechanismin in support of its MILS certification, and refining them to develop a data flow specification and analysis tool useful for reasoning about operating system software. David's current research interests include leveraging automated formal analysis tools to assist in the process of generating high-quality tests.