When presented with the option between playing a computer game and slowly wading through a piece of buggy code looking for flaws, most people would probably pick the former. And, when it comes to improving overall code quality, that choice might be the more effective one. A new DARPA program is looking to tackle the challenge of verifying long, complex pieces of software by enlisting the public to play a set of puzzle games linked to mathematical proofs used for formal verification. By crowdsourcing code review, the project could help improve the quality of Department of Defense and commercial software alike.
Dubbed the Crowd Sourced Formal Verification program, the DARPA initiative introduced five attractive, accessible-looking games, with titles like “Storm Bound” and “Ghost Map,” each of which presents players with puzzles. Focusing on common open source applications written in C and Java, CSFV will use player solutions in the games to carry out mathematical proofs and “verify the absence of flaws or bugs” in code, according to a FAQ on the website, Verigames.com, that hosts the games.
“We’re seeing if we can take really hard math problems and map them onto interesting, attractive puzzle games that online players will solve for fun,” DARPA program manager Drew Dean said. “By leveraging players’ intelligence and ingenuity on a broad scale, we hope to reduce security analysts’ workloads and fundamentally improve the availability of formal verification.”
A more efficient solution to verification
Currently, code review often presents a challenge to large software projects, DARPA noted in its project announcement. Most code bases contain around five errors per thousand lines of code, but military products must be entirely accurate.
“Formal verification of software provides the most confidence that a given piece of software is free of errors that could disrupt military and government operations,” the program announcement stated. “Unfortunately, traditional formal verification methods do not scale to the size of software found in modern computer systems. Formal verification also currently requires highly specialized engineers with deep knowledge of software technology and mathematical theorem-proving techniques.”
The program’s one drawback is that, technically as government volunteers, players of the games must be 18 or older. However, the CSFV initiative will be an interesting test to see how crowdsourcing might be leveraged to strengthen software. Of course, developing a publicly accessible game to test every mathematical function in a program might be outside the scope of what many businesses can accomplish. Nonetheless, any organization can benefit from thorough code review using peer review software tools and automated source code analysis programs, and such approaches should be a part of development regardless of whether there’s a computer game involved or not.
Software news brought to you by Klocwork Inc., dedicated to helping software developers create better code with every keystroke.