More and more, people around the world rely on complex software systems in all areas of life—from transportation to utility grids to medical equipment. We depend on these software systems to be secure and reliable. Yet today, the way to assure bug-free software code is through formal software verification, which requires highly specialized computer scientists to manually verify hundreds of thousands of lines of code. It’s difficult for any one individual to see all of the interactions implicit in the code, and the process is time-consuming and costly. Hence only small, critical components of software systems can be formally verified.
SRI International, a pioneer in formal software methods, is looking to change this. Through an innovative DARPA-funded program called Crowd Sourced Formal Verification (CSFV), teams of researchers and developers are creating games that aim to make the manual process more accessible. By inserting pieces of software code into a game, we can involve many game players in identifying patterns and solving puzzles, which actually helps verify that the software code is bug-free.
The SRI-led team, which includes developers from UC Santa Cruz and CEA/TECH in France, has developed an intriguing puzzle game for the iPad called Xylem. Set on the mysterious island of Miraflora, the player is an explorer who embarks on an adventure to discover new and exotic plant species. As the player identifies and solves the patterns and behaviors of the island’s plants, the player is helping to piece together the parts of the overall software code to ensure that it is bug-free. The more people that play the game and discover previously hidden patterns, the more pieces of code can be correctly verified, which helps ensure that they will work correctly with the rest of the software system. It’s like solving a gigantic jigsaw puzzle.
We’re asking the Sudoku and crossword puzzle enthusiasts out there to give this challenging puzzle game a spin, and we’ve put together a brief video that includes some of the game’s highlights. The time commitment is minimal—it’s perfect for people who like to fit a puzzle into their spare minutes. You can easily pick up where you left off if you need to stop playing.
Best of all, Xylem players will be helping us to improve software and develop bug-free code. By using crowdsourcing techniques to verify that software programs are free of vulnerabilities, we plan to create automated software verification tools that could be used broadly by more software engineers and companies developing mission-critical software systems. Ultimately, these tools could be used to increase the reliability and safety of software that people around the world depend on to be secure.
Play with us!
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