SMTChecker: (almost) practical superpower

Theory: what is SMTChecker?

Would you bet your firstborn that the contract you just deployed doesn’t have critical vulnerabilities? If you’re like me, the answer is a resounding ‘no’.

I’ve seen enough hacks in traditional software engineering to know that you can never be 100% sure. That is scary, but a combination of different techniques can get us pretty close to the desired level of confidence. SMTChecker is one of them.

It’s a tool that performs formal verification of your contract: you define a specification (what you think your contract should do), and SMTChecker formally proves that the contract conforms to the spec. If it doesn’t, SMTChecker often gives you a concrete counterexample: a sequence of transactions that break the specification.

And the best part? If you use Solidity, you already have SMTChecker — it’s part of the Solidity compiler.

It is not a bulletproof solution by any means — there are bugs, verification is slow. Most of all, it’s damn hard to define a complete specification. But even knowing that, it’s still worth a try.

The contract implements a counter —a piece from the game of checkers (or draughts) played on an 8x8 board.

We‘ll implement a (made up) ‘lazy counter’: it can’t move, but can capture pieces on diagonally adjacent cells by ‘jumping over’ them: if I’m at (0, 0) and want to capture a piece at (1, 1), I’ll end up in (2, 2). Easy.

The code is straightforward: we create a counter at a given position. It then can capture other pieces.

The interesting bit is the last function — it defines an invariant that must hold at all times. The invariant is simple — the counter can’t leave the board. Let’s compile the contract and see if our invariant is ever broken (note the extra solc arguments — they turn on the SMTChecker in aggressive but accurate mode):

~/src/smtchecker_demo ❯❯❯ solc 1.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0
Warning: CHC: Assertion violation happens here.
Counterexample:
x = 0, y = 8
Transaction trace:
LazyCounter.constructor(2, 6)
State: x = 2, y = 6
LazyCounter.capture(1, 7)
State: x = 0, y = 8
LazyCounter.invariant()
--> 1.sol:32:9:
|
32 | assert(x >= 0 && x < 8 && y >= 0 && y < 8);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Oops, our invariant is broken. SMTChecker even gives us a counterexample! If our piece is at (2, 6) and it captures the piece at (1, 7), it ends up at (0, 8) which is outside the board. We forgot to check the counter position validity after the capture.

It is important to understand what SMTChecker just did: we gave it a contract with a set of operational boundaries(require statements that define the set of valid inputs) and an invariant. SMTChecker did an exhaustive analysis: called all public functions in a loop with every possible input, in all possible combinations. In reality, it doesn’t do a brute force approach (that’d be too expensive) but relies on math to make it work (I won’t pretend to fully understand this, there are some details here).

Here’s another example that shows that SMTChecker tries long sequences of transactions to test invariants: a contract that implements a chess knight. We’ll add an invariant that we know is not valid, just to give SMTChecker something to find: the knight can’t reach the (7, 7) position. SMTChecker will also give us a counterexample.

~/src/smtchecker_demo ❯❯❯ solc 2.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0
Warning: CHC: Assertion violation happens here.
Counterexample:
x = 7, y = 7
Transaction trace:
Knight.constructor()
State: x = 0, y = 0
Knight.move2()
Knight.isValidPosition() -- internal call
State: x = 2, y = 1
Knight.move2()
Knight.isValidPosition() -- internal call
State: x = 4, y = 2
Knight.move5()
Knight.isValidPosition() -- internal call
State: x = 3, y = 4
Knight.move1()
Knight.isValidPosition() -- internal call
State: x = 4, y = 6
Knight.move3()
Knight.isValidPosition() -- internal call
State: x = 6, y = 5
Knight.move1()
Knight.isValidPosition() -- internal call
State: x = 7, y = 7
Knight.get_to_7_7()
--> 2.sol:61:9:
|
61 | assert(!(x == 7 && y == 7));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Neat! It gave us the sequence of steps that moves the knight from (0, 0) to (7, 7).

Practice

Disclaimer: Everything else is a big experiment to see how to make it useful in ‘production settings’. There may be other ways, I don’t claim to have found THE WAY.

Let’s do something a bit more practical: part of an AMM: liquidity providers add liquidity to a trading pair, but nobody can actually trade.

  • Upon construction, the owner deposits a few (x) X tokens and a few (y) Y tokens. AMM generates x * y LP tokens
  • Anybody can deposit x1 X and y1 Y tokens, as long as this doesn’t change the ratio of X/Y balances (x1/y1 == xReserves / yReserves). AMM generates totalSupply(LP) * (x1 / xReserves) LP tokens
  • We only support fixed-point ERC20 tokens with decimals() == 18

That’s it. We’re not even distributing LP tokens, just generating them.

What invariants can we add? Not much — maybe that reserves are not empty (xReserves != 0 && yReserves != 0), but that’s it.

Let’s turn the definition of an invariant on its side and call it a ‘dynamic invariant’: knowing the state before and after executing addLiquidity, what can we assert?

Notice the revert() at the end — it makes sure that the invariant function does not have side effects (think of it as a view function). Let’s try it out!

~/src/smtchecker_demo ❯❯❯ solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol
...

This is going to take a while (a few hours at best). Not practical enough for 1 simple invariant.

What could make it slow? My guess is addresses and external calls (transferFrom) — SMTChecker models them as unknown functions that can do anything, including calling your contract back. This is good and useful (they can find reentrancy problems), but not practical for our scenario.

We’ll restructure the contract: pull out all external communications to a separate contract. Our ‘core’ contract will keep a minimal state and be just a numbers cruncher. Added bonus — it makes following CEI (checks-effects-interactions) almost automatic.

AMMPairEngine has addLiquidityStateChange as an internal function. It’s meant to be called by AMMPair (that inherits from AMMPairEngine ). The only public functions AMMPairEngine has are the invariants. If we don’t want them in the deployed code, they can be moved toAMMPairEngineTest is AMMPairEngine contract.

~/src/smtchecker_demo ❯❯❯ time solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol:AMMPairEngine 3.sol
Warning: CHC: Division by zero happens here.
Counterexample:
xReserves = 2, yReserves = 2, totalSupply = 0
depositX = 1
depositY = 1
oldSupply = 0
oldXReserves = 1
supplyAdded = 0
Transaction trace:
AMMPairEngine.constructor(1, 1)
State: xReserves = 1, yReserves = 1, totalSupply = 0
AMMPairEngine.invariantAddLiquidity(1, 1)
AMMPairEngine.addLiquidityStateChange(1, 1) -- internal call
--> 3.sol:117:43:
|
117 | assert(depositX / oldXReserves == supplyAdded / oldSupply);
| ^^^^^^^^^^^^^^^^^^^^^^^
Warning: CHC: Assertion violation happens here.
--> 3.sol:117:9:
|
117 | assert(depositX / oldXReserves == supplyAdded / oldSupply);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
solc --model-checker-engine chc --model-checker-show-unproved 0 3.sol 7.11s user 0.17s system 98% cpu 7.357 total

There’s a division by zero that causes assertion violation. The counterexample (depositX = 1; depositY = 1; oldSupply = 0) makes the problem obvious: the contract creator deposited 1e-18 of X and 1e-18 of Y tokens. This made the contract issue 0 LP tokens (1e-36 is too small to be represented with 18-decimal fixed-point math). We’ll switch to 36-decimal math and that should take care of that:

~/src/smtchecker_demo ❯❯❯ time solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol:AMMPairEngine 3.sol
Warning: CHC: Assertion violation might happen here.
--> 3.sol:117:9:
|
117 | assert(depositX / oldXReserves == supplyAdded / oldSupply);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
solc --model-checker-engine chc --model-checker-show-unproved 0 3.sol 75.19s user 0.50s system 99% cpu 1:16.27 total

Notice the change: there’s no division by zero and “Assertion violation happens here” is now “Assertion violation might happen here”. I don’t think it’s safe to interpret the uncertainty as “there are definitely no assertion violations here”, but it’s a partial success. I’ll need to do more digging to better understand what’s going on here.

UPDATE 09/05/2021: Leo Alt pointed out that ‘might happen’ is not good enough to call this ‘partial success’ — it’s really hard for SMTChecker to prove the assertion, so we can’t really rely on it:

FWIW, you can prove the math from the last example manually, but this clearly doesn’t scale. Assertion violation in the original code with a counterexample:

Prove that there’s no assertion violation in the new code:

Conclusion

SMTChecker can be your personal superpower — it probably needs some work, and your contracts need to be written with it in mind. But if the stars align, everybody could enjoy the benefits of automatic formal verification.

I’m hoping to spend some time looking deeper into SMTChecker, stay tuned.

Alternatives

  1. Manticore is a symbolic execution engine that can do things similar to SMTChecker. It is highly programmable — on one hand, it can do fewer things out of the box (invariantAddLiquidity has 2 arguments, SMTChecker explored all possible inputs for them; Manticore can’t do that). On the other hand, these things are implementable, plus we have more control over the verification process (maybe we can make some assumptions about external contracts?)
  2. Echidna is a fuzzing tool — uses a similar idea of invariants and randomly tries to find inputs that break them. It doesn’t prove that invariants hold (maybe it just failed to find that one edge case), but can be fast and discover a lot of non-edge-case flaws. Echidna uses the same syntaxis and Manticore, so they both can be used in parallel (at least in theory).
  3. Scribble takes a different approach — you annotate each function with dynamic invariants. It uses its own language for the invariants and can instrument your code with the materialized invariants.
  4. Myriad of static analysis/other fuzzing tools — they’re super useful, but out of the scope of this article

Acknowledgments

Alberto Cuesta Cañada for most of the references above and the baby AMM idea