DARPA Builds Computer Games to Verify Software

The Pentagon’s research organization has teamed up with software developers and online gamers in order to create computer games that can help verify and develop secure open-source software.

The Defense Advanced Research Project Agency, or DARPA, has partnered with private sector technology and gaming firms to develop online games which enable gamers to do the software verification work normally done by experts. Through a DARPA program called Crowd Sourced Formal Verification, or CSFV, the software verification work typically done by domain experts is done by online gamers.

“There are not enough human experts or available time to demonstrate that software is secure and reliable – so what we’ve done is repackage what human experts would normally do and produce tens of thousands of game levels for players on the internet to play games for us,” said Matthew Barry, principal investigator, Kestrel Technology.

One such game is called Circuit Bot, an online game which packages software development as space exploration.  Users are asked to conduct various missions to asteroids and planets to build infrastructure and support further space exploration, Barry explained.

“Along the way they are assembling teams of robots that have different assignments. If you assemble the robot team in the correct order you get a certain amount of points. The results of those assemblies contribute toward the verification of open source software,” Barry explained.  “We’re enhancing what a human expert has to do by using the internet crowd to play games.”

Barry said Kestrel technology is still collecting data and putting the results through various iterations to ensure they are stable. The game has been played by users since this past December.

“Even software that has been around for a long time reveals vulnerabilities,” he added.

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, according to statements from DARPA.

Circuit Bot is one of five games set up through DARPA’s partnership with private sector gaming and technology firms.  The DARPA-inspired website, called Verigames.com, gives internet users a chance to play Circuit Bot as well as four other games for free –  Xylem where user select plant species,  Storm Bound where users work on patterns of streams, Flow Jam where users connect cables and Ghost Map where users navigate a mind-map.

Xylem, a mobile game played on an ipad, was developed by the University of California, Santa Cruz in conjunction with a firm called SRI International. Storm Bound was developed by a California-based firm called voidALPHA.  BBN-Raytheon is the maker of Ghost Map and Flow Jam was developed by the University of Washington’s Center for Game Science. Circuit Bot is made by California-based Kestrel Technology and a Connecticut firm called Left Brain Games.

Formal verification is the process of analyzing software to detect flaws that make programs vulnerable to exploitation, according to Verigames.com.

The verification process contains a measurable cyber-security function because software without vulnerabilities is much less likely to be successfully hacked into.  The Verigames.com exercise is designed to identify, develop and verify open source software which could be used by commercial or military and government entities.

If this gaming experiment continues to yield helpful results, using online gamers to help with software verification may greatly help improve the formal verification process – because the process can otherwise be slow, expensive and reliant up a small niche group of experts able to perform the work.