Xylem: Crowd-Sourced Gaming for Formal Verification | SRI International

Toggle Menu
screenshot of Xylem game on iPad

Xylem: Crowd-Sourced Gaming for Formal Verification

Researchers have created a computer game that could transform the problem of proving software correctness.

Today, formal software verification is used to help ensure that mission-critical software systems are bug-free, secure, and reliable. Formal verification is often a time-consuming, costly process requiring highly specialized computer scientists to manually verify each line of code. Hence, only small, critical components of software systems are usually formally verified.

To improve this manual process and make it more accessible, SRI is participating in the innovative DARPA-funded Crowd Sourced Formal Verification (CSFV) program. Research teams have developed computer games that use crowd-sourcing techniques, enabling people with a less technical skillset to help formally verify code. SRI, a pioneer in formal software methods, leads a team of researchers and developers that includes University of California Santa Cruz and CEA/TECH (France) on the Chekofv (Crowd-sourced Help with Emergent Knowledge for Optimized Formal Verification) project to develop games for DARPA’s CSFV program.

The team’s first game is called Xylem, an engaging puzzle game for the iPad available for free in the Apple App Store or by visiting www.verigames.com. Set on the mysterious island of Miraflora, the player is an explorer who must identify new plant species by spotting patterns in plants’ behavior on the island. The level of difficulty of each puzzle increases as the player correctly identifies more behavior patterns.

By inserting pieces of software code into Xylem, crowd-sourcing techniques can be used to search for proofs that the software system is free of vulnerabilities. As more people play the game and discover useful patterns, more pieces of code can be verified, which in turn helps ensure they will work with the rest of the system. Completion of the game effectively helps the program verification tool complete a corresponding formal program verification proof.

The ultimate goal is to create automated software verification tools that can be used broadly by software engineers and companies developing complex software systems. These tools could increase the reliability and security of mission-critical software applications.

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.

Approved for Public Release, Distribution Unlimited

Related blog post: Gaming for a Higher Purpose: Crowdsourcing to Find Vulnerabilities in Mission-critical Software