Create a gist now

Instantly share code, notes, and snippets.

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 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.

/// @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;
}
}
}
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

Nice. But what does this line - !msg.sender.call.value(amount)() do?

@hiddentao It's like a send with no gas limit.

@chriseth Well done! 👍

pirapira commented Jul 9, 2016

This is nice. Since the invariant has to be enforced on every method, this approach actually produces contracts with very high integrity. I have two comments.

  • Fund.sol, line 5 should check <= instead of <. It's OK in the Why code.
  • Instead of rejecting incoming Ether, you can change the conditions:
32: ensures { result.success = true ->
      (invariantFun this) <= (invariantFun result.new_state) }
42: ensures { invariantFun (old this) <= invariantFun result }

if you don't mind more Ether in the contract.

Owner

chriseth commented Jul 11, 2016 edited

@pirapira thank you, these are nice suggestions! I was wondering how to generalize invariantFun (old this) <= invariantFun result, and I think a more relaxed notion of a transition condition (like the one you gave) could also be used, which has access to the pre- and to the post-state. It could be dangerous because it has to be a transitive condition, but perhaps we could add another VC that actually asserts the transitivity.

insiderq commented Sep 5, 2016 edited

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment