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.
The Defense Advanced Research Projects Agency (DARPA) Crowd Sourced Formal Verification (CSFV) program is interested in improving and advancing the current processes of formal verification by significantly increasing the number of people working on formal verification projects at any given time through crowd-sourcing. CSFV augments the intensive work done by formal verification experts by greatly decreasing the skill required to do formal verification.
Much of the work required in the process of formal verification can be automated. Computers can be programmed to automatically scour software applications and verify the absence of certain bugs that make the applications vulnerable to misuse. However, certain formal verification work needs to be done by human experts specifically trained to discover and address issues that can be missed by computers. However, there aren’t enough of these experts to cover the huge amount of software generated in today’s modern computing world.
CSFV seeks to add more human expertise to the process of formal verification through fun and engaging video games. The games are created to assist in the formal verification process as players solve puzzles and increase their score. Video games that represent the underlying mathematical concepts allow more people to perform verification analysis of software efficiently. We empower non-experts to effectively do the work of formal verification experts—simply by playing and completing game objectives.
Phase 1 of the Verigames project consisted of five games: CircuitBot, Flow Jam, Ghost Map, StormBound and Xylem. By analyzing the game play and formal verification results of the first five games, the development teams and mathematicians behind the project created five new games for Phase 2: Binary Fission, Dynamakr, Ghost Map: Hyperspace, Monster Proof and Paradox. Phase 2 games have been completely redesigned to incorporate improved playability with increased software verification effectiveness.
The five teams involved in the project include:
StormBound/Monster Proof—Galois, Inc.; voidALPHA
CircuitBot/Dynamakr—Kestrel Technology; Texas Tech University; Left Brain Games, Inc.
Ghost Map/Ghost Map: Hyperspace—Raytheon BBN Technologies; Breakaway Games; University of Central Florida
Xylem/Binary Fission—SRI International; University of California at Santa Cruz; Commissariat à l’Energie Atomique (CEA), Saclay, France
Flow Jam/Paradox—University of Washington Center for Game Science
Need more information? Check out our Citizen Science content for extensive material on the science behind the project, contact us or jump to the FAQs!
