Unreliable software places huge costs on both the military and the civilian economy. Currently, most Commercial Off-the-Shelf (COTS) software contains about one to five bugs per thousand lines of code. Formal verification of software provides the most confidence that a given piece of software is free of errors that could disrupt military and government operations. Unfortunately, traditional formal verification methods do not scale to the size of software found in modern computer systems. Formal verification also currently requires highly specialized engineers with deep knowledge of software technology and mathematical theorem-proving techniques. These constraints make current formal verification techniques expensive and time-consuming, which in turn make them impractical to apply to COTS software.
DARPA created the Crowd Sourced Formal Verification (CSFV) program to overcome these challenges. CSFV aims to investigate whether large numbers of non-experts can perform formal verification faster and more cost-effectively than conventional processes. The goal is to transform verification into a more accessible task by creating fun, intuitive games that reflect formal verification problems. Playing the games would effectively help software verification tools complete corresponding formal verification proofs.
The program envisions numerous benefits, including:
CSFV’s Verigames web portal (www.verigames.com) offers free online games that translate players’ actions into program annotations that help formal verification. Gameplay generates mathematical proofs that can verify the absence of certain software flaws or bugs in common open source software written in the C and Java programming languages. If gameplay reveals potentially harmful code, DARPA will implement approved notification and mitigation procedures, including notifying the organization responsible for the affected software. Because CSFV verifies open source software that commercial, government and/or Department of Defense systems may use, prompt notification is essential to correct the software rapidly and mitigate risk of functional or security breakdowns.
Verigames offers five games:
Because government regulations require adult volunteer participants for this DARPA research program, CSFV games are open only to players ages 18 and up.
Dr. Michael Hsiehmichael.firstname.lastname@example.org