Skip to content

Instantly share code, notes, and snippets.

Forked from chriseth/0
Created Sep 27, 2018
What would you like to do?
Formal verification for re-entrant Solidity contracts

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 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 corresponds to

  if (!
  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.

/// @why3 invariant { to_int - to_int this.balance }
contract Fund {
uint shares;
function withdraw(uint amount) {
if (amount < shares) {
shares -= amount; // subtract the amount from the shares
if (! // send the actual money / ether
module UInt256
use import
type uint256
constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
clone export with
type t = uint256,
constant max = max_uint256
module Contract_Fund
use import ref.Ref
use import int.ComputerDivision
use import UInt256
exception Ret
exception Revert
type state = {
_shares: uint256
type account = {
balance: uint256;
storage: state
(* This is the invariant that is specified as part of the solidity source code *)
function invariantFun (this: account): int = to_int - to_int this.balance
(* This models a potential recursive call (or much more complicated changes
* to the state) because it asserts nothing apart from the invariant *)
type call_result = { success: bool; new_state: account }
val call_external (this: account): call_result
ensures { result.success = false -> this = result.new_state }
ensures { result.success = true ->
(invariantFun this) = (invariantFun result.new_state) }
(* TODO: the code has to reject incoming ether and this functionality has
* to be part of the model *)
(* This is the translation of the actual Solidity function *)
let _withdraw (this: account) (arg_amount: uint256):
(* This will be auto-inserted by solidity *)
ensures { invariantFun (old this) = invariantFun result }
let storage_shares = ref in
let this_snapshot = ref {balance = this.balance; storage = {_shares =}} in
let _amount = ref arg_amount in
if ((!(_amount) <= !storage_shares)) then
storage_shares := !(storage_shares) - !(_amount);
(* this models *)
let call_result = (
if (!_amount) <= (!this_snapshot).balance then
call_external {balance = (!this_snapshot).balance - !_amount; storage = {_shares = !(storage_shares)}}
{ success = false; new_state = {balance = (!this_snapshot).balance; storage = {_shares = !(storage_shares)}}}
) in
this_snapshot := call_result.new_state;
if not (call_result.success) then
raise Revert;
raise Ret
Ret -> (!this_snapshot) |
Revert -> this
(* The browser version of why3 requires a "main" function *)
module Test
let main () = 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment