PROPERTY-BASED RANDOM TESTING (PBRT) is a form of black-box testing in which executable partial specifications of a software artifact are used to check its behavior with respect to large numbers of randomly generated test cases. PBRT offers a range of benefits that complement the traditional strengths of full, formal verification; in particular, it (1) allows much more rapid iteration on designs, (2) encourages early focus on stating correct specifications, and (3) supports later proof efforts by allowing invariants to be debugged quickly. Popularized by the QuickCheck tool in Haskell, PBRT is now widely used in both research and industry.

However, one area where current PBRT methodology has been less successful is where the data values used in testing come with have complex internal structure or intricate invariants. In particular, this is the case in testing of language designs and related artifacts such as compilers, where the test data are programs.  Despite some promising preliminary efforts, random testing has proved difficult to apply to full-scale language designs. Many of the interesting properties of programming languages are "conditional," leading to a large number of discarded test cases when random testing is applied naively. This places a premium on the ability toconstruct good custom generation strategies, but generation strategies for``interesting programs'' are neither well understood nor well supported by existing tools: better techniques are needed for writing and debugging test-data generators.

This project focused on property-based random testing of language designs, with specific applications to testing fundamental properties of language definitions and related artifacts---properties such as type safety, security( e.g., ``secret inputs cannot influence public outputs''), and compiler correctness.  Specific accomplishments included (1) developing new methodology for writing and debugging random generators for complex data, inparticular a framework based on generating ``mutants'' of an artifact under test; (2) designing a domain-specific language for writing generators for random test data with complex invariants (3) distributing polished implementations, both as a compatible extension to the standard QuickCheck library and as a native random-testing tool for the Coq proof assistant; and( 4) evaluating the usefulness of these tools by applying them to severalsignificant case studies.

Our first product was a new domain-specificlanguage, called Luck, for writing random generators. We carried out two major case studies in Luck, replicating previous studies (using different technologies) on using PBRT to find bugs in information-flow analyses and functional-language compilers, showing that we can achieve comparable bug-finding effectiveness with much smaller effort, though (with the current prototype implementation) somewhat more slowly.

The major software product of the grant was a random testing tool called QuickChick for the Coq proof assistant.  This tool already existed in prototype form at the start of the grant, but during the grant period it was enormously improved, re-engineered, and applied to several significant case studies.  In particular, we built a "mutation testing" framework for QuickChick and used it in testing several pieces of software being developed outside of this project. We used it to aid development of the next design iteration of the Vellvm verified compiler framework, and we used it to help design and specify the DeepSpec web server.  QuickChick is now publicly released and included in Coq's continuous integration suite.

QuickChick is described in a new book written during the grant -- volume 4 in the Software Foundations series. We taught about 250 people to use it as part of the NSF-supported DeepSpec summer schools on verified software. 

Apart from work on Luck and QuickChick, we used the Erlang version ofQuickCheck to build a testable specification for distributed file synchronization services, which was able to find several bugs in Dropbox that were not known to the Dropbox engineers.  Finally, in ongoing work that began during the grant, we used the Haskell version of QuickCheck to help prototype, debug, and analyze several of the "micro policies" being developed at Draper Labs and Dover Microsystems for enforcing dynamic security policies using CoreGuard, a new tagged security coprocessor architecture.

Last Modified: 01/27/2020
Modified by: Benjamin C Pierce