Property-based random testing, exemplified by frameworks such as Haskell's QuickCheck, works by testing an executable predicate (a property) on a stream of randomly generated inputs. Property testing works very well in many cases, but not always. Some properties are conditioned on the input satisfying demanding semantic invariants that are not consequences of its syntactic structure—e.g., that an input list must be sorted or have no duplicates. Most randomly generated inputs fail to satisfy properties with such sparse preconditions, and so are simply discarded. As a result, much of the target system may go untested.
We address this issue with a novel technique called coverage guided, property based testing (CGPT). Our approach is inspired by the related area of coverage guided fuzzing, exemplified by tools like AFL. Rather than just generating a fresh random input at each iteration, CGPT can also produce new inputs by mutating previous ones using type-aware, generic mutator operators. The target program is instrumented to track which control flow branches are executed during a run and inputs whose runs expand control-flow coverage are retained for future mutations. This means that, when sparse conditions in the target are satisfied and new coverage is observed, the input that triggered them will be retained and used as a springboard to go further.
We have implemented CGPT as an extension to the QuickChick property testing tool for Coq programs; we call our implementation FuzzChick. We evaluate FuzzChick on two Coq developments for abstract machines that aim to enforce flavors of noninterference, which has a (very) sparse precondition. We systematically inject bugs in the machines' checking rules and use FuzzChick to look for counterexamples to the claim that they satisfy a standard noninterference property. We find that vanilla QuickChick almost always fails to find any bugs after a long period of time, as does an earlier proposal for combining property testing and fuzzing. In contrast, FuzzChick often finds them within seconds to minutes. Moreover, FuzzChick is almost fully automatic; although highly tuned, hand-written generators can find the bugs faster, they require substantial amounts of insight and manual effort.
Fri 25 OctDisplayed time zone: Beirut change
11:00 - 12:30
|CLOTHO: Directed Test Generation for Weakly Consistent Database Systems|
Kia Rahmani Purdue University, Kartik Nagar Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue UniversityDOI Pre-print
|Coverage Guided, Property Based Testing|
Leonidas Lampropoulos University of Pennsylvania, University of Maryland, Michael Hicks University of Maryland, Benjamin C. Pierce University of PennsylvaniaDOI
|FuzzFactory: Domain-Specific Fuzzing with Waypoints|
Rohan Padhye University of California, Berkeley, Caroline Lemieux University of California, Berkeley, Koushik Sen University of California, Berkeley, Laurent Simon Samsung Research America, Hayawardh Vijayakumar Samsung Research AmericaDOI Pre-print
|Compiler Fuzzing: How Much Does It Matter?|
Michaël Marcozzi Imperial College London, Qiyi Tang Imperial College London, Alastair F. Donaldson Imperial College London, Cristian Cadar Imperial College LondonLink to publication DOI Pre-print Media Attached File Attached