What is CSFV?
The Defense Advanced Research Projects Agency (DARPA) wants to help make computer software more safe and secure. DARPA’s Crowd Sourced Formal Verification (CSFV) program intends to create casual computer games that can also perform formal verification of software, a process that checks that software is free from flaws that can make it operate improperly or vulnerable to misuse.
Why is Formal Verification of Software Necessary?
All newly developed software requires time-intensive testing by computers and human experts before the software can be considered reliable. Software testing includes a rigorous analysis process, called formal verification, to ensure the software is free from errors that might cause it to stop working or to work incorrectly.
Why is Formal Verification of Software Currently a Challenge?
Formal verification is currently done manually by specially trained engineers. Consequently, formal verification has been too slow and costly to apply beyond small, critical software components.
What’s the Goal of CSFV?
CSFV aims to create enjoyable games that reflect mathematical models of software. Solving the games provides mathematical proofs that can verify the absence of flaws or bugs. By making the games fun to play and available to the general public via a website, it may be possible for large numbers of non-experts to perform formal verification much faster and more cost-effectively than with conventional processes.
Why Are The Games Restricted to Players 18 Years Old and Older?
Government regulations require adult volunteer participants for this DARPA research program.
What Kinds of Software Does CSFV Verify?
CSFV aims to verify commonly used open source software written in the C and Java programming languages.
What Happens if CSFV Finds a Potential Bug or Flaw?
If CSFV finds potentially harmful code, DARPA will implement approved notification and mitigation procedures including notifying the organization responsible for the affected program. Because CSFV verifies open source software that may be in use in commercial, government and/or Department of Defense systems, prompt notification is essential so that the software can be corrected rapidly.
Which Organizations Are Participating in CSFV?
DARPA has selected five organizations from industry and academia to team with experienced game developers. A U.S. university has been brought on to assess the potential of the game solutions to improve the efficiency of software compiler programs. A web game hosting company (TopCoder, Inc.) has been selected to host the public web site.
For more information on the CSFV program, please visit the DARPA website at http://go.usa.gov/Djmx.