Play games to help defend — or at least debug — your nation.
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.
[Verigames: About Us]
DARPA press release (December 4, 2013)
Via NetworkWorld, via Slashdot.
Example: Xylem
Xylem is a Verigame game which happens to have a nice YouTube video:
Software developers across the world have a major problem producing bug-free reliable code.
Our task is to help the specialists achieve their goal of ensuring that software that is produced is bug-free.
The way we do it is to take that code and turn it into some puzzles and put them in a game that we called Xylem, and crowdsource the games and the results of the game play help us to produce code that is bug-free.
What next?
This is all very interesting, but doesn’t go deep enough.
I want to know more about the principles of how we “take that code and turn it into some puzzles”.