Crowd-Sourced Formal Verification Program Generates Thousands of Software Annotations

The initial phase of a DARPA program that used publicly accessible online games to accelerate the verification of software has helped produce hundreds of thousands of program annotations in common software programming languages, adding credence to the idea that digital games can be an effective means of crowdsourcing solutions to software problems. The results have inspired DARPA to launch a new round of games with the goal of extending the successes to date and learning more about the approach’s potential.

“We’re excited by these results and are encouraging the public to play our new games over the next few weeks so we can see just how far this approach may go,” said Michael Hsieh, DARPA program manager. “The growth of software systems over the past decade has outstripped improvements in verification. There are simply not enough experts to provide manual analysis on the scale required to support formal verification of the countless software systems launched every day.”

Unreliable software imposes significant costs on the U.S and global economies. Existing development practices result in software that contains about one to five bugs or errors per thousand lines of code. Formal program verification–mathematical approach to ensuring the fundamental accuracy of code–is the best way to be certain that a given piece of software is free of certain types of errors. But formal verification today is almost always done manually by specially-trained engineers, and is too costly to apply beyond small, critical software components.

In December 2013, DARPA’s Crowd Sourced Formal Verification (CSFV) program launched the first version of the Verigames web portal (www.verigames.com), which offered five free online formal verification games. 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.

To learn more about the potential of this approach to crowdsourcing verification, CSFV recently released five new games on www.verigames.com, designed for improved playability as well as increased software verification effectiveness:

• Dynamakr: Asks players to energize mysterious patterns in a cosmic puzzle machine
• Paradox: Asks players to use an array of tools to optimize vast networks
• Ghost Map Hyperspace: Asks players to battle alien invaders and seal off their hyperspace rifts
• Monster Proof: Asks players to explore a kingdom of monsters and solve puzzles to get rich
• Binary Fission: An atom-splitting game that asks players to mix and match quarks in the name of cybersecurity

CSFV games are open only to players ages 18 and up.

For more information about CSFV, please refer to the program web page at: http://bit.ly/1lCyL74.