I was excited to read Matt Might’s recent post “An introduction to QuickCheck by example”. QuickCheck is a library that lets you define random generators for arbitrary data-types, and then use these generators to produce test cases for functions.

Matt’s post is a perfect occasion to describe the testing methodology we use a Cryptosense, and how it’s different from QuickCheck. I am going to present the ideas behind it at the next ICFP ML Workshop, so think of this as a sneak preview.

Matt uses Okasaki’s red-black trees as an example. In order to test functions that operate on red-black trees, you have to generate some red-black trees first; and it turns out that it is not an easy business. As Matt wrote,

The most time-consuming part of the process is creating generators for random but valid red-black trees.

In the end, Matt uses two generators: one that is rather involved and a simple one that repeatedly inserts random values in an empty red-black tree. I really liked the latter solution, because it is a simple example of the general method that we use at Cryptosense to generate test cases for cryptographic APIs.

The idea of well-typed smart fuzzing (that’s what we do) is that it is possible to generate test cases for any function of a given API by combining the functions of this API in an arbitrary fashion – without access to the source code behind the API.

Looking back at Matt’s example, the interface of a set data-structure implemented using red-black trees provides (at least) a function for creating an empty set, inserting new elements, deleting elements, and testing the presence of elements. To generate sets, you just need to combine the creation of empty set, the addition of random elements, and the deletion of random elements. It might come as a surprise that the fact that these sets are implemented using red-black trees is irrelevant to the generation of test cases!

I quickly adapted Matt’s code in OCaml using a prototype called ArtiCheck (more on this here) that makes it possible to generate test cases based solely on the API of the module is under test. The Articheck library then combines these functions together to produce sets in a pseudo-random fashion and then checks that all the red-black trees that are available at the end of this process are valid red-black trees.

Unfortunately, it is hard to re-introduce Matt’s Haskell bugs in the OCaml version of the code and demonstrate that ArtiCheck helps find the bugs too, because the bugs that were present in his code seem to be the Haskell equivalent of incomplete pattern-matchings in OCaml, which the OCaml compiler traps. So, I played a bit introducing balancing or coloring bugs. They were all caught by our smart fuzzing algorithm.

There are other exciting new developments that are reducing the gap between testing and verification by building on QuickCheck to generate test cases (for instance, Lee Pike’s SmartCheck). What we are doing at Cryptosense is orthogonal but in the same spirit: we are working on a new way to generate test cases, in the specific domain of APIs, and then using this testing to build models for our model-checker. It’s part of a general movement to make the power of formal verification more accessible to programmers.

If you want to know more about our testing methodology I’d be happy to talk to you at ICFP or via email. We’re also recruiting!