Program Summary
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:
- Increased frequency and cost-effectiveness of formal verification for more types of common COTS software.
- Greatly expanded audience to participate in formal verification.
- Establishment of a permanent community of game players interested in improving software security.
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:
- CircuitBot: Link up a team of robots to carry out a mission.
- Flow Jam: Analyze and adjust a cable network to maximize its flow.
- Ghost Map: Free your mind by finding a path through a brain network.
- StormBound: Unweave the windstorm into patterns of streaming symbols.
- Xylem: Catalog species of plants using mathematical formulas.
Because government regulations require adult volunteer participants for this DARPA research program, CSFV games are open only to players ages 18 and up.