QuickChick: Property-Based Testing for Coq |
Advisor: Cătălin Hriţcu ⟨catalin.hritcu@gmail.com⟩
INRIA Team: Prosecco
Location: 23 Avenue d’Italie, Paris, France
Language: English (no French)
Existing skills or strong desire to learn:
Devising mechanisms for enforcing strong safety and security properties is often very challenging. This makes it hard to be confident in the correctness of such mechanisms without fully machine-checked proofs; e.g., in the Coq proof assistant [1]. However, carrying out these proofs while designing the mechanisms can be an exercise in frustration, with a great deal of time spent attempting to verify broken definitions, and countless iterations for discovering the correct lemmas and strengthening inductive invariants. To prevent failed proof attempts and thus reduce the overall cost of producing a formally verified enforcement mechanism, we advocate the use of property-based testing for systematically finding counterexamples. Property-based testing can find bugs in definitions and conjectured properties early in the design process, postponing proof attempts until we are reasonably confident that the design is correct. Moreover, testing can be very helpful during the proof process for quickly validating potential lemmas, inductive invariants, or simply the current proof goal. In order for this methodology to work well though, testing has to be integrated with the proof assistant. The long term goal of this line of research is to devise QuickChick, the first property-based testing framework for Coq. We believe that such a tool could considerably improve the proving experience in Coq, and thus have a significant and long lasting impact on the growing Coq community.
As a first step in this direction, I collaborated with researchers from University of Pennsylvania, Chalmers, and MSR Cambridge, on building the initial prototype of a random testing framework for Coq similar to QuickCheck [14]. We used this framework to test noninterference for increasingly sophisticated dynamic information flow control (IFC) mechanisms for low-level abstract machines [22]. These case studies showed that property-based random testing can quickly find a variety of missing-taint and missing-exception bugs, and incrementally guide the design of a correct version of the IFC mechanisms. We found that both the strategy for generating random programs and the precise formulation of the noninterference property are critically important for good results.
We plan to extend this initial prototype, building on the existing research literature on property-based testing (e.g., random testing [14, 19, 6, 9], exhaustive testing with small instances [29, 23, 9], narrowing-based testing [26, 29, 13, 9], etc.), as well as related work on generating executable code from inductive definitions [5, 16, 4, 30], automatically generating data that satisfies the preconditions of the tested property [20, 10, 12], integrating testing and proof automation [28], exploiting model finders [31, 7], etc. However, our ambition goes beyond bringing some of these existing techniques to Coq and integrating them into a cohesive testing framework. Our research goal is to extend the state of the art in property-based testing by working out several promising new ideas that could become QuickChick’s killer features. Two of these ideas, smart mutation and the deep integration with Coq/SSReflect, are explained in more detail below and constitute the main focus of this proposal.
The first idea is to use smart mutation to evaluate and improve the effectiveness of property-based testing and to obtain confidence not just that no bugs are found, but that no bugs are left.1 As a first step we are focusing our attention on testing the soundness of static and dynamic enforcement mechanisms (e.g., type systems, dynamic IFC systems, etc.). In this case, we are looking at smart mutation strategies that can only make the enforcement mechanism more permissive and that cover whole classes of interesting pointwise bugs. This enables the following iterative workflow: We start with the best guess for the mechanism and enforced property, and use property-based testing to find and fix bugs in the definitions and conjectured property. When we can no longer find any bugs this way, we use mutation to evaluate how good our testing is by generating a large number of more permissive enforcement mechanisms and separately testing each of them. If testing finds a counterexample to a mutant that mutant is killed, and if testing kills all generated mutants then we are done: we get high confidence that no bugs are left and our mechanism is sound with respect to the tested property. On the other hand, if some mutants escape testing, we inspect them one by one and try to manually construct a counterexample against any of them. In case we can manually find such a counterexample that was missed by testing, then our testing is clearly not good enough, and we need to improve it until the new counterexample is found automatically, e.g., by fixing bugs in the generator, or changing the random probability distribution, or coming up with a smarter generator. In practice we observed that improving testing based on a counterexample often kills a large number of other live mutants, and also sometimes finds new counterexamples against the current non-mutated design, which we fix before continuing. At the end, either all mutants are killed, or we are left with some live mutants to which we cannot find counterexamples by hand. These remaining live mutants are probably correct, and since we are only generating more permissive mutants we can use them to produce a better enforcement mechanism by applying these positive mutations to our current design, and iterating the whole process.
We believe that this workflow would be extremely effective in practice. However, in order to support this workflow, we need to be able to automatically generate smart mutants. While syntactic code mutation has been used to empirically evaluate the effectiveness of testing for decades [24], the existing techniques do not generate only more permissive mutants, which in our case means one would have to manually weed thorough lots of mutations which are simply stupid, and for which not finding a counterexample doesn’t produce any benefit (probably just frustration). In recent experiments with testing noninterference (a followup of [22]) we found that splitting the IFC enforcement mechanism out of the operational semantics and into a separate rule table2 allows us to easily generate all “missing check” and “missing taint” mutants.3 This is guaranteed to lead to a more permissive mechanism, allows us to cover all interesting mistakes one can make in this setting, and worked very well in our experiments.
The big open problem is generalizing this idea beyond IFC to arbitrary properties and mechanisms. One simple thing to try first would be writing the enforcement mechanism as an inductive relation in Coq and mutating this relation by dropping or weakening premises. While such relations are not directly executable, and thus not directly testable, a Coq plugin can often extract an executable variant [30, 16], and could be extended to additionally apply our mutations beforehand. One could try this out on the System F<: [11, 2] type system, or some other mechanized metatheory benchmarks [25].
As discussed above we want QuickChick to be deeply integrated into the Coq proving process. However, an important limitation of our current prototype is that it only works for executable specifications written as Coq functions, which doesn’t match usual Coq practice of defining things inductively. We could lift this limitation using the Coq plugin by Delahaye, Dubois, et al. [30, 16] for producing executable variants of inductively defined relations. More ambitiously, we would like to take advantage of QuickChick at any point during the proof process, by freely switching between declarative and efficiently executable definitions. We believe we can achieve this by integrating testing into the normal workflow of small-scale reflection proofs, as supported by the SSReflect extension for Coq [21]. However, while traditional SSReflect proofs use execution to remove the need for some reasoning in small proof steps, the objects defined in the SSReflect library and used in proofs are often not fully executable and often not efficiently executable either. We believe we can support efficient testing during SSReflect proofs by exploiting a recent refinement framework by Dénès et al. [17, 15], which allows maintaining a correspondence and switching between proof-oriented and computation-oriented views of objects and properties.
Finally, testing can also help during automated proof search, as illustrated by recent work on ACL2s [28]. Moreover, automatically finding the witness of an existential quantifier is the same problem as generating data that satisfies the preconditions of the tested property, for which solutions have already been proposed [20, 10, 12]. This kind of usage requires to integrate testing more seamlessly into Coq though, so that the result of testing and the produced counterexamples are available to Coq tactics and terms. While our current prototype implements most things in Coq, it uses extraction to generate Haskell programs that are then executed efficiently outside of Coq,4 and we could envision exploiting recent progress on efficient Coq reduction [8] to complement extraction. The random testing mode of the resulting internal testing framework would need to use a deterministic random number generator implemented in Coq, with the initial seed introduced in the environment through a plugin. Additional care needs to be taken when using random testing inside tactics and proofs, which need to be stable across multiple runs and different machines. Potential solutions include capturing the random seed or the produced counterexamples and saving them inside the proof script, or replacing random testing with exhaustive testing with small instances [29, 23, 9] and narrowing-based testing [26, 29, 13, 9] when possible.
This document was translated from LATEX by HEVEA.