WITH its bleepy sound effects and cheery music, Xylem draws me into the puzzle without giving away its secret. A bit like the plot of the recent movie Ender鈥檚 Game, my solutions are helping the US military, or at least its research arm, DARPA.
One of commissioned by the agency, Xylem hides mathematical teasers inside the story of a botanist identifying flowers on a pristine island. In another game, Storm Bound, I play a fearless 鈥淕olamancer鈥�, fighting to turn a magic storm against itself by finding patterns in runes.
Launched last week, the games use a player鈥檚 actions to find security loopholes in anything from internet infrastructure to military software.
Advertisement
The simplest way to check software for bugs is to give it a bunch of commands and see if something goes wrong. Anything a programmer doesn鈥檛 think to check might not be working right, leaving a hole a hacker could wiggle into. The best way to do this is by checking if all of the code鈥檚 underlying logic is sound, a process called formal verification. It鈥檚 a lot more effective than trial and error.
Using the crowd to find patterns within sets of data has grown significantly since the success of Foldit, which recruited people online to decode protein structures. 鈥淢y vision is that, while people are waiting for the bus, they are proving my software correct,鈥� says Michael Ernst, one of the scientists behind the game Flow Jam. 鈥淭hey do it because it鈥檚 more fun than waiting for the bus, and to improve the software that runs the internet, research institutions and industry.鈥�
In Flow Jam, players sort through tangles of pipes and boxes arranged in messy, imperfect circuits. In the process of solving these puzzles they are also looking for holes in sign-up forms and other places where users put information into a database.
鈥淭he recent deployment of [in the US] showed that validating code before it goes live is necessary and difficult,鈥� says Sabine Hauert, who works on crowdsourcing nanotechnology problems at the Massachusetts Institute of Technology. 鈥淭he game developers managed to entirely hide the tedious aspects behind fun games that feel like brain-teasers.鈥�
鈥淭he game developers managed to entirely hide the tedious aspects of testing behind fun games鈥�
Both Xylem and Storm Bound analyse loops, bits of code that call for some repetitive action. For every input, there should be a definite output, so if you鈥檙e walking, for example, your right foot always moves after your left 鈥� the two steps make one loop. Formal verification of these loops calls for creative mathematical models called loop invariants. In a loop with two steps, left should invariably equal right. If the equation doesn鈥檛 hold true, there鈥檚 a coding error. This generally requires human insight, rather than brute computer strength.
鈥淧eople are good at seeing patterns and coming up with creative solutions. Software that automatically tries to find loop invariants takes a scattershot approach,鈥� said Heather Logas, Xylem鈥榮 lead designer. 鈥淗umans actually notice what鈥檚 happening with the loops. They mix and match the tools they have in ways a computer can鈥檛.鈥�
The games aren鈥檛 perfect. None of them are simple to play, and the training rounds are complicated and can be confusing. But the underlying concept is a leap forward for software verification. 鈥淚t鈥檚 audacious to claim that game players who know nothing about programming can do a better job than today鈥檚 highly sophisticated automated program analysis tools,鈥� Ernst said. 鈥淚鈥檓 still amazed that this idea can work at all.鈥�
This article appeared in print under the headline 鈥淧lay games for The Man鈥�
