Verification, Model Checking, and Abstract Interpretation

Information security has benefited from mathematically cogent modeling and analysis, which can assure the absence of specific kinds of attacks. Information security provides the right sorts of problems: Correctness conditions may be subtle, but they have definite mathematical content. Systems may be complex, but the essential reasons for failures are already present in simple components. Thus, rigorous methods lead to clear improvements.

Initiating from the seminal work of Volpano and Smith, there has been ample evidence that type systems may be used to enforce confidentiality of programs through non-interference. However, most type systems operate on high-level languages and calculi, and “low-level languages have not received much attention in studies of secure information flow” (Sabelfeld and Myers [16]). Further, security type systems for low-level languages should appropriately relate to their counterparts for high-level languages; however, we are not aware of any study of type-preserving compilers for type systems for information flow.

In answer to these questions, we introduce a security type system for a low-level language featuring jumps and calls, and show that the type system enforces termination-insensitive non-interference. Then, we introduce a compiler from a high-level imperative programming language to our low-level language, and show that the compiler preserves security types.

Typed Assembly Languages (TALs) can be used to validate the safety of assembly-language programs. However, typing rules are usually trusted as axioms. In this paper, we show how to build semantic models for typing judgments in TALs based on an induction technique, so that both the type-safety theorem and the typing rules can be proved as lemmas in a simple logic. We demonstrate this technique by giving a complete model to a sample TAL. This model allows a typing derivation to be interpreted as a machine-checkable safety proof at the machine level.

Polygonal hybrid systems are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. Here, we identify and compute an important object of such systems’ phase portrait, namely invariance kernels. An invariant set is a set of initial points of trajectories which keep rotating in a cycle forever and the invariance kernel is the largest of such sets. We show that this kernel is a non-convex polygon and we give a non-iterative algorithm for computing the coordinates of its vertices and edges. Moreover, we present a breadth-first search algorithm for solving the reachability problem for such systems. Invariance kernels play an important role in the algorithm.

A reactive system does not terminate and its behaviors are typically defined as a set of infinite sequences of states. In formal verification, a requirement is usually expressed in a logic, and when the models of the logic are also defined as infinite sequences, such as the case for LTL, the satisfaction relation is simply defined by the containment between the set of system behaviors and that of logic models. However, this satisfaction relation does not work for interval temporal logics, where the models can be considered as a set of finite sequences. In this paper, we observe that for different interval based properties, different satisfaction relations are sensible. Two classes of properties are discussed, and accordingly two satisfaction relations are defined, and they are subsequently unified by a more general definition. A tool is developed based on the Spin model checking system to verify the proposed general satisfaction relation for a decidable subset of Discrete Time Duration Calculus.

Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models where the system state contains mutable function and predicate state variables. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the function state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol with unbounded FIFO channels.

Given a finite-state abstraction of a sequential program with potentially recursive procedures and input from the environment, we wish to check statically whether there are input sequences that can drive the system into “bad/good” executions. Pushdown games have been used in recent years for such analyses and there is by now a very rich literature on the subject. (See, e.g., [BS92,Tho95,Wal96,BEM97,Cac02a,CDT02].)

In this paper we use recursive game graphs to model such interprocedural control flow in an open system. These models are intimately related to pushdown systems and pushdown games , but more directly capture the control flow graphs of recursive programs ([AEY01,BGR01,ATM03b]).

We describe alternative algorithms for the well-studied problems of determining both reachability and Büchi winning strategies in such games. Our algorithms are based on solutions to second-order data flow equations, generalizing the Datalog rules used in [AEY01] for analysis of recursive state machines. This offers what we feel is a conceptually simpler view of these well-studied problems and provides another example of the close links between the techniques used in program analysis and those of model checking.

There are also some technical advantages to the equational approach. Like the approach of Cachat [Cac02a], our solution avoids the necessarily exponential-space blow-up incurred by Walukiewicz’s algorithms for pushdown games. However, unlike [Cac02a], our approach does not rely on a representation of the space of winning configurations of a pushdown graph by (alternating) automata. Only “minimal” sets of exits that can be “forced” need to be maintained, and this provides the potential for greater space efficiency. In a sense, our algorithms can be viewed as an “automaton-free” version of the algorithms of [Cac02a].

Java is a very successful programming language which is also becoming widespread in embedded systems, where software correctness is critical. Jlint is a simple but highly efficient static analyzer that checks a Java program for several common errors, such as null pointer exceptions, and overflow errors. It also includes checks for multi-threading problems, such as deadlocks and data races. The case study described here shows the effectiveness of Jlint in finding certain faults, including multi-threading problems. Analyzing the reasons for false positives in the multi-threading warnings gives an insight into design patterns commonly used in multi-threaded code. The results show that a few analysis techniques are sufficient to avoid almost all false positives. These techniques include investigating all possible callers and a few code idioms. Verifying the correct application of these patterns is still crucial, because their correct usage is not trivial.

A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs, commonly called worst-case execution times (WCET). The task solved by abstract interpretation is to verify as many local safety properties as possible, safety properties who correspond to the absence of “timing accidents”. Timing accidents, e.g. cache misses, are reasons for the increase of the execution time of an individual instruction in an execution state. This article attempts to give the answer to the frequently encountered claim, “one could have done it by Model Checking (MC)!”. It shows that it is the characteristic property of abstract interpretation, which proves AI to be applicable and successful, namely that it only needs one fixpoint iteration to compute invariants that allow the derivation of many safety properties. MC seems to encounter an exponential state-space explosion when faced with the same problem. ILP alone has also been used to model a processor architecture and a program whose upper bounds for execution times was to be determined. It is argued why the only ILP-only approach found in the literature has not led to success.