DARPA’s games crowdsource discovery of software flaws
The Defense Advanced Research Projects Agency (DARPA) has developed a series of games aimed at discovering whether large numbers of non-expert users can perform formal software code verification faster and cheaper than trained experts would.
Formal verification is an analysis process aimed at finding exploitable flaws and vulnerabilities in software, but is usually performed manually by engineers who know what they are looking for. That means that the process is usually long, tedious, not at all cost-effective, and therefore not used often.
“Finding faster, more cost-effective means to perform formal verification is a national security priority, so DARPA’s Crowd Sourced Formal Verification (CSFV) program has developed and launched its Verigames web portal offering free online formal verification games,” the agency announced last week.
“The CSFV games translate players’ actions into program annotations and generate mathematical proofs to verify the absence of important classes of flaws in software written in the C and Java programming languages,” they explained.
“CSFV has developed an automated process that enables the creation of new puzzles for each math problem the 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.”
Five games are currently offered. In “CircuitBot”, players must link up a team of robots to carry out a mission, and in “Flow Jam” they have to analyze and adjust a cable network to maximize its flow. The goal of “Ghost Map” is to find a path through a brain network, and “StormBound” sees players “unweaving” a windstorm into patterns. Finally, “Xylem” makes them catalog species of plants using mathematical formulas.
With these games and others that might follow, DARPA is trying to harness the power of the crowd to solve a critical security issue, and in order to entice users to participate, it offers fun puzzles.