SRI International and UC Santa Cruz Turn Software Verification into Gameplay

MENLO PARK, Calif. and SANTA CRUZ, Calif., Dec. 9, 2013 /PRNewswire/ -- A team of computer scientists from SRI International and University of California, Santa Cruz 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.

(Photo: http://photos.prnewswire.com/prnh/20131209/SF30093)

Xylem is 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 are freely accessible through the Verigames website: www.verigames.com.

"The Xylem game leverages crowd-sourcing techniques to search for proofs that software programs are free of vulnerabilities," said John Murray, Ph.D., 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."

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. As the community of players contributes solutions by finding and describing flowers, players can see how much of the island has been explored.

"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, Ph.D., professor and chair of computer science at UCSC's Baskin School of Engineering and the university's principal investigator for Xylem.  

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 more than 25 years of experience developing and using formal software verification tools, SRI understands how vitally important it is to assure that mission-critical computer systems are error-free, secure, and interoperable," said Patrick Lincoln, Ph.D., director of the Computer Science Laboratory at SRI International. "The Chekofv project is an aggressive research program that addresses these complex software problems in highly innovative ways. By making formal software verification more accessible and fun, a lot more people can help increase reliability and security for critical software around the world by playing the Xylem game."

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."

The result of their efforts is an interesting puzzle game with a story line and interactive features to keep players engaged.

A team of computer scientists and engineers from SRI's Information and Computing Sciences Division are providing the Chekofv software verification infrastructure for Xylem. About 20 faculty staff, graduate students, and undergraduates at UCSC's Center for Games and Playable Media were involved in creating the game. 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. Currently, Xylem is 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.

About SRI International
Innovations from SRI International have created new industries, billions of dollars of marketplace value, and lasting benefits to society—touching our lives every day. SRI, a nonprofit research and development institute based in Silicon Valley, brings its innovations to the marketplace through technology licensing, new products, and spin-off ventures. Government and business clients come to SRI for pioneering R&D and solutions in computing and communications, chemistry and materials, education, energy, health and pharmaceuticals, national defense, robotics, sensing, and more.
Visit SRI's website and Timeline of Innovation to learn more about SRI.

SOURCE SRI International