Binary Fission: Crowd-Sourced Software Verification Program
By playing a game, citizen scientists can help increase reliability of mission-critical software systems.
SRI and partners at University of California, Santa Cruz (UCSC) have created a game where sophisticated gamers can help improve security of the U.S.’ critical software. Binary Fission is a fun, accessible way for “citizen scientists” to help increase the reliability and security of mission-critical software by verifying that it is free of cyber vulnerabilities.
From a gaming perspective, the goal of Binary Fission is simple—sort colored 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 behavior 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 behavior, along with some pre-made invariants, are used to generate each level in Binary Fission. Quarks in the game 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.
Through integrated chat, active community management, and regular community events, Binary Fission also emphasizes community—an important aspect of successful citizen science projects.
Currently, formal software verification is rarely used because relatively few people have the necessary training in software verification techniques. 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 Crowd-Sourced Formal Verification (CSFV) program. 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 (Commissariat à l'énergie atomique et aux énergies alternatives) to develop tools for software analysis and formal verification that feed into Binary Fission.
This material is based upon work supported by the United States Air Force and the Defense Advanced Research Projects Agency under Contract No. FA8750-12-C-0225. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force or DARPA.