Prof. Robert Stärk

A Logic for Secure Memory Access of Abstract State Machines

How can we formally prove that all memory accesses of a program are permitted? How can we show that high-performance C code like a network filter is memory safe? How can we use formal methods to prove that applets on a smart card are isolated and do not read critical locations of each other? How can we safely eliminate array bound checks and null pointer checks in Java programs? --- An attempt to solve such problems with standard programming logics like Hoare logic or dynamic logic will immediately fail, since the problems have to do with memory access and it is not even possible to formulate memory access properties of programs in these logics. For example, a simple property of a sorting algorithm, like that when sorting the subarray in the interval from l to r the algorithm reads array elements a[i] with index i between l and r only, cannot be proved in these logics, since the property cannot be expressed in the formal language of the logics.

We therefore extend our logic for Abstract State Machines by a read predicate that allows to make precise statements about the accesses of locations of an ASM. The logic can be used to prove security properties of ASMs like that the machine does not read locations containing critical information or that all accesses of the machine to the abstract memory are permitted. The logic is sound and complete for hierarchical ASMs without cycles in the call graph and it is sound for turbo ASMs with possibly recursive rule declarations. It is integrated in the AsmKeY theorem prover, an extension of the KeY system developed at the University of Karlsruhe for modeling, specifying and verifying object-oriented programs, in particular JavaCard programs.

The new read predicate of the logic for ASMs is also useful for proving refinements of parallel ASMs to sequential C-like programs. Assume that two ASMs P and Q run in parallel. If one can show that Q does neither read nor update locations updated by P, then the parallel composition of P and Q is equivalent to the sequential composition, first P then Q, with respect to memory accesses and updates.

What are Abstract State Machines?

The states of an Abstract State Machine are (finite or infinite) algebraic first-order structures as they are used in mathematics and mathematical logic since almost a century. The structures are understood as a kind of abstract memory. A mathematical term like f(x + f(y)) corresponds to an expression mem[x + mem[y]]. The function f is dynamic and can change its values during a run of the ASM. The value f(x) is the content of the function f at the location x, as mem[x] is the content of the memory cell with address x. Dynamic functions are more general than ordinary arrays. They can be of arity greater than one and their arguments can be of any type not just non-negative integers.

The transition rules of an abstract state machine consist of a finite number of guarded updates which are executed in parallel. Updating a function means putting a new content into a location of the function. Why the parallel composition? Since Gurevich's ASM thesis says that "any computer system can be simulated step-for-step on its natural abstraction level by an Abstract State Machine", an ASM has to be allowed to do some work in parallel, e.g. update a program counter, write data from registers to memory and read the next instruction. Moreover, the usage of parallel composition has the advantage, that the system is never in an intermediate state, where the main invariants of the system are temporarily violated.

ASMs have been successfully used for the specification of systems in several industrial projects (see [1] for a survey). The "Foundation of Software Engineering Group" at Microsoft Research has implemented an ASM based specification language AsmL which is fully integrated into the .NET environment and can be used for run-time verification of C# programs. In our book [3] on Java and the JVM we have used ASMs for a complete specification of the Java programming language, the Java Virtual Machine, a Java-to-Bytecode compiler and a bytecode verifier. During the attempt to prove that the compiler generates verifiable code, we found examples of legal Java programs which can be compiled but are afterwards rejected by the verifier and cannot be executed on the virtual machine.

Formal Methods for Abstract State Machines

When a transition rule of an ASM is evaluated in a given state, it produces a set of updates. If the updates do not conflict, then they are applied to the state and yield the next state in the computation. Hence the change from one state to the next state is fully described by the set of updates. In order to produce the updates, however, a transition rule has also to read some locations of the state. The reading of locations is not observable from outside by looking just at the sequence of states in the computation of an ASM.

In the world of ASMs the states are global states of a system, sometimes also called configurations of the system. It has always been assumed that a transition rule can read every location of the state. Therefore the main focus has always been on function updates and the dynamic change of states. The reading of locations has been considered as not so important.

In our current paper [2] we extend our previous work on a logic for ASMs. The new logic allows to express and prove properties like `the program P does not read the location f(x)' or `whenever program P reads location f(x), then 0 < x < 10'. Thus the logic has a read/access predicate in addition to the already available update predicate. The meaning of the predicate acc(P,f,x) is that the program P accesses (reads) the function f at the argument x, whereas the old predicate upd(P,f,x,y) still means that the program P updates the function f at the argument x to the new value y. The predicate con(P) expresses that P is consistent and does not produces conflicting updates. The logic is designed in a modular way such that a local analysis of a program is sufficient to assess possible vulnerabilities as opposed to a global analysis of all uses of a program.

Literature

[1] E. Börger and R. F. Stärk: Abstract State Machines - A Method for High-Level System Design and Analysis. Springer-Verlag, 2003.

[2] S. Nanchen and R. F. Stärk: A Logic for Secure Memory Access of Abstract State Machines. To appear in: Theoretical Computer Science, 2004.

[3] R. F. Stärk, J. Schmid and E. Börger: Java and the Java Virtual Machine - Definition, Verification, Validation. Springer-Verlag, 2001.