Gamers improve the security of country's critical software

From a gaming perspective, the goal of Binary Fission is simple: sort coloured atomic particles or ‘quarks’ in as few steps as possible. Players use up to 100 filters to sort the particles into separate pools. As players move their cursor over a particular pool, they are shown in real time how successfully a particular filter would sort the quarks in that pool.

Binary Fission also allows more sophisticated interactions: rather than defining behaviour of software elements from scratch, players can mix-and-match pre-made descriptions. The search for such descriptions, technically called ‘loop invariants’, takes advantage of visual pattern recognition that people are better at than computers.

Examples of critical software behaviour, along with some pre-made invariants, are used to generate each level in Binary Fission. The quarks in the game actually represent values of variables inside the critical software, and the sorting filters represent the potential invariants to be explored and applied. By combining filters efficiently, players can help to verify that the software is free of security vulnerabilities. Binary Fission also emphasises community, an important aspect of successful citizen science projects, through integrated chat, active community management and regular community events.

Currently, formal software verification is rarely used because relatively few people have the necessary training in verification techniques. In addition, finding loop invariants in software programs has historically been a challenging task requiring extensive training and insight.

Binary Fission is one of five games that DARPA is releasing under its CSFV programme. All games, including the first SRI-and-UCSC-created game, Xylem, are freely accessible through the Verigames website. UCSC and SRI are also collaborating with researchers at CEA, the French Alternative Energies and Atomic Energy Commission to develop tools for software analysis and formal verification that feed into Binary Fission. 

"We're very excited about the play experience in Binary Fission," said Heather Logas, Lead Game Designer, UCSC. "Informed by new research about formal software verification and inspired by the citizen science phenomenon, the game is both very playable and also should contribute well to the underlying science problem."

“The auxiliary Binary Fission feature set is very light, since our goal is to keep players focused on solving problems,” said John Murray, Ph.D., Program Director in the Computer Science Laboratory at SRI International and Principal Investigator for the overall project. “However, as a citizen science project, our recruitment policy draws in players who are interested in solving cybersecurity issues.”

“SRI is well versed in formal software verification, with over a quarter of a century spent assuring that mission-critical computer systems are error-free, secure and interoperable. We are pleased to work with our partners in DARPA’s highly innovative, creative and fun program,” said Patrick Lincoln, Ph.D., Director of SRI’s Computer Science Laboratory. “We learned a lot of valuable lessons with our first game of this type, Xylem. For our gaming approach to succeed, we need a more sophisticated game for a more sophisticated audience. We have levelled up our research, and with more automation, interaction and sophistication, Binary Fission is our best game yet.”