4

The question holds. What's the difference between the two? What would be an example of using these two tools on a minimal piece of solidity code?

1
  • 1
    Might be off but I think that SMT solvers are simply a kind of tool used for producing formal verification reports. "Formal verification" is a pretty fuzzy category. Feb 21 at 21:51

1 Answer 1

5

The two terms represent quite different things:

Formal Verification (FV) is a generic term for applying formal methods (FM) to verify the correctness of hardware, software, abstract models, etc. Applying FM means anything based on mathematical proofs, in software often used as a proof of correctness or proof of "bug". The Wikipedia page on FV is actually quite good.

SMT stands for Satisfiability Modulo Theories and extends SAT solvers (which solve the Boolean Satisfiability problem). SMT solvers are concrete tools, automated theorem provers that take in a Boolean formula written in SMT theories (such as Integers, Reals, Arrays, Tuples, etc) and apply specialized decision procedures to answer the question "is this formula ever true?". The solver may answer satisfiable, if there is a valuation of the variables that leads to the entire formula being true, unsatisfiable if it is impossible for the formula to ever be true, or unknown, if the solver was unable to find a decisive answer. The unknown case may happen if you give the solver a timeout, for example, or if you used theories that are complicated to solve, such as Nonlinear Integer Arithmetic (which is undecidable so you can only hope for the best). You can play with the z3 SMT solver in their brand new docs/tutorial page.

Within the FV field, there are several techniques that are used to verify systems (hw, sw, etc). Some of them are graph based, where you define your program and the properties you want to check in terms of a transition system, and you make graph queries of the form "can this bad state ever be reached?", like in Model Checking.

Nowadays, one of the main techniques is a specialization of the above called Symbolic Model Checking, where instead of using an explicit graph you represent the system and properties you want to verify as theorems. That's where SAT and SMT solvers come in. Instead of asking a graph "can my explicit bad state S be reached from my initial state I?", you would represent the same reachability problem as a Boolean formula (potentially using SMT theories), such that an SMT solver will answer unsatisfiable if S cannot be reached from I, and satisfiable otherwise. In summary the former means your property is proven to be correct for every input case ever backed by a mathematical proof, and the latter means there's at least one buggy path in your program leading I to S, where the valuation of the variables is the counterexample to your property.

As a more concrete toy example, take the following Solidity function:

function property(uint16 x, uint16 y) external pure {
    require(x < 100);
    require(y < 100);
    assert(x + y < 1000);
}

Usually FV tools treat constructs like requires as assumptions/pre-conditions. We're not trying to prove the requires, we're assuming they're always true when continuing the execution path. Our target is the assert condition. We want to prove that, given a uint16 x and uint16 y, such that both are < 100, their sum is < 1000. This is of course quite trivial to solve just by looking at it, but it serves as an example of how an SMT solver can be used here. From that code, we'll write the following theorem (basically consisting of a set of constraints):

x >= 0 && x < 2**16      && // type constraints on x
y >= 0 && y < 2**16      && // type constraints on y
x < 100                  && // require(x < 100)
y < 100                  && // require(y < 100)
x + y >= 1000               // negation of our assertion

The reason we negate the assertion we want to prove is that we're looking for a proof by contradiction: if the solver says unsatisfiable to the above, it means it's impossible for the assertion to be false (therefore broken), therefore the assertion must always be true!

Here's the full smtlib2 file to prove the above, you can run it with $ z3 theorem.smt2:

(declare-const x Int)
(declare-const y Int)

(assert (and
    (>= x 0)
    (< x 65536)
    (>= y 0)
    (< y 65536)
    (< x 100)
    (< y 100)
    (not (< (+ x y) 1000))
))

(check-sat)

The solver says unsat. We've now proven our assertion is correct, thus always true regardless of the input values. For the sake of comparison, we can change our property to something less true: assert(x + y < 150). The full theorem in smtlib2:

(declare-const x Int)
(declare-const y Int)

(assert (and
    (>= x 0)
    (< x 65536)
    (>= y 0)
    (< y 65536)
    (< x 100)
    (< y 100)
    (not (< (+ x y) 150))
))

(check-sat)
(get-model)

The solver now says

sat
(
  (define-fun x () Int
    51)
  (define-fun y () Int
    99)
)

The sat answer means our assertion is not always true, and the model that follows gives us exactly how to break the assertion: pass 51 and 99 for x and y in our function. This is a counterexample to our broken property.

The approach above is also called Symbolic Execution and is an example of what many tools do under the hood, for example Solidity's SMTChecker, hevm, Halmos, Manticore.

There are also other more complex techniques that are applied on top of SMT solving a theorem and will give you different pros/cons in tooling, for example Horn solving (used by SMTChecker's CHC engine, solc-verify) and Abstract Interpretation (used by Certora afaik). I try to keep a list of FV tools for Ethereum.

8
  • If I may summarize, you're saying: "Formal verification (FM) is applying formal methods to verify correctness. An SMT Solver is a type of FM." Now, symbolic execution afaik is figuring out what inputs will lead to what paths in a system. An SMT Solver as described above doesn't feel like it fits that description. How is an SMT solver an example of symbolic execution? Feb 22 at 13:10
  • 1
    (1). "An SMT Solver is a type of FM" and (2). "SMT solver an example of symbolic execution" are incorrect. An SMT solver is "just" a tool that receives a theorem and answers "yes" or "no", such as z3, cvc5, OpenSMT2, Eldarica. SMT solvers are used by FV tools/techniques, but they are lower in the stack and don't care what the technique above it is. Symbolic execution is one of the techniques of how to use an SMT solver to analyze programs. Maybe there's some confusion with the "SMTChecker" FV tool, which is not an SMT solver (it's an assertion checker that uses SMT solvers). Feb 22 at 14:49
  • What would be a full example of suite of tools for formal verification? You're saying the "SMTChecker" is an example of FV? What would be the relationship between an SMT Solver or SMTChecker and FV? Feb 22 at 15:17
  • 1
    Yea that sounds good! To be more precise, the entire strategy you described is contained within symbolic execution. Also this technique is widely used, not only in web3. You'll see the same being done for C and other languages. Feb 25 at 12:47
  • 1
    Yes! It's just one of many existing FV techniques (one of the most common ones). Feb 27 at 19:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.