Crowd-sourced formal verification program generates thousands of software annotations

May 28, 2015, DARPA

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—a 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" . 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 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 that asks players to mix and match quarks in the name of cybersecurity

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

Explore further: Games help improve software security

More information: For more information about CSFV, please refer to the program web page at: www.darpa.mil/Our_Work/I2O/Pro … fication_(CSFV).aspx.

Related Stories

Games help improve software security

December 5, 2013

Ever more sophisticated cyber attacks exploit software vulnerabilities in the Commercial Off-the-Shelf (COTS) IT systems and applications upon which military, government and commercial organizations rely. The most rigorous ...

Can control theory make software better?

March 19, 2013

"Formal verification" is a set of methods for mathematically proving that a computer program does what it's supposed to do. It's universal in hardware design and in the development of critical control software that can't ...

Recommended for you

Matter waves and quantum splinters

March 25, 2019

Physicists in the United States, Austria and Brazil have shown that shaking ultracold Bose-Einstein condensates (BECs) can cause them to either divide into uniform segments or shatter into unpredictable splinters, depending ...

How tree diversity regulates invading forest pests

March 25, 2019

A national-scale study of U.S. forests found strong relationships between the diversity of native tree species and the number of nonnative pests that pose economic and ecological threats to the nation's forests.

0 comments

Please sign in to add a comment. Registration is free, and takes less than a minute. Read more

Click here to reset your password.
Sign in to get notified via email when new comments are made.