Pierluigi Paganini
December 13, 2013
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 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.
“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.
(Security Affairs – Crowd Sourced Formal Verification, DARPA, games)
