Verification of Erlang Programs

Thomas Arts
Computer Science Laboratory, Ericsson Telecom AB,
thomas@cslab.ericsson.se

Dilian Gurov, Mads Dam, Lars-åke Fredlund
Swedish Institute of Computer Science,
{dilian, mfd, fred}@sics.se

Introduction

One of the major concerns of most programmers is to produce bug-free programs. Bug-free is a vague notion if you have not described how the program should behave. With a wishlist of the demanded behavioural properties we are, however, able to state that the program does or does not behave correctly. A behavioural property should be stated in a specification language which is precise enough to allow rigorous treatment. Having specified a certain property, the big question is: how can we make sure the program has this property?

First of all, we may obtain trust in a program's correctness by examining the way the program is written, and by the experience of its programmer/designer. However, the more complex the programs get, the easier it is to overlook a flaw in the program. Therefore, secondly, a program is tested as exaustively as possible. Testing a program means that you take a certain configuration of the program and its environment and that for this configuration you run the program and see what happens. The more configurations you try, the more you believe that you have covered the program behaviour in general. Since most programs have infinitely many configurations to start with, testing implies that you might have overlooked that configuration that is causing your program to fail.

If we are able to formulate the property that we want the program to meet in a very precise, mathematical way, then we can use verification techniques to actually prove that the property holds for all possible configurations.

Verification

The aim of our project is to develop a method for verification of rather general properties of arbitrary distributed and concurrent Erlang programs. In particular we focus on developing a tool such that large parts of the verification process can be handled automatically.

Before one can prove anything about a program, one has first to make clear what to prove, which then should be formalised. This specification process involving "deep thinking" turns out to be probably half as effective as the actual verification. By explaining yourself, or better, a colleague what you did and why it should work correctly, many serious mistakes and pitfalls show up.

After that it has become clear which property of the program should be verified, one can consider using our verification technique. For using this technique we have designed:

a formal language, based on a temporal logic called the modal mu-calculus, in which to state the properties,
a proof system, consisting of a set of proof rules, for reasoning about program correctness, and
a tool that assists and partially automates the latter reasoning.

In our approach we focus on verifying programs written in Erlang. In contrast to several other approaches, this results in a method in which one can directly read in and work on an Erlang program, instead of abstracting from it in a different language. As a consequence, we really verify the program and not an abstraction of it. The price to pay, of course, is that we have to consider more details in our verification.

In the formal language, we directly address the Erlang primitives and the Erlang processes. Additional logical connectives and quantifiers enable us to express properties like:

Given a list X, the evaluation of the term length(X) terminates and results in an integer.
The process P1 can only send messages to process P2 and P3.
Given processes P1 ... P5 in a ring, if process P1 continuously sends 0 to process P2, then eventually P5 sends 0 to P1.

The propery that we want to prove about a program is called a goal and a proof consists of reducing a goal to subgoals and recursively applying this technique until every subgoal is a trivial fact. One can view this as building a tree, where all the nodes are subgoals and the leaves of the tree represent simple facts or axioms.
The difficulty is of course to reduce the goal into subgoals, such that in the end we end up with something trivial. We developed a set of approximately 50 proof rules that, depending on the form of the goal, can be used to devide a goal into subgoals. Often several of these proof rules are applicable to a certain goal and the hard part is to choose the right one.

The tool we have built enables to apply the proof rules to a certain goal, where the user has to choose the proof rule that should be applied. In order to partly automate this, and in order to obtain a higher level of abstract reasoning, several heuristics have been developed that help the user in the hard task of choosing the right rules. For keeping an overview of what is proved and which subgoals are still open, the proof can be visualized by the daVinci graph manipulation tool, developed at the university of Bremen.

Case studies

We used the verification tool for proving some interesting properties of several small programs. In order to give an impression of what is feasable by using the tool, we describe our two major examples.

Billing agent

In this example we want to verify some security properties that deal with buying something via the Internet. In our simplified example, we consider the software that enables a user to access a resource from the Web paying for this resource via a virtual bank. The user issues a request to a resource manager which responds by dynamically creating a billing-agent process. The billing agent acts as an intermediate between the user, the resource owner, and the bank with the account of the user.
The billing agent asks the user for a secret account number and the resource owner for the resource. The billing agent makes sure that the money is transfered from the account of the user to the account of the owner of the resource, and only than hands over the resource to the user.

The user is clearly taking a risk by exposing the account number and so is the resource owner by giving away the resource before any money has been payed. The software written for performing these tasks should be trusted. Both the user as the resource owner, and probably even the bank want to be sure that the software meets certain security criteria. Typical properties that have been verified for this example are: (a) the number of transfers from the user account does not exceed the number of requests to use the resource; and (b) the billing agent does not communicate the user-account key to any other party than the bank.

Query binding in Mnesia

In the kernel of the code for the Mnesia database management system there is some code for setting up a query. The query is devided in sub-queries and those sub-queries are distributed over the network. A request for retrieving data according to such a distributed query results in starting a certain protocol that sends a message to the first sub-query, which gathers part of the information, passes that to the next sub-query etc. Eventually, the last sub-query sends answers back to the original process, which may ask for more data if required.

Typical properties to verify here are those concerning the termination of the search, and the guarantee that all data that should be found eventually arrives.

Conclusion

Verification of software can provide more robust software, and in particular, it can provide assurance about certain properties that the software fulfils. Experiments with the prototype of the verification tool demonstrated that interesting properties can be proved, but at the same time taught that the functionality of the tool is not yet sufficient for addressing verification of properties of large programs. The problems that we have encountered during our experiments are addressed in the next version of the tool, which is currently being developed. The techniques are scaleable, and we hope to be able to check properties of larger complexity with the forthcomming tool.