If you were wondering what formal verification is, well Wikipedia says its “the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.”
Which I think means something like ‘making sure all the computer code is working right’ though I may be over-simplifying. However, formal program verification is the only way to be certain that a piece of software is free of errors, errors that if they occurred in military operations could cost lives. Formal verification is a manual process performed by specially trained engineers, which generally aren’t cheap.
The purpose of DARPA’s program is to make this verification process more accessible by producing understandable and fun to play games that mimic the formal verification process. Completion of the game helps the program verification tool complete the corresponding formal program verification proof.
“We’re seeing if we can take really hard math problems and map them onto interesting, attractive puzzle games that online players will solve for fun,” said Drew Dean, DARPA program manager. “By leveraging players’ intelligence and ingenuity on a broad scale, we hope to reduce security analysts’ workloads and fundamentally improve the availability of formal verification.”
As always, it all boils down to how good these games are. These games are available to anyone, and the primary reason that any gamer buys a game is because it’s fun to play, or at least they believe it will be. Being free also helps; I mean who can turn down a free game?
I guess, I’ll have to download a few of them and see if they hit the right buttons.
The five games are:
- Circuitbot – PC
- StormBound – PC
- Xylem: the (code) of plants – iPad
- Flow Jam – PC
- Ghost Map – PC
If you want to read more about DARPA and their verification program, you can find the full press release here – http://www.darpa.mil/NewsEvents/Releases/2013/12/04.aspx
Read on for more details on Circuitbot and Stormbound
Humanity is reaching out to the stars and colonization of the Solar System will be the first bold step in Left Brain Games’ turn-based strategy title, Circuitbot. While players are venturing beyond a virtual Earth, they will also be making a significant real world contribution. The title is one of five games in DARPA’s crowdsourced formal verification program, which identifies flaws that hackers can exploit in software.
In Circuitbot, players are tasked with building facilities fit for human habitation in far-flung planets throughout the galaxy. To conquer the asteroids, moons and planets throughout space, players must manage resources and direct teams of robots to build factories on these interstellar locations.
“This is one of the most ambitious development projects in the history of gaming,” Andrew Keplinger, president, Left Brain Games, said. “Circuitbot synergizes the thrill of interstellar exploration with the tactical decision-making of the strategy genre, while incorporating a hidden real-world crowdsource program that goes unnoticed, because gamers are having fun!”
Circuitbot is now available at http://circuitbot.verigames.com.
StormBound, a new browser-based puzzle game from voidALPHA, asks players to use their visual pattern recognition and problem solving skills to find weaknesses in magical storms. Conquering the game, one of five games launching as a part of DARPA’s crowdsourced formal verification program, could contribute to the identification of flaws that hackers exploit in software. Are gamers up to that challenge? DARPA wants to find out.
In StormBound, players take on the role of a powerful wizard, trapped from returning to his home world by magical storms. Gamers must look for weaknesses in the patterns that make up storm energy. These flaws can be overloaded and fused shut, reducing the power of the storms.
“The ability of the human mind to look at abstract information and innately recognize patterns is something our most powerful computers can’t match,” Aaron Cammarata, Lead Design, voidALPHA, said. “The challenge DARPA brought to us, and the reason behind the design we created for StormBound, is to find out if some of the millions of smart people out there can conquer this puzzle game. If gamers can, they will help make software more secure.”
Stormbound is now available at http://stormbound.verigames.com.