Formal Verification in Solidity

Last week I gave a talk “Using Solidity’s SMTChecker” at Devcon4, as part of the Security track. You can read the slides on GitHub. This post introduces Solidity’s SMTChecker and explains on a (very) high level how it works. Deeper technical details on how the SMTChecker works can be found in [1]. A little bit of background on logic might be useful for the SAT/SMT introduction, although not completely required. If you are interested in more information about SAT/SMT solving, please see [2,3].

The Solidity compiler has a built-in formal verification module called SMTChecker. We’re developing the SMTChecker to be an SMT-based Bounded Model Checker that verifies assertions at compile-time. Moreover, it can detect underflow/overflow, trivial conditions and unreachable code. No extra knowledge/tool is required to use the SMTChecker, as the formal specification is part of the Solidity code. If buggy code is found, the compiler presents program variable values that lead to the bug.

SAT/SMT Solvers

The Boolean Satisfiability (SAT) problem consists of finding values — True or False — for the variables of a formula such that it evaluates to True. If those values exist they are called a model and the formula is Satisfiable; otherwise the formula is Unsatisfiable. For example, the formula a∧¬b is satisfiable since the values a = True, b = False make the formula True, and a∧¬a is unsatisfiable.

SMT stands for Satisfiability Modulo Theories, and the SMT problem is to decide whether a first-order logic formula written as a combination of different theories is satisfiable. Take the following formula, for example, using the theory of integers:

      ∀x (f(x) = x * 42) ∧ (a ≥ b) ∧ (b ≥ c) ∧ (f(a) ≥ f(c))

The first part of the formula ∀x (f(x) = x * 42) simply defines a monotonic function f. The second part (a ≥ b) ∧ (b ≥ c) adds some linear constraints. The third and last part f(a) ≥ f(c) applies function f over the constrained variables. The formula is quite simple, so we can quickly see that it is satisfiable. For example, values a = 0, b = 0, c = 0 satisfy the formula.

Notice that there are multiple values we can give to the variables such that the formula evaluates to True:

• a = 0, b = 0, c = 0
• a = 1, b = 1, c = 1
• a = 2, b = 1, c = 0
• a = 300, b = 200, c = 100
• …

In fact, this formula has infinitely many models.

Now, if we change the last part of the formula to f(a) < f(c) (the opposite), the formula becomes unsatisfiable. This means that there are no possible values for a, b, c that satisfy the constraints. This is a very powerful statement and very useful for program verification.

Solidity Verification

The SMTChecker is an experimental feature and is not enabled by default. To enable it on your Solidity code add the line pragma experimental SMTChecker; . The module uses Solidity syntax to identify the formal specification of the program. Conditions inside require are treated as assumptions and statements inside assert are verification targets which the SMTChecker tries to prove statically.

The SMT problem presented above represents how the following Solidity program is verified (with some syntax sugar) while being compiled:

pragma experimental SMTChecker;
contract C
{
    uint c;
    function f(uint x) public pure returns (uint) {
        return x * 42;
    }
    function g(uint a, uint b) public {
        require(a >= b);
        require(b >= c);
        assert(f(a) >= f(c));
    }
}

The Solidity program is encoded into SMT statements using the relevant theories, where verification targets are encoded negated. Therefore the query that verifies the assert above would be encoded as the SMT problem:

      ∀x (f(x) = x * 42) ∧ (a ≥ b) ∧ (b ≥ c) ∧ (f(a) < f(c))

The trick here for SMT-based Solidity verification lies exactly on negating verification targets:

• If the SMT solver answers that the formula is Satisfiable, it means that there are values for the program variables that satisfy the negation of the assertion, that is, the assertion can be violated and there is a bug. In that case the values are a counterexample that can be reported back to the developer.
• If the formula is Unsatisfiable, there is no program behavior that can break the assertion, therefore the assertion is correct.

In the given Solidity example, the assertion is true. As another example, let’s change the verification target to assert(f(a) == f(c)) . In that case, the compiler returns

Warning: Assertion violation happens here
  assert(f(a) == f(c));
  ^------------------^
  for:
  a = 1
  b = 1
  c = 0

which is a counterexample for the violated assertion.

False Positives

The formal approach we use in the SMTChecker is sound but not complete: if the compiler claims that the program is safe with respect to an assertion, that is the case. However, if the compiler claims that a piece of code is buggy, the counterexample might be spurious since complex types, complex functions and external functions have to be over-approximated (abstracted) due to lack of expressiveness. Another reason for spurious counterexamples is the difficulty of automatically inferring invariants over contract state variables.

Thus, in many occasions it makes sense to help the SMTChecker to prove properties by adding extra constraints (requires), even if they seem redundant.

pragma experimental SMTChecker;
contract C
{
    uint sum;
    uint count;
    function () external payable {
        require(msg.value > 0);
        require(sum + msg.value <= 1000000);
        sum = sum + msg.value;
        count = count + 1;
    }
    function average() public view returns (uint avg) {
        require(count > 0);
        avg = sum / count;
        assert(avg > 0);
        return avg;
    }
}

The example contract above is able to receive Ether up to 1000000 wei, value that is stored in state variable sum. A valid transaction must have a value greater than zero, and for every valid transaction state variable count is incremented by one.
The contract also has a function average that computes the average value sent per transaction, where at least one transaction must have been executed.

The SMTChecker tries to prove assert(avg > 0) and returns:

example.sol:19:3: Warning: Assertion violation happens here
  assert(avg > 0);
  ^-------------^
  for:
  avg = 0
  count = 1
  sum = 0

The counterexample indeed breaks the assertion, since avg = sum / count = 0 / 1 = 0. However, it is impossible that sum = 0 and count = 1 at the same time:

• msg.value is an unsigned integer and the fallback function guarantees that it is least 1;
• sum is incremented by msg.value in the fallback function, where count is incremented by 1;
• from the points above we know that the invariant sum >= count holds in the beginning/end of every function.

Therefore the counterexample is spurious.
In such cases, we can help the SMTChecker by explicitly adding the invariants that we know about the contracts we write, since at the moment the SMTChecker cannot infer those automatically. We plan to add this feature in the future.

pragma experimental SMTChecker;
contract C
{
    uint sum;
    uint count;
    function () external payable {
        require(msg.value > 0);
        require(sum + msg.value <= 1000000);
        sum = sum + msg.value;
        count = count + 1;
    }
    function average() public view returns (uint avg) {
        require(count > 0);
        require(sum >= count);
        avg = sum / count;
        assert(avg > 0);
        return avg;
    }
}

After explicitly adding the invariant to the function, the SMTChecker is able to prove that the program is safe.

Future Plans & Conclusion

At the moment our work on the SMTChecker focuses on improving support to the language. There is still work to be done on supporting modifiers and address member functions, for example.

In the future we want the SMTChecker to try to infer state invariants automatically, as well as use modifiers for function abstraction.
We also intend to add syntax that allows the Solidity programmer to add invariants contract-wide, such that they are added in the beginning and end of every function and shown to be inductive.

If you have questions/ideas please reach out! You can comment here or talk to us on our Gitter channel.

References

[1] Alt, L., Reitwießner, C.: SMT-Based Verification of Solidity Smart Contracts. In: ISoLA 2018. LNCS, vol. 11247, pp. 376–388 (2018).

[2] Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability. Volume 185 Frontiers in Artificial Intelligence and Applications (2009).

[3] De Moura, L., Bjørner, N.: Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, n. 9, pp. 69–77 (2011).