20.1 Formal Verification Techniques

As in the techniques discussed in previous chapters, formal verification techniques rely on descriptions of the properties or requirements of interest, descriptions of systems to be analyzed, and verification techniques for showing that the system descriptions are sufficient to meet the requirements. The difference between the formal methods and those described in Chapter 17 is the degree of formality of the approach.

Part 3, "Policy," presented a variety of formal and informal security policy models. The formal models are presented in the language of mathematics. This chapter introduces other formal languages, called specification languages, that are useful for representing policies, models, and system descriptions. These languages have well-defined syntax and semantics and are based on a mathematical logic system. This chapter also addresses formal verification techniques that process the formal specifications, determining how well each specification meets the requirements stated in the policy/model or requirements specification. All verification techniques rely on the underlying structure of some mathematical logic system and the proof theory of that logic. Chapter 34, "Symbolic Logic," provides a very brief overview of several logical systems that are used in formal proof technologies and presents fundamental definitions and theories. The reader who is inexperienced in logical systems should review that chapter before proceeding.

Although all formal verification techniques implement similar concepts and approaches, current trends have divided these techniques into inductive verification techniques and model checking techniques. The differences between these two types of techniques are based on the intended use, degree of automation, general logical approach, and underlying logic system. Huth and Ryan [503] provide an excellent set of criteria for classifying verification technologies.

• Proof-based versus model-based techniques. Proof-based techniques define a set of formulas called premises that embody the system description and another formula called the conclusion that represents what is to be proved (the properties). These techniques rely on finding a set of intermediate formulas that allow the verifier to reach the desired conclusion beginning from the premises. Model-based techniques rely on establishing that the premises and the conclusion exhibit the same truth table values.

• Degree of automation. Approaches vary from fully automated to fully manual, with every possibility in between.

• Full verification versus property verification. The system specification may describe an entire system or parts of it, and the property specification may be as small as a single property or may contain many properties.

• Intended domain of application. This may be hardware or software, sequential or concurrent, reactive^[1] or terminating, or other types of systems.

  ^[1] Huth and Ryan [503] define a reactive system as one that is not meant to terminate. Examples include operating systems, embedded systems, and computer hardware.

• Predevelopment versus postdevelopment. A verification technique may be intended to be used as a design aid or for verification of the system after the design is complete.

Inductive verification techniques are typically more general in nature. Some of the techniques we discuss below were designed to be general-purpose software development methodologies, addressing all stages of the life cycle. Other inductive verification systems simply provide mechanisms for proof of theorems. All are based on generation of formulas that show that a specification of a system meets the requirements of a set of properties. These techniques often have separate steps to create formulas that claim that the specification meets the properties. These formulas are submitted to a theorem prover that uses a higher-order logic such as predicate calculus. The theorem prover attempts to show that the premises and conclusion are provably equivalent by finding a series of proof steps starting with the premises of the formula and eventually reaching the conclusion of the formula. The user of an inductive verification technique generally guides a theorem prover in finding a proof by supplying lemmata and previous results that can be used to prove more complex theorems. Some inductive verification techniques are used in the development cycle to find flaws during the design process. Others are used to verify the properties of computer programs.

Model checking techniques also establish how well a specification of a system meets a set of properties. The systems modeled are state transition systems, and a formula may be true in some states and false in others. Formulas may change truth values as the system evolves from one state to another. The properties to be verified by a model checker are formulas in a temporal logic. In temporal logic, truth or falsehood of a formula is dynamic and is not statically true or false as in propositional and predicate logic. Section 34.3, "Temporal Logic Systems," presents an example of a temporal logic system.

Typically, a model checker addresses a single model that is built into a tool or given to the tool as a specification of external properties. The tool is usually automatic, with little or no interaction with the users' point of view. Formula generation and proof are a single step from the user view. The model checker attempts to show that the model of the system and the desired properties are semantically equivalent, which can be described by saying that the model and properties exhibit the same truth table. The user initiates the model checker and waits for the results. The model checking approach is often used after development is complete but before a product is released to the general market. Model checking was designed for concurrent systems and systems that react to the environment and that are not expected to terminate.

EXAMPLE: The Hierarchical Development Methodology (HDM) of SRI, International, will be used in many examples in this chapter. HDM began as a general-purpose proof-based formal verification methodology addressing design through implementation. It was an automated and general-purpose (rather than property-oriented) methodology. It supported formal descriptions of a system at various levels of abstraction, using specification languages, implementation languages, and verification techniques to demonstrate that successive levels of abstraction were consistent. HDM also provided one of the earliest so-called model checkers with its Multilevel Security (MLS) tool, although the theorem prover uses a proof-based technique. The input to the MLS tool was a formal specification in the language SPECIAL, a nonprocedural design specification language that was very effective for writing external functional specifications. This tool is a fully automated, property-oriented verification system. The MLS tool embodies the SRI model, which is an interpretation of the Bell-LaPadula Model. MLS processed SPECIAL specifications to determine potential violations of the model within the specification. This was accomplished by the MLS verification condition generator, which created formulas that asserted that the specifications correctly implemented the embedded SRI model. The Boyer-Moore theorem prover processed these formulas. The output of the MLS program was a list of formulas that passed and those that failed.

The final section of this chapter addresses the analysis of cryptographic protocols, which lends itself nicely to the use of formal methods. The protocols themselves are relatively small and contained but may present complex and exploitable flaws. Protocol verification has been a hugely popular topic in the computer security research community over the past decade. Protocol verification has been accomplished using inductive proof methodologies as well as model checkers, and there are several special-purpose protocol verification methodologies in wide use. Many are based on the knowledge and belief logics of Burrows, Abadi, and Needham [163], and others describe the interactions of a set of state machines to attempt to prove that a protocol is secure.