Program Correctness through Self-Certification

A brief history of verification.  The deductive approach to program verification was originated by Goldstine-von Neumann⁴⁶ and Turing⁴⁴ in the late 1940s and early 1950s. These informal methods for verifying sequential programs were formalized by Floyd in 1962 (published in 1967,¹⁶ who attributes his ideas to unpublished work by Perlis and Gorn), and by Hoare in 1969.¹⁹ A deductive proof consists of invariance assertions, which define stable properties of program state, and ranking arguments, which establish convergence to desired subsets of program states. Pnueli and Manna showed how to extend invariance and ranking arguments to prove the correctness of reactive non-terminating programs, such as device controllers and network protocols.^25,26

A program may also be verified through a process of stepwise refinement. Here, an initial abstract program forms the specification. This program is systematically converted to a concrete program with a desired level of efficiency or detail. At each step of transformation, it is necessary to show that every behavior of the transformed program is a behavior of the original program, a relationship known as refinement. The refinement property is proved through an inductive correspondence relation between the state spaces of the two programs, known as a (bi)simulation.^20,30,31 Mechanized proof assistants (such as Coq, PVS, Isabelle/HOL, and ACL2) support the construction and checking of proofs. Yet, the major burden of formulating a proof remains on the human verifier. As a result, the construction of proofs of even moderately sized programs may require considerable time, effort, and mathematical expertise. As a concrete data point, a proof of a 1,000-line compiler optimization required a 10,000-line Coq proof script and more than a person-year of expert effort.⁴⁸ Such numbers are typical. This enormous effort is balanced by the considerable benefit of having established, once and for all, that a program behaves as expected in every case.

An important class of programs is that of finite-state circuits and network protocols. Such programs typically have several concurrently active components or threads, which considerably increases the difficulty of formulating a deductive proof argument. Model checking decides correctness entirely algorithmically, by systematically and exhaustively analyzing the finite state space.^9,39 Model checking works remarkably well in many cases. Its fundamental challenge is that of state explosion: A program with m concurrently executing components, with two states each, has a potential reachable state space of size 2^m. State explosion can be tamed to an extent by the use of compact data structures and abstraction methods but, in general, it limits the practical applicability of model checking.

Logic.  We give two examples of certificates from logic. The first is for the prototypical NP-complete problem: Boolean Satisfiability (SAT). A Boolean formula is in SAT if it is satisfiable, that is, if there is an assignment of Boolean values to the variables of the formula under which the formula evaluates to true.

For a “Yes” answer to SAT, a satisfying assignment forms a valid certificate. The format of a certificate is that of an assignment of values to variables. A certificate in this format is valid if the formula evaluates to true under the assignment provided by the certificate. The past three decades have seen remarkable advances in SAT-solving in practice. SAT solvers are implemented with highly optimized C or C++ code, which raises concerns about the presence of subtle bugs. Although the research community has developed some formally verified solvers, commonly used solvers are not formally verified. Nonetheless, all produce a satisfying assignment to certify a Yes answer.

What about formulas that are not satisfiable? A formula φ is unsatisfiable if, and only if, its negation ¬$\phi$ is valid (that is, if ¬$\phi$ is true for all assignments.) The validity of ¬$\phi$can be established through a deductive proof, which acts as a certificate for the unsatisfiability of $\phi$. While the proof length cannot be guaranteed to be polynomial in the length of $\phi$ (which would imply NP=coNP), it is easy to check a claimed proof by inspecting each inference step. There are several proof systems to choose from; many SAT solvers produce unsatisfiability proofs in the DRAT format.¹⁸

The second example is the extension of propositional logic with Boolean quantification. A Quantified Boolean formula (QBF), as the name suggests, allows nested application of the existential (∃) and universal (∀) quantification operators to propositional formulas. QBF satisfiability is the prototypical PSPACE-complete problem.

Consider a quantified formula of the shape (∀x(∃y $\phi$ (x, y))), where the inner “kernel” $\phi$ is quantifier-free. This formula is either true or false, as it has no free variables. If it is true, then for every Boolean value a for x, there is a Boolean value b for y such that $\phi$ (a, b) is true. Unlike SAT, a single assignment cannot serve as a certificate. Instead, one needs an “assignment generator” to produce an appropriate value of y for each value of x. This is known as a Skolem function, after the logician Thoralf Skolem. Given a Skolem function F, the QBF formula can be rewritten to (∀x $\phi$ (x, F (x))). A Skolem function can be viewed as a Boolean circuit with input x and output y. A certificate of correctness is thus the Skolem function F as a Boolean circuit, along with a deductive proof for the validity of the quantifier-free Boolean formula $\phi$ (x, F (x)), which is generated as for the SAT problem.

Formulas with a deeper alternation of quantifiers require a Skolem function for each existentially quantified variable. For instance, the certificate for (∀x₁(∃y₁(∀x₂(∃y₂ $\phi$ (x₁,x₂,y₁,y₂))))) consists of a Skolem function F₁ mapping x₁ to y₁, a Skolem function F₂ mapping x₁ and x₂ to y₂, and a validity proof for $\phi$ (x₁,x₂,F₁ (x₁), F₂ (x₁,x₂)).

This discussion is based on the traditional notion of a proof as a static object. Complexity theorists have fruitfully extended the notion of a proof to that of an interactive randomized protocol (IP), where a Prover and Verifier engage, informally speaking, in a question-and-answer session before the Verifier reaches a decision on the validity of a claim made by the Prover. Shamir⁴² shows that IP=PSPACE; that is, that all PSPACE-questions have short interactive proofs.

A fascinating offshoot is the notion of a zero-knowledge (ZK) proof. Here, the interaction is such that a verifier is convinced (with high probability) of the truth of the Prover’s claim without learning anything about why it is true. Non-interactive variants of ZK-IP proofs, known by various acronyms (SNARKs, STARKs, …), are used for applications where, for instance, one party wants to offer an algorithm as a service while keeping secret certain aspects (for example, Ben-Sasson et al.²). Succinct ZK proofs act as certificates that, in addition, hide information.

Model checking.  Model checking in its pure form^9,39 is a fully automatic process for verifying sophisticated temporal properties of finite-state machines. Model-checking methods systematically explore the state space of the machine, using either graph algorithms or fixed-point calculations.

It is perhaps easiest to appreciate the automata-theoretic approach to model checking.⁴⁵ Here, the machine is viewed as a generator of words, and the negated property as an acceptor of words, both being represented as automata over (infinite) words. The machine satisfies the property if the intersection of these two automata languages is empty; thus, model checking reduces to a language emptiness test over finite automata.

If the property is violated, there must be a word that is accepted by the intersection automaton; this word is a certificate that explains the violation. This certificate is commonly known as a counterexample. Historically, the ability to generate counterexamples was a major factor in the widespread adoption of model checking.

What if the property holds (that is, the intersection automaton has an empty language)? The authors (with collaborators) show in Namjoshi³² and Peled et al.³⁷ that, in this case, one can instrument the model-checking algorithm to extract a deductive proof that justifies correctness.

The extracted deductive proof is expressed in terms of the central concepts of invariance and ranking introduced earlier in this article. Deductive proof certificates can be generated for both linear and branching-time temporal specifications, and from a variety of model-checking algorithms. Several software model-checking tools produce deductive proofs of correctness (and violation) in a well-defined and machine-checkable format of a “verification witness.”³

Interestingly, for branching-time logics, it is possible to produce a deductive proof of failure. Model checking can also be framed as an infinite game in an arena defined by the product of the program and a (branching) property automaton.¹² The opponent makes the universal choices in this game, while the player makes the existential choices. The property holds if and only if the player has a winning strategy. The deductive proof represents a winning strategy for the player, expressed compactly in the form of invariants and ranking functions. As branching-time logics are closed under negation, a program that fails to satisfy a property φ must necessarily satisfy the negated property ¬$\phi$. A failure proof thus represents a winning strategy for the opponent in the model-checking game and can also be expressed in terms of invariants and ranking functions.³²

Conceptually, the notion of a proof-generating model checker neatly links the algorithmic and deductive approaches to program verification. In practice, it guards against the danger that a production model checker, which typically runs into the hundreds of thousands of lines of code, may have a serious bug that causes it to incorrectly miss reporting a property violation.

Graph algorithms.  We present two examples of certificates for graph algorithms. For the NP-complete Hamiltonian Path problem, the certificate is a path. A claimed certificate is valid if the path has the Hamiltonian property. Indeed (by definition) for any language in NP, every word in the language has a polynomial-sized certificate that can be validated in polynomial time. A different and useful way of seeing this is via Fagin’s elegant characterization of NP as those properties expressible in existential second-order logic,¹⁴ that is, as (∃R : $\phi$ (R)) where R is a set of relation variables and $\phi$ is a first-order formula.

This formulation compactly represents many graph problems, including Hamiltonian Path. The certificate is then an instantiation of the variables in R, while validation is the process of checking that $\phi$ is true for a claimed certificate R.

Our second example is that of graph planarity, a problem that is solvable in polynomial time. For a positive answer, the certificate is an embedding of the graph in the plane. For a negative answer, the certificate is an embedding in the input graph of the “forbidden” graphs K₅ (complete graph on five vertices) or K_3,3 (complete bipartite graph with three vertices on each side). Such an embedding certifies non-planarity by Kuratowski’s theorem.⁷ Checking a given embedding is simpler than verifying an implementation of a planarity algorithm, such as the Hopcroft-Tarjan method.

Here, we would like to emphasize once again that the focus of self-certification is on the correctness of implementations. The underlying algorithms are usually stated in mathematical notation and have correctness proofs. The difficulty arises with validating their implementations. A programmer must turn the algorithm into an implementation, making choices about representations of data structures, expanding computation steps, and possibly introducing optimizations to detect and solve special cases. Hence, the implementation differs from the algorithm and is harder to verify. Certification for graph algorithms was pioneered by Mehlhorn and collaborators and implemented in the LEDA package. The work in McConnell et al.²⁸ describes the genesis of this work: It came about from the recognition that bugs in LEDA could go unnoticed unless there was a way to check each answer. LEDA contains checkers for several graph algorithms and for geometric algorithms such as computing triangulations.

An interesting question arising from the Hamiltonian Path example is the following: What is the certificate if the graph does not have a Hamiltonian Path? One option is to list all simple paths and check that they are not Hamiltonian, but this is neither concise nor elegant, and it raises other concerns: for example, how does one prove that all paths have been enumerated?

A possible answer is through a verified reduction to SAT. It is, in principle, possible to convert a negative answer to the Hamiltonian Path problem on a graph G to a certificate of the unsatisfiability of a Boolean formula r(G) obtained via a provably correct reduction r. We discuss reductions later in this article.

Distributed computing.  The notion of certification is well-studied in the distributed computing literature, appearing under several formulations. We illustrate the central ideas through two examples.

Consider the problem of computing a maximal independent set (MIS) of nodes in a connected graph. An MIS is a subset S of the nodes such that every node v ∈ S has no neighbors in S, and every node v ∉ S has a neighbor in S. A distributed protocol computes an MIS by letting a node output “Yes” if it is in the set, and “No” otherwise. (An example is Luby’s well-known probabilistic protocol for MIS,²³ where termination of each node is guaranteed with probability 1.) Once all nodes terminate, one can check locally whether the computed set is indeed an MIS. Consider a node v. If its output is “No” then one needs to check that v has some neighbor whose output is “Yes.” If the output of v is “Yes” then one needs to check that the output of every neighbor of v is “No.”

This example demonstrates that although MIS is a global property, it has a correctness certificate that can be locally checked, that is, where each node checks a property of its own output (and certificate) and that of its immediate neighbors.

Consider now the problem of computing a spanning tree in a connected graph. (See, for example, Lynch’s spanning tree protocols²⁴). In most protocols, a terminating node knows its parent and can determine its children. The root, of course, has no parent. Protocols may be initiated at the leaves and work toward the root, or start from the root and go down the tree. For this exposition, assume that the protocol starts at a unique designated root. Assume further that each terminating (non-root) node outputs its parent. Then, checking that the protocol indeed computes a spanning tree requires checking that each non-root node has a parent connected to it and that the root, together with all nodes reachable from it, comprises all the nodes of the graph. Being a spanning tree is also a global property but, unlike in the MIS example, the assignment of parents does not suffice for a local test of correctness, as it is also necessary to compute reachability in the graph.

There is, however, a way to augment the parent information to form a locally checkable certificate. Let each node, in addition to its parent, output its level in the tree, with the root being level 0. This suffices for a local check: Each node at level k > 0 should have a parent to which it has an edge and is at level k − 1, and the (a priori designated) root is the single level-0 node, which, unless the graph is a singleton, has children.

Various aspects of locality have been studied in distributed computing. The research of local certificates focuses on runtime, efficiency, and communication costs of certification.

The work in Naor and Stockmeyer³⁴ formally defines locality in the context of identifying the class of computations that can be performed “locally” (that is, within a given fixed distance of each node) in constant time. It studies the class and describes some rather nontrivial members of it. A nice survey of local certification and self-stabilization is in Feuilloley,¹⁵ which studies the certificate size of a protocol as the size of the smallest certificate that permits local checking of the protocol. The work in Korman et al.²¹ establishes that every predicate on network configuration can be certified by a certificate of size Θ(n²) (where n is the number of nodes). This certificate consists of the adjacency matrix of the graph distributed to each node. Each node verifies that its own result is consistent with this certificate and that all neighboring nodes have the same certificate. There are cases where much shorter certificates exist.

We conclude this section of distributed systems by pointing out a particular class of systems whose computation is inherently self-certifying, namely, those whose goal is to establish consensus and carry the proofs of others’ computations. This is often carried out by digital signatures when the parties are not to be trusted. In the Byzantine Generals algorithms for consensus, the goal is to establish that every honest player will eventually know that every honest player . . . will eventually know that the decision is some value d. Thus, every (honest) player that reaches a decision has concrete information (that is, certificates) about the state of other players that allows it to reach the decision. These certificates are often digitally signed to prevent dishonest players from tampering with or forging them. While the protocol may not explicitly publish these certificates, they usually can be produced by adding a “publish all certificates” action to each participant.

Program transformations.  A compiler converts a program written in a source programming language to an executable form. In its typical form, the front end of a compiler transforms a source program into a simpler intermediate representation (IR), then a sequence of IR-to-IR transformations are applied to “optimize” execution, followed by a back-end process that transforms the IR into an executable form. Production-quality compilers are very large programs. For example, the popular GCC compilation framework has more than 10 million lines of code. Despite considerable care in programming, errors inevitably creep in.

Compilation errors are difficult to detect, as the transformations convert a human-understandable source program to a barely recognizable target executable; moreover, an error may result in a difference in behavior between source and target programs only on a vanishingly small proportion of inputs. Several ingenious compiler testing methods have been developed but, by the nature of testing, those may miss errors.

Compiler correctness has been, for these reasons, a major verification challenge since the 1960s. The classical approach is to develop a machine-checked deductive proof of correctness for each program transformation; notable examples include Leroy²² and McCarthy and Painter.²⁷ Proofs of this sort require considerable time, effort, and expertise. For instance, a well-documented effort at proving a 1,000-line transformation (to static single assignment, or SSA, form) for the LLVM compilation system required roughly 10,000 lines of proof script for the Coq proof assistant and more than a person-year of expert effort.⁴⁸

The correctness criterion for all transformations is the same: a transformation should preserve input-output behavior. That is, given the same sequence of inputs, the original and optimized program should produce the same sequence of outputs. (This criterion is complicated slightly by the presence of potentially undefined behavior in the source program, such as a division by zero or a buffer overrun. In those cases, the target program may replace the undefined behavior with a specific action, such as halting, if allowed by the language semantics.) In its essence, compiler correctness is a program equivalence question, which is undecidable in general.

In the 1970s, Samet⁴¹ developed methods to check for equivalence of programs related by compiler transformations. This approach was independently rediscovered in the 1990s^8,38 and named translation validation. On each run of compilation, the source and target programs are checked for semantic equivalence, using heuristics that rely on static analysis and hints from the compiler, such as the sequence of transformations applied to the program. In effect, the validation program attempts to discover a stepwise correspondence—a (bi)simulation relation—between the behaviors of the source and target programs. This technique was applied in Necula³⁶ and Zuck et al.⁴⁹ to certify several optimizing compiler transformations.

In the late 1990s, Rinard proposed⁴⁰ that each compiler transformation could simply generate a suitable correspondence relation. This relation acts as a certificate of program equivalence, which is valid if it is a (bi)simulation. A single (bi)simulation-checking validator thus suffices to check the correctness of a variety of program transformations. In one such instance,³³ certifying the SSA transformation required only 200 lines of additional certificate-generation code (over a 1,000-line SSA transformation), and the implementation was completed in three person-weeks, illustrating the considerable savings in effort that can be achieved through certification.

Program transformations can take unusual forms. The work in Pnueli et al.³⁸ certifies a transformation from a synchronous dataflow language (Signal) to asynchronous sequential code in C. Self-certification is applied in Arons et al.¹ to show backward compatibility for microcode, establishing that a new, manually generated microcode has equivalent behavior to the original microcode on the original hardware.

Properties of certification schemes.  The essential property required of a certification scheme is the soundness of the validator: namely, if the validity test succeeds, the specification must be met. Formally, it must hold that for every x, y, w ∈ X × Y × W, if $V$ (x, y, w) is true then (x, y) ∈ ψ. In its equivalent contrapositive form, soundness ensures that incorrect results are never accepted, that is, if the output y is such that (x, y) ∉ ψ, there is no witness w for which $V$ (x, y, w) is true.

There are several other desirable, but not essential, properties for a certification scheme. Some can be formulated precisely; others, while important, appear to be difficult to formulate in precise mathematical terms.

Reductions.  A certification scheme depends only on the problem specification. This property makes it possible for different solutions to a problem to share a common certificate format and certificate validator. For example, the certificate of bubblesort applies to any sorting algorithm. Another useful consequence is it allows a reduction from one problem specification to another, so one can set up a certification scheme for the first problem in terms of an existing certification scheme for the second.

We saw one such reduction earlier, where a certification scheme for the Hamiltonian Path problem is defined in terms of a certification scheme for Boolean formula validity (that is, unSAT). By the formulation of NP, this is possible in principle for any problem in NP. The advantage is that one needs only to construct provably correct certificate checkers for SAT and unSAT to obtain certification for a large class of important questions. The correctness of each reduction must be proved separately. As reductions operate at the level of specifications, we may expect such proofs to be simpler in nature and easier to mechanize than proofs of the correctness of implementations.

Consider problems A and B with their respective input and output domains and specifications. A reduction r from A to B is a function that maps X_A × Y_A to X_B × Y_B with the following property: For any x in X_A and y in Y_A, if the specification ψ_B holds for r (x, y), then specification ψ_A holds for (x, y).

A primary use for a reduction is to derive a certification scheme for A from a scheme for B. Let (W_B, V_B) be a certification scheme for B. Let W_A = W_B and V_A (x, y, w) = V_B (r (x, y), w). This induced scheme is sound for A. (Proof: Consider x, y, w such that V_A (x, y, w) holds. By definition, V_B (r (x, y), w) holds. By soundness of the scheme for B, it follows that r (x, y) satisfies ψ_B. By the correctness of the reduction, (x, y) satisfies ψ_A.)

This discussion on completeness and reduction gives rise to two questions on the universal applicability of self-certification. First, is there a systematic way to formulate a certification scheme for any specification? Second, is there a universal problem such that certification schemes for any other problem can be derived from it through a reduction?