SMTChecker toward completeness

The SMTChecker current model checking engine is safe but not complete. This means that assertions and other verification targets reported as safe should be safe — unless there’s a bug in the SMTChecker or backend solver — but false positives might be spurious due abstractions.

Two of the main sources of false positives in the counterexamples given by the current engine are

  • loops are handled in a bounded way (only one iteration is considered);
  • functions are analyzed separately in their own contexts.

Thus, contracts that either rely on loops for program logic or use state variables in different functions will likely lead to false positives when analyzed by the SMTChecker.

In order to increase the SMTChecker’s proving power and reduce false positives, we recently implemented a new model checking engine based on systems of Horn clauses capable of reasoning about loops and relations between state variables. We use SPACER as the backend Horn solver, which is integrated into Z3 and also used by Seahorn. Note that the life cycle of a smart contract can also be modeled as the following loop, where each loop iteration is a transaction:

constructor(...);
while(true)
random_public_function(...);

The goal of the new engine is to automatically infer both loop and state invariants while trying to prove safety properties, removing the need for extra assumptions, as written before. More technical details can be found in an upcoming paper which will be linked here when ready.

We can immediately see the results by analyzing the same contract from the previous post without the extra assumption as :

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

The SMTChecker now tries to prove the assertion considering the entire contract and an unbounded number of transactions, instead of one execution of only function . It automatically learns the contract invariant which holds at the beginning and end of every function and is decisive to prove the desired property. The check takes 0.16s on my laptop.

If we replace the division by , which clearly breaks the assertion, we get the following counterexample:

(and 
(function_average_68_0 2 1 0 0)
(interface_C_69_0 2 1)
(fallback_42_0 0 0 2)
(interface_C_69_0 0 0)
)

This is an internal representation of the multi-transaction bottom-up path that leads to the assertion failure where

  • is the contract’s idle state and the following numbers are the current values of state variables and , respectively.
  • is a call to the fallback function.
  • is a call to function .

Note that this format is internal only and transforming it into a more readable version is under development.

After contract construction both and are 0. The first transaction calls the fallback function with , which leads to and . The second transaction calls function where . The check takes 0.14s.

Besides contract invariants the engine also tries to summarize and loops inside functions. It can prove simple properties regarding loop behavior quite quickly, but the problem can also easily become too hard. Remember, this is an undecidable problem :)

function f(uint x) public pure {
uint y;
require(x > 0);
while (y < x)
++y;
assert(y == x);
}

The assertion above is proven in 0.05s.

function f() public pure {
uint x = 10;
uint y;
while (y < x)
{
++y;
x = 0;
while (x < 10)
++x;
assert(x == 10);
}
assert(y == x);
}

The assertions above involve a more complex structure with nested loops and are proven in 0.375s.

uint[] a;
function f(uint n) public {
uint i;
while (i < n)
{
a[i] = i;
++i;
}
require(n > 1);
assert(a[n-1] > a[n-2]);
}

Even though the code above also uses an array the assertion concerns only two elements of the array and the check takes just 0.16s.

function max(uint n, uint[] memory _a) public pure returns (uint) {
require(n > 0);
uint i;
uint m;
while (i < n) {
if (_a[i] > m)
m = _a[i];
++i;
}
i = 0;
while (i < n) {
assert(m >= _a[i]);
++i;
}
return m;
}

The function above computes and returns the max value of an array. The length of the array is given as a parameter since is not supported yet. This check is a lot more complex, since it checks that the computed max value is indeed greater or equal all the elements of an unbounded array.
EDIT: When writing this post, this sequence of assertions could not be proven after an 1 hour timeout. After tweaking some quantifier solver parameters the check is successful after 0.13s!
If we change the assertion to the given counterexample is the array .

Another example more similar to a state machine is the following Crowdsale skeleton:

pragma experimental SMTChecker;contract SimpleCrowdsale {
enum State { INIT, STARTED, FINISHED }
State state = State.INIT;
uint weiRaised;
uint cap;
function setCap(uint _cap) public {
require(state == State.INIT);
require(_cap > 0);
cap = _cap;
state = State.STARTED;
}
function () external payable {
require(state == State.STARTED);
require(msg.value > 0);
uint newWeiRaised = weiRaised + msg.value;
// Avoid overflow.
require(newWeiRaised > weiRaised);
// Would need to return the difference to the sender or revert.
if (newWeiRaised > cap)
newWeiRaised = cap;
weiRaised = newWeiRaised;
}
function finalize() public {
require(state == State.STARTED);
assert(weiRaised <= cap);
state = State.FINISHED;
}
}

Function can be called only once, when is . The fallback function accepts multiple deposits (without issuing tokens in this mock) while is . The Crowdsale may be finalized in function , where it makes sure that the was not breached.
The analysis automatically learns the invariant which proves the assertion. The check takes 0.09s.

If we change the correct assertion to we get the following 3-transactions counterexample:

(and
(function_finalize_107_0 1 1 1)
(interface_SimpleCrowdsale_108_0 1 1 1)
(fallback_85_0 1 0 1 0)
(interface_SimpleCrowdsale_108_0 1 0 1)
(function_setCap_42_0 0 0 0 1)
(interface_SimpleCrowdsale_108_0 0 0 0)
)

This bottom-up internal representation follows the same format as the one presented in the first example. All state variables start as 0. The first tx calls which leads to and . The second tx calls the fallback function with which modifies to 1. Finally, the third tx calls and the assertion fails. The check takes 0.08s.

There are still features missing for the engine to be considered ready, and we are constantly increasing the supported subset of Solidity, but these preliminary experiments show that the new engine might be able to automatically prove complex properties that involve multi-tx behavior reasonably quickly. For the next set of experiments I hope to verify some real world contracts that were already verified by other tools.

The code is still under development and the new SMTChecker engine should be released as part of one of the next 2 Solidity releases.

Building Solidity and Formal Verification tools.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store