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