TABLE OF CONTENTS The definition and the promise of formal methods is that they provide a means to "allow the specification, development, and verification of a computer system using a rigorous mathematical notation. Using a formal specification language to specify a system allows its consistency, completeness, and correctness to be assessed in a systematic fashion" [4]. The standard approach towards trying to achieve this goal for security-relevant systems is through the use of formal program verification techniques that make use of mathematical logic to try to prove the correctness of a piece of software or hardware. There are two main classes of tools used in this task, proof checkers (sometimes called theorem provers), which apply laws from logic and set theory to a set of assumptions until a desired goal is reached, and model checkers, which enumerate all of the possible states that a system can be in and check each state against rules and conditions specified by the user [5] [6] [7]. In terms of reporting problems, proof checkers (which work with symbolic logic) will report which step in a particular proof is invalid, whereas model checkers (which work with finite state machines, FSMs) will report the steps that lead to an invalid state.
Proof checkers are named thus because they don't generate the entire proof themselves but only aid the user in constructing a proof from an algebraic specification, performing many of the tedious portions of the proving process automatically. This means that users must...
