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.
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
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
As a first step, we’ll try running the proofs for one of the example contracts provided in the
klab repository. Navigate to
Files to take a look at:
dapp/src/SafeAdd.sol, Solidity source.
src/specification.act.md, our specification written in
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:
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.
klabwhere 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
Navigate back to
SafeAdd/ and run
klab build to compile our
K “rules”. You can see the generated rules under
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
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
- error in
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