Smart contract code is guilty until proven innocent.


Hundreds of millions $USD worth of assets have been locked in yield farming contracts that have not been audited by an uninterested third party, let alone proven correct by formal methods. Worse still, SushiSwap, with more than $USD 100m in assets locked, was audited and found wanting.

I can’t blame Chef Nomi for people trusting in his code without due diligence. The law will see things differently. Developers should hesitate to deploy contracts that control user funds and are not well documented, tested, externally audited, and proven correct according to an open source formal specification.

To that end, how do we know that our code is correct, and how can we credibly guarantee this to our users?

The Ethereum Virtual Machine or EVM is an atomic state machine. Each transaction is a change from one state of the blockchain to the next. A correct program cannot reach any state that isn’t allowed to according to our specification.

Program designs are often informal or implicit. To verify that our code is correct, we need a formal specification, a description of our program’s allowed states. Once we have this, we can use a proof assistant to confirm whether our program matches the specification.

Let’s do a simple specification and verification.

To perform verification we use an SMT solver like Z3.

Z3 doesn’t speak Solidity, and we’d rather verify at the bytecode level anyway so that bugs don’t slip in during compilation. We need a formal specification of the EVM semantics for Z3 to use, so that it knows which state changes are possible for the EVM.

The best option is the KEVM, implemented in K which is designed for specifying and designing languages.

klab provides a high level specification language called act that we will use for specifying programs. klab can translate our act spec to K) and feed it to Z3 to run based on the rules of the KEVM.

To get started, install klab from GitHub, taking care to make sure you have the dependencies installed correctly. I plan to create a Dockerfile for conveniently running klab in the future.

As a first step, we’ll try running the proofs for one of the example contracts provided in the klab repository. Navigate to klab/examples/SafeAdd directory.

Files to take a look at:

  • dapp/src/SafeAdd.sol, Solidity source.
  • src/specification.act.md, our specification written in act.
behaviour add of SafeAdd
interface add(uint256 X, uint256 Y)
iff in range uint256

    X + Y

iff

    VCallValue == 0

returns X + Y

This specification states the following:

Contract SafeAdd has the function add, which takes two 256 bit unsigned integers as input.

Function should revert if X + Y exceeds limit of uint256.

Function should revert if ether is sent as part of the call.

Otherwise, should return X + Y.

  • config.json tells klab where to look for our files

First, let’s compile our contract. Navigate to the dapp/ directory and run solc --combined-json=abi,bin,bin-runtime,srcmap,srcmap-runtime,ast src/SafeAdd.sol > out/dapp.sol.json to compile SafeAdd.sol and output the bytecode in out/dapp.sol.json.

Navigate back to SafeAdd/ and run klab build to compile our specification.act.md to K “rules”. You can see the generated rules under SafeAdd/out/specs/.

If this works with no errors, you can run klab prove --dump <rule> to attempt to prove the generated K code. The --dump flag tells klab to output result logs. To learn the rule name, open one of the files in SafeAdd/out/specs/ and Ctrl+F “rule”. You will find a line like rule [SafeAdd.add.pass.rough]:. In this case, run klab prove --dump SafeAdd_add_pass_rough. The results will be logged tersely in terminal as well as output in format SafeAdd/out/data/<hash>.log. You can explore the results of the proof using klab debug <hash>. If this works for all the rules, congratulations, your code has been proven to conform to its specification.

Formal verification is the best guarantee of code’s correct behavior. You should keep in mind the method’s failure points:

  • error in specification
  • error in KEVM
  • error in K itself

Of these, an error in your own specification demands the most caution. No testing method should be relied upon in isolation, and the odds of a bug escaping unit tests, static analysis, fuzzing, and formal verification all together approaches zero.

Stay tuned for more posts about formal verification and smart contract security. Next time, we’ll try adding a new sub() function to SafeAdd. One small step towards a proven SafeMath.sol.