Formal verification for re-entrant Solidity contracts

0 README.md

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

  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.

1 Fund.sol

/// @why3 invariant { to_int this.storage._shares - to_int this.balance }
contract Fund {
    uint shares;
    function withdraw(uint amount) {
        if (amount < shares) {
            shares -= amount; // subtract the amount from the shares
            if (!msg.sender.call.value(amount)()) // send the actual money / ether
                throw;
        }
    }
}

2 Fund.mlw

module UInt256
	use import mach.int.Unsigned
	type uint256
	constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
	clone export mach.int.Unsigned with
		type t = uint256,
		constant max = max_uint256
end

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 this.storage._shares - 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):
			(account)
			(* This will be auto-inserted by solidity *)
			ensures { invariantFun (old this) = invariantFun result }
		=
		let storage_shares = ref this.storage._shares in
		let this_snapshot = ref {balance = this.balance; storage = {_shares = this.storage._shares}} in
		let _amount = ref arg_amount in
		try
		begin
			if ((!(_amount) <= !storage_shares)) then
			begin
				storage_shares := !(storage_shares) - !(_amount);
				(* this models msg.sender.call.value(_amount)() *)
				let call_result = (
					if (!_amount) <= (!this_snapshot).balance then
						call_external {balance = (!this_snapshot).balance - !_amount; storage = {_shares = !(storage_shares)}}
					else
						{ 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;
			end
		end;
		raise Ret
		with
			Ret -> (!this_snapshot) |
			Revert -> this
	end
end

(* The browser version of why3 requires a "main" function *)
module Test
  let main () = 0
end

First of all awesome project. I'm currently working in a startup that issues stocks on ethereum and also underway academic research on formal verification.

I'm trying to reproduce what you're done here with online solidity compiler https://ethereum.github.io/browser-solidity/ it has a formal verification tab that generates code with prompt to test that on http://why3.lri.fr/try/ but the code generated differs from your's.

The latest build is showing the following code that fails on try on the line 30 starting with invariant word. Can you please explain what happened?

module UInt256
    use import mach.int.Unsigned
    type uint256
    constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
    clone export mach.int.Unsigned with
        type t = uint256,
        constant max = max_uint256
end

module Contract_Fund
    use import int.Int
    use import ref.Ref
    use import map.Map
    use import array.Array
    use import int.ComputerDivision
    use import mach.int.Unsigned
    use import UInt256
    exception Revert
    exception Return
    type state = {
        mutable _shares: uint256
    }
    type account = {
        mutable balance: uint256;
        storage: state
    }
    val external_call (this: account): bool
        ensures { result = false -> this = (old this) }
        writes { this }
        invariant { to_int this.storage._shares - to_int this.balance }
    let rec _withdraw (this: account) (arg_amount: uint256):
            ()
        invariant { to_int this.storage._shares - to_int this.balance }
        writes { this }
        =
        let prestate = {balance = this.balance; storage = {_shares = this.storage._shares}} in 
        let _amount = ref arg_amount in
        try
        begin
            if (!(_amount) < this.storage._shares) then
            begin
                this.storage._shares <- (this.storage._shares - !(_amount));
                if (not (
                    let amount = 0 in let amount = !(_amount) in 
                    if amount <= this.balance then
                        let balance_precall = this.balance in
                        begin
                            this.balance <- this.balance - amount;
                            if not (external_call this) then begin this.balance = balance_precall; false end else true
                        end
                    else false
                )) then
                begin
                    raise Revert
                end
            end
        end;
        raise Return
        with Return -> () |
             Revert -> this.balance <- prestate.balance; this.storage._shares <- prestate.storage._shares; ()
    end
end