Computer scientists are making a game out of the difficult task of software verification by creating an entertaining and accessible way to help ensure software programs or systems are free from common vulnerabilities. The Xylem puzzle game, initially available on the iPad, helps find "loop invariants," an important element of formal software verification.
A team of computer scientists from the University of California, Santa Cruz, and SRI International developed Xylem as part of an SRI-led project called Chekofv (Crowd-sourced Help with Emergent Knowledge for Optimized Formal Verification), which is under the broader, multi-institutional Crowd Sourced Formal Verification (CSFV) program funded by the U.S. Defense Advanced Research Projects Agency (DARPA). Xylem is one of five computer games in DARPA's CSFV program, all of which launched publicly on December 4 and are freely accessible through the Verigames website: www.verigames.com.
To play Xylem, you don't need to know anything about software. The setting is a newly discovered island called Miraflora, and the player is a botanist sent to describe the many unusual flowering plants on the island. The intrepid explorer is provided with a "floraphase comparator" for examining the plants. Using this device, the player finds mathematical relationships among the features of flowers on the plants.
"The numbers of flowers are actually values of variables inside software loops. By finding these relationships among flowers, you're actually describing the behavior of a loop," explained Jim Whitehead, professor and chair of computer science at UCSC's Baskin School of Engineering and principal investigator for the project.
Ordinarily, finding loop invariants in software programs is a challenging task that requires extensive training and insight. "It's a hard concept to get across even to computer science students," Whitehead said. "By turning it into a game, it becomes something that an untrained person with basic math skills can do."
Currently, formal software verification is not used very much because relatively few people have the necessary training in verification techniques, according to Whitehead. "There aren't enough experts to formally verify all the kinds of software that are being developed," he said.
With the current release of Xylem, players will be helping to verify the code for the Domain Name System (DNS) server software called BIND, which is widely used on the Internet. In the future, the game could be used to verify other types of software, such as those used in medical equipment or flight-control systems.
Heather Logas, the lead game designer for Xylem, said the project's software verification goals placed tight constraints on the possibilities for gameplay. "There are a lot of things that would make sense to do if we were just designing a game, but to meet the software verification goals we couldn't do them. So we had to come up with some creative solutions," Logas said.
The result of their efforts is an interesting puzzle game with a story line and interactive features to keep players engaged. The island of Miraflora is divided into different regions that players can explore. As the community of players contributes solutions by finding and describing flowers, players can see how much of each region has been explored.
"The Xylem game leverages crowd-sourcing techniques to search for proofs that software programs are free of vulnerabilities," said John Murray, program director in the Computer Science Laboratory at SRI and principal investigator for the overall Chekofv project. "Pieces of software code are inserted into this engaging puzzle game, where players identify new plant species by spotting patterns in the plants' behavior on the island. The more people that play the game and correctly identify patterns, the more pieces of code are verified that they will work with the rest of the software program--it's like solving a gigantic jigsaw puzzle."
About 20 faculty, staff, graduate students, and undergraduates at UCSC's Center for Games and Playable Media were involved in creating the game. A team of computer scientists and engineers from SRI's Information and Computing Sciences Division are providing the Chekofv software verification infrastructure for Xylem. 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 the formal verification process.
Availability
Xylem and other games released from the CSFV program are freely available in on the Verigames website at www.verigames.com. Xylem is also available for free in the Apple App Store, and is expected to be available for Android tablets in 2014.
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.
