Crowd Sourced Formal Verification, find software bugs is a game

Pierluigi Paganini December 13, 2013

DARPA has launched the Crowd Sourced Formal Verification, it creates a set of games that search for software vulnerabilities involving volunteer gamers.

The US Department of Defense Is evaluating the use of video games for finding software vulnerabilities with the collaboration of a network of volunteers. The idea is revolutionary, the support offered to DoD analyst could be theoretically unlimited according John Murray, a program director in SRI International’s computer science laboratory.

Today only adults are allowed to participate in the program due strictly government regulations regarding volunteer participants.

John Murray and his team worked in the creation one game specialized in the above task, the application called Xylem is the demonstration that is possible to exploit game players’™ actions to find software vulnerabilities.

The project is sustained by DARPA,  code named Crowd Sourced Formal Verification (CSFV) program, and has launched a website, called Verigames, that already proposes five free games that can be freely played online and one of them, titled Xylem, on an Apple iPad. In Xylem, for example, the user explores a tropical island and catalogues unusual plants his find by writing short descriptions about their characteristics.

The CircuitBot game involves users to link up a team of robots to carry out a mission, man while Flow Jam requires the user to analyze and adjust a cable network to maximize its throughput.

Crowd Sourced Formal Verification

The project invites participants to play online to a set of games designed to generate “program annotations and mathematical proofs that can identify or prove the absence of flaws in software written in either C or Java”. The principle proposed by DARPA Crowd Sourced Formal Verification (CSFV) program in the exploitation of games for formal software verification flows.
Code review is a very complex activity, time consuming and very costly, that’s why DARPA has launched the program that could involve a large number of people that could provide their support for free.
“Formal Verification is the process of rigorously analyzing software to detect flaws that make programs vulnerable to exploitation. Performing this analysis requires highly skilled engineers with extensive training and experience. This makes the verification process costly and relatively slow. ” states the Verigames portal.

The principle is to correlate complex math problems onto puzzle games that would be fun to play.

“The Defense Advanced Research Projects Agency (DARPA) Crowd Sourced Formal Verification (CSFV) program seeks to replace the intensive work done by the domain experts by greatly decreasing the skill required to do Formal Verification, and therefore allow more people (who do not need to be domain experts) to perform the analysis in a more efficient manner.How might we achieve this? By creating fun and engaging games that represent the underlying mathematical concepts, we empower the non-experts to effectively do the work of the formal verification experts – simply by playing and completing the game objectives. “

To achieve the goals of Crowd Sourced Formal Verification, DARPA designed the Verigames.com portal involving the elite designers, mathematicians, and developers  and Topcoder’s community of over 500,000 registered global members.

According Murray some types of vulnerabilities, including buffer overflows or flaws that result in privilege escalation, fit particularly well into the puzzle format.

“We are able to take those small snippets of code that need further analysis and turn them into the parameters to generate a puzzle,” he said.

DARPA has involved a number of companies to design games for the program, the ambitious goal is to build up a game playing community that would improve the activities of code review reducing the number bugs in the evaluated software.

Pierluigi Paganini

(Security Affairs –  Crowd Sourced Formal Verification, DARPA, games)



you might also like

leave a comment