Thesis Committee:
Edmund Clarke, Chair
Randal Bryant
Todd Mowry
Ken McMillan
Natarajan Shankar
As hardware components become more and more complex, the task of formally verifying them also becomes increasingly difficult. The two major streams of verification approaches, Model Checking and Theorem Proving, have long reached their limitations as general-purpose techniques, and most of the research now is concentrated on efficient specialization of both approaches to relatively narrow problem domains. There are a host of such special-purpose techniques developed both in model checking and theorem proving communities that often allow formal verification to be applicable to amazingly large and complex systems.
The never-ending growth of the complexity of modern hardware and software systems requires more and more sophisticated methods of verification. The state space explosion problem leaves little hope for automatic finite-state verification techniques like Model Checking to remain practical, especially when designs become parameterized. The use of Theorem Proving techniques is inevitable to cope with the new verification challenges. ``Pure'' Theorem Proving, on the other hand, can also be quite tedious and impractical for complex designs. Ideally, one would like to find an efficient combination of Model Checking and Theorem Proving, and the quest for such a combination has long been one of the major challenges in the field of formal verification.
Many new methodologies have been proposed to make the two techniques work in ensemble. Observing such a wide variety of methodologies, one may even question the mere possibility of finding a universal technique that would combine model checking and theorem proving. Instead, it seems more practical to expand the collection of these problem-specific methodologies.
The development of new methodologies is usually an iterative experimental process in which researchers implement their ideas in a prototype tool and run several verification examples in it. The experiments provide the necessary feedback for refining the methodology and generalizing it to handle wider class of examples, or give hints on how to tune the technique to specific applications.
Since the methodologies often use both model checking and theorem proving techniques, implementing new tools becomes the main bottleneck in the their development. In this work, we provide a new unified framework that includes both model checking and theorem proving, and is designed for fast prototyping or manual but computer-assisted testing of new verification methodologies. The tool SyMP (Symbolic Model Prover) implements this methodology in a theorem prover-like environment. Moreover, the tool is in fact a programmer's kit for generating new, possibly highly specialized, theorem provers. It provides a basis for the development of new tools which support emerging methodologies, and reduces the implementation time. The architecture of the tool and the theory behind it help to organize the new methodologies in a systematic and extensible way.
There has been quite a number of different methodologies proposed in the past few years to help overcome the drawbacks of ``pure'' model checking and theorem proving. Some techniques augment model checking with new state reductions, others provide meta-reasoning to simplify the model before running a model checker on it. In theorem proving, a very ubiquitous and conceptually simple technique is to add a model checker as a decision procedure to discharge finite-state subgoals. Many other methodologies help to systematize the proofs, so they become smaller, more manageable, and even more automatic. Yet a few methodologies tackle the very problem of combining model checking and theorem proving techniques at a rather general level.
Below we briefly describe some of the most common verification methodologies. Our claim is that they can all be expressed in our new framework without any loss of generality, and more importantly, without much loss of efficiency. The latter is a very important point - after all, anything in formal verification can in principle be expressed in Higher Order Logic (HOL), and therefore, done in a pure theorem proving environment. But in practice, this often comes at a very high cost of losing efficiency. Therefore, keeping the efficiency and the degree of automation is an important factor in our contribution.
Cone of Influence is a very straightforward but effective state reduction technique. Before running a model checker on the model, one finds the set of variables that can potentially affect the specification, and removes all the other variables from the model. The dependency is computed by first taking the variables that directly occur in the specification, adding to this set those variables that appear on the right hand side of the assignments to the variables already in the set, and doing this repeatedly until no new variables can be added.
When the original model has symmetric components (e.g. an array of caches in a shared memory protocol), it is often possible to reduce the number of these components by reordering them dynamically. This way we can force the components that influence our specification to be always some particular selected components. Since the other components will not be important, we can then remove them from the model.
Alternatively, when the model is too large or even infinite, one may use abstraction to reduce the size of the mode. Some constraints are removed from the original model and replaced by nondeterminism, making the model smaller (it has fewer constraints on the transitions), but with ``more behaviors,'' so that the abstract model has more ways of reaching erroneous states. Therefore, if a safety property is true in the abstract model, then it must be true in the original model as well.
Assume-Guarantee Reasoning is a variant of compositional reasoning when some properties are proven for each of the component, and then the property of interest is derived for their parallel composition. The properties of some components are proven under certain assumptions about other components, and then those components are proven to guarantee these assumptions.
The reduction techniques mentioned above come mostly from the model checking world. We now discuss some of the verification techniques from theorem proving.
From the point of view of temporal specifications, there are two types of induction that can be applied. One is induction on time, and the other is induction on the data structures.
Safety properties in theorem proving are often proven by induction on time. First, one proves that the property holds in the initial states (the base of the induction), and then, assuming that the property holds in some arbitrary state, one proves that all the states in its transition image also satisfy this property (inductive step). Since the original property is rarely inductive (not strong enough to satisfy the inductive step), it is often necessary to strengthen the invariant before it can be proven, and this is usually the hardest and the least automatic step in the verification. Nowadays there are a few tools that help compute inductive invariants automatically.
While proving properties about complex or infinite data structures, one may need to use natural or structural induction within the current state of the system.
A combination of assume-guarantee and induction on time yields the so-called ``circular'' compositional reasoning. In some systems with tightly coupled components, the dataflow goes back and forth among the components, and to prove the guarantees of one module, we need to assume some properties about the other, and vice versa. The classical assume-guarantee rule does not work in this case, since we cannot break the cyclic dependency. However, we can require that the assumptions about the other components be considered only up to time t while proving the property at time t+1 . The base of this induction is, as usual, to show that all the guarantees are satisfied at time t=0 , and then the actual assume-guarantee reasoning proves the inductive step.
Symbolic simulation is a method of ``running'' a hardware device or a software program with symbolic inputs (terms) instead of concrete bit values. The result is a term built from these inputs and functions that the design applies to the inputs when it executes. The concrete functions in the design are often replaced with uninterpreted functions, both for efficiency and generality. Interpretations of the resulting term represent possible outputs that the device may produce. The properties of interest are then proven directly on the result term, usually automatically, using decision procedures for uninterpreted functions with equality like SVC.
If the above methods are generally applicable to virtually any type of a model, the method of completion functions has been developed with the focus on pipelined and superscalar microprocessors. The idea is to prove the Burch and Dill commutative diagram using special user-defined function that computes the state of the microprocessor after flushing it from the current state. When these functions are simpler than the direct flushing of the machine, the verification can be done much easier. However, the user has to provide the completion functions manually, and these functions must be proven to be equivalent to the direct flushing, which is an additional overhead of the method.
Our contribution to the field of formal verification is two-fold. First, we have developed a framework for combining model checking and theorem proving in such a way one does not dominate the other, and all of the main advantages of both techniques are preserved. The resulting system, therefore, has the same expressive power as a theorem prover, but at the same time enjoys the same degree of automation and speed as the state-of-the-art model checkers for finite-state part of verification. In addition, many powerful transformations can now be included into the system that were not directly present in any ``pure'' model checker or theorem prover, such as induction on time or various types of abstraction.
Second, we have extended the notion of theorem proving from how it was traditionally accepted in formal verification to a more abstract one which allows us to specialize it very efficiently to a wide range of specific problem domains. In particular, the framework for combining model checking with theorem proving becomes one such specialization. We have also built a tool called SyMP (stands for Symbolic Model Prover) that supports this extension of theorem proving, and in effect, is a theorem prover generator, or a programmer's kit that simplifies the task of building new theorem provers for various specific problem domains. To date, this tool has been tested on four problem domains: combination of model checking and theorem proving for hardware verification, security protocol analysis using the Athena approach, verification of C programs in the Reedpipe proof system implemented by Daniel Kr\''oning, and an emerging combination of Presburger arithmetic with a bitvector theory based on Verilog operations. One more proof system is being started that will be a re-implementation of Analytica theorem prover, originally implemented in Mathematica.
In a nutshell, our framework is simply a theorem prover based on a
special-purpose proof system. Since the problem we are solving involves
a complex model and a usually relatively simple property, the sequent
in this proof system includes the model explicitly, and otherwise
can be thought of as a Gentzen sequent. In its simple version, it
can be written as follows:
|
The inference rules include all the rules similar to the ones in the
classical Gentzen proof system for the higher-order logic, and contain
additional rules that operate on the model and the modal operators
of the logic. For example, model checking as a decision procedure
can be introduced as a rule:
|
|
The advantages of such a system are not only in the fact that model checking and theorem proving can be used at the same prompt. The proof rules can now be constructed specifically for the transformations that one uses most often in hardware verification. Besides the model checking procedure and the cone of influence reduction (which are already atomic rules at this point), we can add various abstractions, case splitting, circular reasoning. etc. as atomic rules. Now, when the user outlines the verification plan for his example, he can then simply apply the appropriate rules that correspond one-to-one to the high-level steps in the outline on the paper. This means the verification itself can be done on a higher level, the proofs get simpler, and more low-level steps are performed by the tool automatically inside the high-level rules, compared to the traditional theorem proving.
The proof system that we actually use has many other powerful proof rules, a slightly more complex sequent, and it operates on full branching time and linear time μ-calculus.
As we have already mentioned, most of the advances in formal methods are done by designing new verification methodologies for specialized problem domains. Often, these new methodologies are based on existing, ``traditional'' approaches and corresponding tools. In practice, however, the available techniques and their implementations often present intrinsic problems that significantly slow down the development of new verification methods. These problems stem mostly from the artificial standards imposed on researchers in both model checking and theorem proving by various factors ranging from the stereotypes in the foundations to implementation artifacts in the tools.
If we take one more look at the previous section, the reason we can achieve a combination of model checking and theorem proving is quite simple in its root: we use a custom sequent and a specialized proof system for our specific problem domain, as opposed to using an ``all-in-one'' proof system of an off-the-shelf general purpose theorem prover. A natural question arises whether we can apply a similar approach to other problem domains than hardware verification. While designing the architecture of our tool SyMP, we conjectured that allowing the tool to work with arbitrary sequents and proof systems would greatly increase it versatility.
To test this conjecture, we have developed a general purpose prover generator kit that takes a data structure for the sequent and a proof system as a parameter, and generates an interactive theorem prover with a user interface and a proof management (keeping track of the proof tree, editing the proof, automated proof search using strategies, etc.).
Our first proof system, of course, was the one described above for combining model checking and theorem proving, which fits very nicely in the framework. But for testing our conjecture, we needed at least one more example of some clearly different problem domain. We picked security protocol verification, since it is about as far from hardware verification as one can get in formal methods, and, moreover, it has very little to do with traditional notions of theorem proving and model checking. If this problem domain can be efficiently implemented in our tool, then most likely many other domains not as alien to theorem proving have a good chance of finding their place in SyMP too.
Our proof system of choice for security protocols became Athena, a verification methodology originally developed by Dawn Song based on the strand space model, and later reformulated in our joint work as a specialized proof system. Athena implementation in SyMP was developed quite fast (about 2 person-months total of actual effort), and the result was a very efficient automatic theorem prover highly specialized to security protocols, and with an option of interactive user guidance with a convenient interface. The automatic proof search is comparable in speed and efficiency to the original implementation of Athena by Dawn Song upto some constant factor due to the overhead for the proof management and the interactive user interface.
We believe that the success of our implementation of Athena strongly supports our conjecture that theorem provers parameterized by customized proof systems can be much more versatile and efficient than conventional ones. The implementation of two more proof systems, Reedpipe for verification of C programs and Bitvector that combines bitvector theories with Presburger arithmetic, also show a lot of promise. Another proof system Analytica is also emerging, which was originally a stand-alone theorem prover implemented in Mathematica, and specialized in elementary analysis.
The notion of a special-purpose proof system is, of course, not new, and has been studied in the field of Automated Deduction quite extensively, resulting, in particular, in a creation of Logical Framework. Logical framework (LF) can be viewed as a way to specify the sequent and the inference rules of a user-defined proof system, and letting a tool search for proofs automatically, or build a custom theorem prover for this proof system.
The difference between our approach and LF is that LF provides the user with a fixed language for defining the proof system, and usually has limited expressive power (on purpose) to ease the automated proof search and make use of certain theoretical results that apply to such a language to increase the efficiency. In addition, the specification language is also usually fixed by LF. This is not a problem for various forms of the first- or higher-order logic, or similar formalisms, but can be quite restrictive in many other problem domains. In fact, both our proof systems (model checking + theorem proving and Athena) cannot be efficiently expressed in LF.
In contrast, we let the proof system developer use the full power of SML (general-purpose programming language, and the implementation language of SyMP) to express his or her sequents and rules. The result is, perhaps, not as automatic a prover as it can be with LF, but it is much better catered to the problem domain, and has an interactive mode which is invaluable for designing verification methodologies in the new fields, where the only available approach is by trial and error. Implementing a proof system in our framework might be more difficult than in LF, since it is done on a lower level, but the advantages of the resulting tool are often worth it, as we have seen from our experience in developing the two proof systems.
As we have already mentioned, our work consists of two most important contributions. First, we have shown that Model Checking can be efficiently combined with Theorem Proving in a way that sacrifices neither efficiency of the former, nor the expressiveness of the latter. We call this combination Model Proving. One of the important lessons that we learned is that such a fusion must be specific to the problem domain, and not too general, otherwise the efficiency is very hard to preserve. To address this issue, we have developed a framework for generalizing theorem proving (as it is usually accepted in the formal verification community) to arbitrary but narrow enough problem domains. This framework, along with its implementation in our tool SyMP, comprises our second major contribution in this work.
Although there has been much work in combining model checking and theorem proving in formal verification, we have not seen any results providing a general enough theory unifying both techniques without loss of expressiveness and efficiency. The latter is a very important aspect, since, theoretically, anything can be expressed in the Higher-Order Logic, but very often in practice, working with such an encoding is virtually impossible. For instance, the simplest and most widely used method of adding model checking to theorem proving framework is to add a model checker as an external decision procedure in a special inference rule. The model is extracted from the sequent with the help of some heuristics or by matching certain formula formats for which the translation is easy. Many HOL-based theorem provers use this approach: PVS, ACL2, HOL, etc. This approach suffers from two drawbacks: first, the original structure of the model is lost, and often cannot be recovered and used to simplify the verification. Second, very often model checking is used only as a direct decision procedure for finite-state models to prove the current subgoal, and a plethora of reduction techniques developed in model checking is simply omitted in the hope that they can be done with the existing theorem proving techniques.
Another theorem prover, STeP, uses a similar idea in spirit, but more sophisticated in detail. Since STeP uses first-order LTL as a logic, the original model can be encoded in this logic and later extracted rather precisely in the model checking inference rule. Besides, other transformations that are usually attributed to model checking can be done efficiently (e.g. abstraction). However, STeP is highly specialized to software verification, its proof system is tightly integrated into the core of the tool, and therefore, it is not as general and flexible as our framework.
On the model checking side, the situation is almost reversed, but with the same overall effect. Whenever theorem proving techniques are added to a model checker, they usually stand separately, and often can only be activated at a ``preprocessing'' stage before the main model checking run. In addition, the theorem proving add-ons almost always consist of a fixed set of rules applied completely automatically, and therefore, not as adaptive to the problem domain or a particular problem as an interactive one.
One of the most often used reductions in model checking that may require some theorem proving capabilities is abstraction. In fact, it is used in the model checking context so often that it has become a standard practice and an integral part of the model checking process. Many tools apply abstraction to reduce the model to a manageable size and then run a model checking engine directly on the abstracted model. The theorem proving component here is to derive that if a property holds in the abstracted model, then it must hold in the original model. As it is, this ``inference rule'' is implemented only implicitly by checking the applicability conditions and abstracting the model. A few model checkers implement more theorem proving rules: assume-guarantee reasoning (Mocha), induction, case split, and use of lemmas (SMV), and so on. However, all these tools still have the set of rules hard-wired into the structure of the implementation. This makes them very specialized to a particular problem domain where they can be extremely efficient, but they perform poorly outside of it.
In our framework, the inference rules are always defined explicitly, and the user has a control in the amount of automation while applying these rules. In particular, if the automated verification goes terribly wrong, there is an option to guide it manually. Also, an explicit notion of an inference rule provides better modularity, and new reductions and transformations can be added easily and systematically.
Another practical advantage of using this framework is the appropriate level of abstraction of the user interface with the tool. When the proof system is designed specifically for the problem domain, the actual proofs in the tool correspond very closely to their mathematical description. For example, the proofs for the IBM cache coherence protocol correspond almost exactly, both in the level of abstraction and in the sequence of steps, to the proofs in the default proof system of our tool SyMP. Given the original model description, one can easily repeat the proofs in SyMP while reading their description with little extra work. Moreover, the proof of the coherence property can be done using just theorem proving techniques or using more model checking-oriented methodology. We have essentially repeated PVS proofs step by step in SyMP without any difficulties, and then proved the same property by agressive use of abstraction and model checking closely following the SMV proof discovered by Ken McMillan.
Our second contribution is closely related to the ways the research is carried out in formal verification. This research area is very experimental, and new methodologies must be implemented and tested on real examples. Whenever a researcher comes up with a new methodology, he or she always faces a design decision of how to implement it. Development of formal verification tools is often an arduous process, and one of the big reasons for developing very general tools is an attempt to capture as many aspects of formal verification as possible in one single implementation. The experiments then can be carried out in such a tool as soon as one provides an encoding of his or her verification problem in the supported specification language. The other extreme that is often taken is to develop a new highly specialized tool for each problem domain or even each methodology, which results in a very efficient but not as flexible implementation.
Our experience with several tools both from model checking and theorem proving indicates that only sufficiently specialized ones can be very efficient in practice, and very general solutions quite often fail to exploit the shortcuts and powerful reductions particular to certain classes of examples, because what works great in one problem domain may be making things worse or even be unsound in another. But instead of writing yet another highly specialized tool or using a very general one, we decided to choose the middle-ground. We have designed and implemented our tool SyMP as a general framework for creating specialized verification modules. Therefore, although the tool itself is very general, we solve the problem of efficiency by adding modules specialized to different problem domains. That is, unlike in the other tools, there can be many different specializations in SyMP at the same time, which makes our framework and the tool versatile.
Despite the differences in techniques and representation, there are still quite a bit of common features in the process of formal verification that can be used in virtually any problem domain, and the most important ones are the proof management mechanism and the interactive component of the user interface. This is not surprising, since whatever we are proving, we would like our proofs to be complete; and almost any proof can be formalized in a suitable proof system. Therefore, a tool that serves as a basis for specialized proof systems and provides this common functionality can significantly reduce the implementation time of new verification methodologies, and this comprises our second major contribution in this thesis. To date, we have not yet seen a tool or a library providing similar functionality.
The idea of a generic tool for implementing custom proof systems is not new, however. Logical Framework has been developed in the area of Automated Deduction, and is one of our most closely matching competitor. However, most of the implementations of the logical framework require that a custom proof system be expressed in a fixed input language of the tool, and although it often provides powerful automated proof search for each new proof system, it is again only efficient for the problem domains that can be adequately expressed in the provided language. In particular, none of the proof systems implemented so far in SyMP can be efficiently encoded into the Logical Framework.
Customized proof systems in SyMP can be used not only for theorem proving-based methodologies, but also as a way to house several existing tools under one roof. This can be done at different levels: within the same proof system, and across different proof systems. For instance, SyMP already uses the CMU version of SMV as a decision procedure in the default proof system, and at the same time another proof system is being developed that consists entirely of an interface to an external prover written in C++. This type of combination provides the common user interface to different applications for different problem domains, but it does not allow these tools to communicate with each other. Another possibility is to use external tools as decision procedures or processing filters in different inference rules of the same proof system. This forces the output of the tools to be translated into the common sequent representation (which is only fixed for a particular proof system, and can be different in the others), and passed to another tool.
Similar idea has been proposed at SRI several years ago as a SAL project. One of the central goals was to develop a universal language that can be used as an intermediate representation in virtually any problem domain. External tools would be communicating among each other through this language, and adding a new tool would only require writing translators to and from SAL for that tool. As in any other general approach, the bottleneck of SAL is the intermediate language itself. In our opinion, it is impossible to come up with a universal representation that would work efficiently for every problem domain. Therefore, SAL will most likely be successful only for some problems that it can express elegantly and adequately.
In SyMP, we deliberately did not commit ourserves to any particular specification language or intermediate representation. This, of course, adds some work for the developers of new proof systems, but each proof system then can have its own common representation most suitable to the problem domain, and at that point the situation is similar to the original idea of SAL: each new external tool only needs a small translator to and from the common sequent representation, but this time the sequent is optimized to the problem domain, and overall, we hope that SyMP can bridge more tools and more efficiently than SAL and similar projects.
There is still a lot of work to be done in this project, most of it is related to the development of our tool SyMP. First of all, the default proof system is far from being complete. The idea of this proof system is to provide a very general framework that includes model checking and theorem proving together. Ideally, we would like to see most of the existing theorem proving rules and model checking reduction techniques implemented in it.
The reason we want to be very general in this case is to be able to provide a quick prototyping environment for new verification methodologies. In research, at the time of trying out a new idea, the efficiency usually is not a big issue, and researchers often prefer a quick feedback, even at the expense of tedious manual guidance and not very natural encoding of the problem. This is what the default proof system should provide: a research-oriented prototyping environment for methodologies that require both model checking and theorem proving techniques. One would be able to use virtually any existing reduction technique and the full deductive power of a theorem prover to run through several examples, and then decide which reductions were crutial to their methodology, and what was the bottleneck. Later, when the new methodology is thoroughly tested, another specialized proof system can be developed that carries out the verification process much faster and more automatically for that specific class of problems.
Adding new proof systems to our tool is another dimension of its growth. SyMP has already proven to be a very convenient basis for the two proof systems developed in it (the default one and Athena), and there are three more projects going on at the time of writing that will add a reimplementation of Analytica, a new prover module Reedpipe specialized in arithmetic hardware circuits is being written in C++, and a prototype of a decision procedure for a combination of Presburger arithmetic and a Verilog-like bitvector theory.
In the future, more modules will be added to cover other specific
areas of formal verification. For instance, there are some thoughts
about adding a module for software verification. It is quite possible
that in a few years SyMP will become a powerful tool capable
of efficiently solving many formal verification problems in a wide
range of problem domains.