This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.
Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.
The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made here is the following:
You cannot withdraw more than your shares, not by a recursive call exploit or any other means. Recursive calls are allowed, but the contract can still handle them fine.
More specifically, the difference between the total balance and the shares is constant across the lifetime of the contract. Thus, this difference is a so-called invariant.
All you need to do on the Solidity side is add this invariant as an annotation to the contract, as seen in the first line.
The Solidity compiler will then translate the contract into a language called why3 and use the why3 tools to verify that this invariant is indeed an invariant.
If you want to do that youself, go to http://why3.lri.fr/try/ copy the .mlw file into the text pane there and click on the gear symbol. Then, after some time, green ticks should appear on the right pane.
Oh and if you are in the mood, you can try moving the line that says
storage_shares := !(storage_shares) - !(_amount); to after
raise Revert; and click the gear sybmol again. This change
if (!msg.sender.call.value(amount)()) throw; shares -= amount;
i.e. a contract that is exploitable by recursive calls. The why3 tool should tell you that it was not able to verify the condition in that case.
This is a proof of concept that still needs to be verified by experts, but I think we are already quite far here.
What still needs to be done:
- model the actual "message", i.e. incoming ether, which needs to be rejected
- add a matching condition to the constructor
- add these features to the existing Solidity -> why3 translator
- add why3 to browser-solidity for ease of access
Note that these features still do not protect you from bugs in the compiler or the EVM. In order to get protection at this level, the formal model of the source code needs to be matched to the one of the generated bytecode. This is part of our ongoing research into formal verification.