Formal Verification for Solidity Contracts

chrisethchriseth Posts: 170 ✭✭✭
edited October 2015 in Solidity


We just merged a first pull request that allows Solidity contracts to be formally verified using a toolkit called why3.
This means that a computer creates and checks a mathematical proof of assertions about the behaviour of the contract.
Only a small subset of Solidity is supported for now, but that makes it already possible to verify a recursive binary search routine on arrays:
https://gist.github.com/chriseth/0c671e0dac08c3630f47

In that example, it is assumed that the given array of integers is sorted and the formal verification toolkit verifies the assertions that

1. if the function returns -1, then none of the elements of the array is equal to the requested value
2. if the function returns some i which is not -1, then the element at position i is equal to the requested value.

As an important part of the verification, why3 actually also checks that arithmetic operations never overflow and you never divide by zero.

Disclaimer

This is a prototype, it is not guaranteed to be working for any meaning of "working" and especially the interface can change at any time.

How to use it on the example

The solidity compiler (only solc at latest develop for now) can translate the source code into a different programming language which can be understood by why3 (the language is a dialect of ocaml). To do that, call it as "solc --formal -o /tmp/output_directory/ source.sol". Furthermore, using special tags in the Solidity comments of the form "///@why3 ..." you can formulate assertions and requirements that can be understood by the why3 framework and will be literally inserted into the generated code.

After that, you can use "why3 ide /tmp/output_directory/solidity.mlw" to start a graphical version of the toolkit and perform the verification.

How to install why3

I am not aware of any binary packages, so you have to download the source from the website.
As why3 itself is only a frontend to the real workhorses, the provers, you need to install a prover. I tried "alt-ergo" and Z3 - the first is part of the ubuntu distribution, the second has binaries for most platforms.

After installing the prover (and making sure it is in the PATH), call "why3 config --detect" and it should detect your prover.

How to use the why3 ide

I will just describe a quick way on how to "make all the ticks green".

The blue question marks on the left are assertions that are not yet known to be true or false. If you click on one of them and then on the "Alt-Ergo" or "Z3"-button, it will invoke the prover and try to prove the assertion. The default is to try for 6 seconds which is too short for the whole task for alt-ergo (Z3 will have no problems), but it is also more fun to see what the prover actually does, so let us do an interactive proof:

If you click on "VC for _find_internal" (assuming you are looking at the binary search example), it will show you the source code on the right. The marked parts of the source code are parts which the selected task will reason about. Green are positive assumptions, red are negative assumptions and orange are assumptions to be proven. The three "Strategies" buttons on the left will ask the prover to try a certain strategy. In this case, you should click on "Split", which will create several sub-goals to be proven. If you now click the "Alt-Ergo" button, it will try again to prove all the sub-goals but now allot 6 seconds for each sub-goal. The prover will succeed in verifying most of the sub-goals and the blue circles will turn green. If you repeat the same process for all blue circles, alt-ergo will eventually prove all the assertions.

How to verify your own contracts

Currently, only the types "uint256" and "uint256[] memory" are supported. If you want to use variables in verification conditions, you have to prefix them with "_" - this is done to avoid name clashes with why3. If you want to reference arguments to functions, use "arg_x" if the parameter is called "x" - this differentiates the initial argument from the mutable variable in the function (called "_x").

Comments

Sign In or Register to comment.