RTLWS: Modeling systems with Alloy

The final day of this year's Real Time Linux Workshop (RTLWS) had talks from a number of different researchers and others from the realtime Linux community. It also featured a talk from outside of that community, but on a topic—as might be guessed—that may be important to users and developers of realtime systems: modeling system behavior for better reliability. Eunsuk Kang from MIT gave an introduction to the Alloy language, which has been used to model and find bugs in systems ranging from network protocols to filesystems.

RTLWS organizer Nicholas Mc Guire prefaced the talk by noting that "Z" is used widely for modeling and design verification, but that there is no free Z support. Alloy, on the other hand, is similar to Z, but is free software. The availability of a free alternative will make this kind of analysis more widespread.

Kang is part of a group at MIT that focuses on how to build more reliable software, which is the motivation behind Alloy. Software design often starts with sketches, then moves into creating design documents in various formats. "Is this the best way to design software?" is one question to ask, he said.

Sketches are good because they are lightweight and informal. That allows people to brainstorm and to quickly prototype ideas. Documents are much more heavyweight and are geared toward completeness. But those documents can't be used to answer questions about the design, nor to determine whether the system design is consistent.

So, they set out to create a new language that is "simple" and would be easy to learn, so it would impose a low burden on its users. It could be used in a step between sketches and design documents. The language would be "precise and analyzable", so that one could ask questions about the system described. The language and tools would provide instant feedback in support of rapid prototyping. That new language is Alloy.

As a demonstration of Alloy and its development environment, Kang created a model of a filesystem in the language. The model consisted of several different kinds of objects, such as files, paths, and filesystems, as well as operations for things like adding and deleting files. The model didn't describe the implementation of the filesystem, just the relationships between the objects—and how they change based on the operations.

The model can then be "run" in the GUI. There is a built-in visualization component, which shows solutions that satisfy the constraints set out in the model. One can add assertions to the model, which can either be confirmed to a certain search depth or a counterexample can be found. Alloy is, in many ways, a descendant of languages like Prolog and automated theorem proving systems.

In the demo, Kang's seemingly reasonable model was missing a key constraint. Alloy was able to find a counterexample to an assertion because the model did not preclude multiple file objects having the same path. Once the add-file operation was changed to eliminate that possibility, no counterexample to the assertion (which essentially stated that the delete operation undoes the add operation) could be found.

Alloy has a small number of constructs, purposely. It is a declarative language that describes the system, but, importantly, not the implementation, in "pure first-order logic". Alloy allows for two different kinds of analysis, Kang said, simulation or assertion. The models get translated into a "constraint solving engine" that can find problems that testing misses.

Standard software testing tries to cover as many different behaviors of the system as possible, but one of its weaknesses is that it can't show the absence of bugs. The analyzer in Alloy is exhaustive, and can be used to "verify very deep properties" about the model, he said. The analyzer allows the designer to "reason about the behavior" of systems.

That kind of reasoning has been done using Alloy, Kang said, both by his group and other researchers and universities. One of his examples was not directly computer-related, instead concerning the beam-scheduling policies for radiation therapy at Massachusetts General Hospital. There are multiple treatment rooms, where several different kinds of requests for radiation from a single cyclotron can be made. There are multiple doctors and nurses making the requests, which get funneled to a master control room that enforces various safety requirements. By modeling the system, several race conditions and other problems were found that had the potential to silently drop requests.

In addition, Stanford and Berkeley have applied Alloy to web security protocols and found previously unknown vulnerabilities in HTML 5 and WebAuth. In fact, researchers using Alloy have found problems in protocols that had previously been "proved" correct. Pamela Zave analyzed the Chord peer-to-peer distributed hash table protocol, which had proofs of its correctness in one of the most cited papers in computer science, Kang said. But Zave found that it is not correct according to its specification, and that six properties believed to be true were not.

There are lots of other examples, he said, including smart card security, the flash filesystem for a Mars rover, and Java virtual machine security. What his group has found is that by using Alloy one will often "find very surprising results". There is ongoing work to generate test cases for the actual implementation from the models to help ensure that the code matches the model. There are also efforts to generate code from the models, but it is a difficult problem.

Going the other way, from existing code to models, is even more difficult. It is far more efficient to start modeling at the design stage, Kang said. The key observation from the team is that spending the time to model a system (or a portion of a larger system) is worth it because it will uncover "a lot of surprises". Those surprises are typically bugs, of course, so finding them—early or late—can only lead to better systems.

[ I would like to thank the RTLWS and OSADL for travel assistance to attend the conference. ]