How playing computer games can make the world safer

Playing computer games can help make the world a safer place. Yes, really.

Maybe not blockbusters like Grand Theft Auto, but a new type of game designed to perform another function while you're playing it.

Take Binary Fission, for example. It challenges you to sort coloured atomic particles in as few steps as possible. It may seem like just another brain-teasing puzzle game, but you're actually helping to foil hackers and cyber-criminals while playing it.

How so?

Well, as you solve the puzzles you're actually helping to "verify formally" that an underlying software program is free from bugs and vulnerabilities that could leave it open to attack.

And as software is critical in the running of almost everything these days, from national energy networks to police drones, air traffic control systems to emergency services, formal verification is an essential process.

Binary Fission has been developed by SRI International, a non-profit research institute based in California, in partnership with the Air Force Research Laboratory and the University of California, Santa Cruz.

John Murray, a program director at SRI International, explains that the puzzles are generated automatically by the game using program code and data from the software that is being verified.

Sets of data - good and bad - are converted into coloured balls that are presented to the player - blue balls representing good values, and gold balls representing bad values.

The player has to select combinations of "filters" generated by the game to separate the blue balls from the gold balls, and successfully doing so assists with the software verification process.

"When a player solves a puzzle in this way they speed up the verification," says Dr Murray. "It may be that one player on one level of the game comes up with the key pattern that helps complete the verification job."

Now this may not sound as exciting as Call of Duty: Black Ops, but Simone Castagna, a games designer and player of PC-based puzzle and shooting games, says Binary Fission and other verification games are "quite fun to play, and they're very similar to other puzzle games I've played."

She adds: "It's worth noting I was only told Binary Fission was a puzzle game, so I was surprised when I found out it had a research component to it."

The game is part of a crowdsourcing project funded by the US Defense Advanced Research Projects Agency (Darpa), which is trying to address the fact that commercial off-the-shelf software typically contains up to five bugs per thousand lines of code.

The problem is that formal verification - providing mathematical proof that a piece of software is error-free - is a complex business.

"Formal verification is wildly expensive and very difficult," says Michael Ernst, a computer science professor at the University of Washington who is involved with the Darpa project.

"That's because you usually need a highly skilled, highly paid software engineer to carry out the process."

There are "only 3,000-to-4,000 people who can carry out verification today," according to SRI's Dr Murray.

So harnessing the power of the crowd - a volunteer army of gamers - is one way to tackle the problem.

Many companies, including Google, Facebook and PayPal, already use a slightly different crowdsourcing technique to try to make their software more reliable.

They run "bug bounty" schemes that award money to anyone who finds and reports security vulnerabilities in their software. And some companies, such as Bugcrowd and Bugwolf, run such schemes on behalf of others.

The key difference is that while bug bounty programs may reduce the number of bugs in a piece of software, they can't provide a guarantee that there aren't more bugs yet to be discovered.

But making games that help with formal verification and are also fun to play has proven to be tricky, says Michael Ernst.

"We would have loved to have been able to pick up the idea of Angry Birds or Candy Crush and turn it into something that does useful work, but it turns out that you can't," he says.

"To encode the problems we are tackling, these types of puzzles would have had to have been huge - like a Candy Crush puzzle that had 10,000 fruits."

So far there are just six of these specialist games listed on Darpa's Verigames.com website.

Andrew Keplinger, president of Connecticut-based Left Brain Games and the designer of two other games in Darpa's project, had a similar experience.

"In effect, what you are doing is getting game players to do disguised work. We started off by applying the ideas of existing games like Candy Crush, or popular maze games, but what we found is that the underlying information that we needed to use just didn't work with this type of game," he says.

"So in the end we had to go in the other direction by taking the underlying science and seeing what we could do to make it fun."

In the future, SRI International's Dr Murray would like to develop a service so that any software developer could submit software and have it verified by a game.

"That could be a good business model because there is an enormous amount of critical software that needs to be subjected to verification," he says.

If he is successful, then the security of vital software used by large companies and governments around the world may end up being improved by hordes of computer games players simply having fun.

"And I used to tell students that video games are just meant to be fun and have no other purpose!" Dr Murray concludes.