Slashdot Mirror
DARPA Wants You To Verify Software Flaws By Playing Games
coondoggie writes: Researchers at the Defense Advanced Research Projects Agency (DARPA) think online gamers can perform the tedious software verification work typically done by professional coding experts. They were so impressed with their first crowdsourced flaw-detecting games, they announced an new round of five games this week designed for improved playability as well as increased software verification effectiveness. “These games translated players’ actions into program annotations and assisted formal verification experts in generating mathematical proofs to verify the absence of important classes of flaws in software written in the C and Java programming languages. An initial analysis indicates that non-experts playing CSFV games generated hundreds of thousands of annotations,” DARPA stated.
I'm one of the people involved in creating the Binary Fission game, so I can explain a little bit about what is going on "behind the scenes" in this game.
In Binary Fission (http://binaryfission.verigames.com/), players use filters to try and make clean separations between piles of blue and gold colored dots ("bits"). It is usually the case that no one filter cleanly separates all of the blue bits from the gold bits, and hence solving a puzzle requires judicious use of filters to subdivide the piles into smaller piles, until you can find filters that do cleanly separate the smaller piles.
Overall, the science goal of the game is to have players discover "loop invariant" conditions (http://en.wikipedia.org/wiki/Loop_invariant). This is a mathematical expression that describes (an approximation to) the behavior of a loop (for loop, while loop). For example, if a loop increments x by two each time through the loop, then a loop invariant would be x = {initial value of x} + {loop iteration count} * 2. At any point in the execution of the loop, this condition always holds. That is, the condition doesn't vary, and is "invariant".
Behind the scenes, each of the bits (the dots) really represents a cluster of mappings of variables to values within a single iteration through a loop. One color of bits represents values of variables that are "good" -- they are consistent with the values that variables could have during loop execution. The other color of bits represents values of variables that are "bad" -- they are values that the variables could never have during loop execution.
The filters represent possible loop invariant conditions. A strong loop invariant condition will perfectly separate the good values from the bad values, and thereby be a precise description of the behavior of the loop. Multiple combinations of filters can be combined together to create an aggregate loop invariant expression.
One way of putting this is we're looking at finding loop invariants as a kind of classification problem, where we're trying to find the best possible classifier that will separate valid variable values from invalid variable values. The act of applying filters involves the player constructing a classifier.
Right now, the filters in Binary Fission are candidate loop invariants that are output by the Daikon automated loop invariant finder (http://plse.cs.washington.edu/daikon/). These candidate invariants from Daikon are not usually good enough to describe the entire loop behavior, so the human player is using their unique judgement to augment the best output we get from automated invariant finder tools.