StormBound: From the Formal Verification PerspectiveThursday, Dec 12 2013

Posted byJefBell66

I’m Jef Bell (yes, really, just one “f”) and I’m the project lead on the Galois side of the Galois/voidALPHA team that has created StormBound.  I’ve been working in software engineering and computer science research since, well, let’s just say the first computer I owned had 16K of memory and stored its programs on a cassette tape.  This is my first chance to contribute, at least in a small way, to constructing a video game since those early days writing game programs that displayed on black-and-white screens with annoyingly scratchy sound effects.

Galois comprises a small team of computer scientists located in Portland Oregon, that aims to make critical computer systems trustworthy.  We apply our work to both security, ensuring that vital information remains well protected, and safety, ensuring that systems that lives depend on (such as aircraft control systems) run correctly. 

As we all know, software usually has bugs, and doesn’t always operate as its creators intended.  Most software development teams use extensive testing, both by the team itself and by the users of the software, to find and eliminate bugs and to validate that the software works as expected.  Generally speaking this works okay, but we’ve all used applications and operating systems where this testing approach clearly hasn’t worked well enough.

With the critical systems on which Galois focuses, you can’t afford to have bugs, or at least certain kinds of bugs, and it’s more important than ever that the software runs correctly.  Since conventional testing techniques are clearly not always up to the task, one approach we take is to use is formal verification (FV) tools and techniques.   FV approaches include constructing mathematical proofs that the software always acts according to a precise behavioral specification.

I don’t think I’m going out on a limb to say that to folks other than highly-trained FV experts, that last sentence doesn’t sound like a fun way to spend your time. The Crowd Sourced Formal Verification (CSFV) program, sponsored by the Defense Advanced Research Projects Agency (DARPA), gives us a rare opportunity to combine abstract computer science concepts with software that is fun for anyone to use.  It’s also the source of another kind of fun for us, in that we get to collaborate with our voidALPHA partners whose skills in game design and implementation are a great complement to the skills we provide.

Here’s a high level view of how StormBound works, from the FV perspective.  First we figure out the properties of the system we want to prove.  Think of these properties as statements that are either true or false.  Our goal is to ensure that a program does not contain a certain kind of errors, which are the source of common security vulnerabilities.   For example, if a program contains errors in the way it works with the computer’s memory, it may be susceptible to what are called “code injection attacks,” which can be used to spread viruses and other malicious software. 

Based on our knowledge about the common sources of errors we are trying to prevent, we select certain code points in the program source code where we need to check that a property we care about is in fact true. I’ll not go into great detail about how these selections are made, but for those who are interested: in the memory manipulation example we could imagine that the code points would include places in the program where memory accesses occur, and the property of interest ensures that the memory manipulation is valid (e.g., we are not accessing data outside the memory allocated for an array).

Unfortunately, in a typical program there are a lot of these code points, and it is not always easy to find the exact property that needs to hold at each point.  It turns out this is where StormBound players can help, so bear with me as I explain how.

We run the system a whole bunch of times in a variety of scenarios that are intended to exercise the system as it would be exercised in real-world use.  As we run the system all these times, we collect snapshots of the data that is in the computer’s memory, every time the program gets to one of the code points we identified.

This provides us with a large collection of examples of the data in the computer’s memory. Now, we want to identify some things in common about the data at each code point, every time that same code point is reached while running the program.  These things in common are in fact the kinds of properties we are looking for. And here’s an important bit: it turns out that computers aren’t always good at finding these “things in common,” but human beings are very adept at finding patterns, especially visual patterns. 

This is where the StormBound game comes in.  Each game level actually consists of the data that was in memory all the times a particular code point was reached.  When you play a level, you are looking for common patterns in that data.  The game shows you the data (in what we think is a fun and visually appealing form), and allows you to “experiment” with the data in various ways, to help you to find those common patterns. The spells you cast in StormBound describe the patterns.  In the FV world we call these spells assertions.  We combine together the assertions discovered by many players of the same game level, which enables the FV tools we use to prove the truthfulness of the desired properties at the corresponding code point.  Not every assertion discovered by game players is in fact useful to help prove the properties, but that’s okay—as long as lots of players are playing the game, they’ll eventually find and tell us all the assertions we need to do the formal verification work. 

And that’s where you come in.  Please join the crowd playing StormBound!

Approved for Public Release, Distribution Unlimited