"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," said DARPA in a press statement Wednesday. The best solution to this problem, it says, is formal code verification on a line by line basis by specially trained engineers. The problem, however, is "that up to now has been too slow and costly to apply beyond small software components."
Now there's a new approach. "DARPA’s Crowd Sourced Formal Verification (CSFV) program has developed and launched its Verigames web portal (www.verigames.com) offering free online formal verification games." (It has to be said that when this reporter visited the Verigames site in order to help the COTS industry, the site was unusable. Whether this is a problem is Verigames' own code, or simply a self-induced DOS caused by the world's gamers accessing the site in droves was not clear.)
The idea is to see if the actions taken by gamers in solving puzzles can be translated into formal code verification – the games translate players' actions into program annotations and generate mathematical proofs to verify the absence of C and Java programming flaws. “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,” said Drew Dean, DARPA program manager. “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.”
For now, five games are available from Verigames: CircuitBot ('link up a team of robots to carry out a mission'); Flow Jam ('analyze and adjust a cable network to maximize its flow'); Ghost Map ('free your mind by finding a path through a brain network'); StormBound ('unweave the windstorm into patterns of streaming symbols'); and Xylem ('catalog species of plants using mathematical formulas.') But this could rapidly increase if it proves successful because DARPA has also developed an automated process that helps create new games for each new problem the CSFV program seeks to review.
"If gameplay does reveal potentially harmful code, DARPA will implement approved notification and mitigation procedures, including notifying the organization responsible for the affected software. Because CSFV verifies open source software that commercial, government and/or Department of Defense systems may use, prompt notification is essential to correct the software rapidly and mitigate risk of security breakdowns."
But before that can happen, it has to work. In 2009, Dan Pink concluded in Drive: The Surprising Truth About What Motivates Us: "Carrots & Sticks are so last Century. Drive says for 21st century work, we need to upgrade to autonomy, mastery and purpose." The question is whether the Verigames games provide sufficient 'autonomy, mastery and purpose.'
If they do, the results could be surprising. Discussing the new games, SFGate points to Foldit. "In 2008, researchers at the University of Washington released a game, known as Foldit, that challenged players to manipulate chains of amino acids into optimal shapes. In several weeks, users had produced a model of a protein that could help design antiretroverial [sic] drugs to fight the spread of HIV, according to a 2011 study in the journal Nature Structural & Molecular Biology. That task had stumped scientists and computers for a decade."