Categories: Security

Crowd Sourced Formal Verification, find software bugs is a game

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.

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)

Pierluigi Paganini

Pierluigi Paganini is member of the ENISA (European Union Agency for Network and Information Security) Threat Landscape Stakeholder Group and Cyber G7 Group, he is also a Security Evangelist, Security Analyst and Freelance Writer. Editor-in-Chief at "Cyber Defense Magazine", Pierluigi is a cyber security expert with over 20 years experience in the field, he is Certified Ethical Hacker at EC Council in London. The passion for writing and a strong belief that security is founded on sharing and awareness led Pierluigi to find the security blog "Security Affairs" recently named a Top National Security Resource for US. Pierluigi is a member of the "The Hacker News" team and he is a writer for some major publications in the field such as Cyber War Zone, ICTTF, Infosec Island, Infosec Institute, The Hacker News Magazine and for many other Security magazines. Author of the Books "The Deep Dark Web" and “Digital Virtual Currency and Bitcoin”.