[More Detail] [Collapse All]
Feature: Withdraw pattern of sending Ether


The recommended method of sending funds after an effect is using the
withdrawal  pattern in [http://solidity.readthedocs.io/en/develop/common-patterns.html].

This feature uses an example of the withdrawal pattern in practice
in a contract where the goal is to send the most money to the
contract in order to become the “richest”, inspired by King of the
Ether.

This feature is demonstrated using three scenarios
- scenario 1: Normal start without attack
- scenario 2: Game implementation correct attacker fails in stealing
- scenario 3: Game implementation erronous,  attacker steals value

Application correctness is verified using two invariant:

- invariant_game_ok: value in game enough to pay pending withdrawals
- invariant_stack_ok: stack is not allowed grow to deep

First scenario is used to check that game is working as expected. No
attack is launched. All invariant are resppected.

In second scenario, an attach launched using the following
re-entrant code method 'send'. 

            function send() {
             game.withdraw();
          }

Hower, this attack fails because implementation in 'withdraw'
function is correct, and it stores amount to transfer to a local
variable. Attack results to violation of 'invariant_stack_ok'.

In the third scenario, game implementation is erronous, and attacker
succeeds in stealing game value and causing violation of invariant
game_ok.
features/050-ether-balance/260-withdraw-attack.feature
- Background: Create 'WithdrawalGame' and define setups
link
features/050-ether-balance/260-withdraw-attack.feature:41
Given I create initial sbuilder context with:
Directory
solidity WithdrawalGame
setup setup1
And an entry in `snippets` -section in YAML file `cnf/sbuilder.yaml`:
#
#  Use 'SnippetLoaderSimple' to load 'invariant' 'stack_ok'
#  from a file 'src/stack_ok.tla' (which we populate later).
#  Simple snippet loader is passed name of snippet in the file
#  ('invariant_stack_ok' in this case)
#
- className: Sbuilder::SnippetLoaderSimple 
  snippets:

       - metatype: invariants
         appName: stack_ok
         name: invariant_stack_ok
         url: src/stack_ok.tla

       - metatype: invariants
         appName: game_ok
         name: invariant_game_ok
         url: src/game_ok.tla
And an entry in `invariants` -section in YAML file `cnf/sbuilder.yaml`:
- invariant_stack_ok: stack is not allowed grow to deep
And an entry in `invariants` -section in YAML file `cnf/sbuilder.yaml`:
- invariant_game_ok: value in game enough to pay pending withdrawals
And a file named "src/stack_ok.tla" with:
(* Define operator 'invariant_stack_ok' to guard against stack size growing to large.
   TLA-tools model checking mode uses breadth-first approach for the
state space exploration (default), and havig stack depth so large 
    meands that a infinite recusion (is most likely) encountered.
 *)

invariant_stack_ok == \A se \in DOMAIN stack: Len(stack[se]) <= 20
And a file named "src/game_ok.tla" with:
(* operator 'invariant_game_ok' checks when game is runnig value on a game contract
 * is sufficient to pay pending withdrawals. 
 * 
 * Len( eth_accounts_temp ) # 0    :  game transaction is running
 * Len( eth_storageRoot_temp) = Len( eth_accounts_temp ) : game is ready to run
 * 
 * a.codeHash = "WithdrawalContract" /\ a.address = s.address  : identify game account and contract
 * 
 * a.balance > SumOfFunction( s.pendingWithdrawals : correctness criterium
*)

invariant_game_ok ==
Len( eth_accounts_temp ) # 0  /\  Len( eth_storageRoot_temp) = Len( eth_accounts_temp ) =>
\A a \in Head(eth_accounts_temp):  \A s \in Head(eth_storageRoot_temp):
     a.codeHash = "WithdrawalGame" /\ a.address = s.address => a.balance > SumOfFunction( s.pendingWithdrawals )
- Scenario: Normal game start without attack
link

Expect to see balances:
          step                   acc1   acc2 acc3      richest   mostSent
                                 block  game attacke
step 1   create account acc1       -      -    - 
step 2   mine acc1                10      -    -
step 3   construct game            9      1    -         acc1      1
step 4   construct attacker        4      1    5         acc1      1
step 5   play game                 4      3    3         acc3      2
step 6   play game                 4      5    1         acc3      2      
step 7   withdraw                  4      1    5         acc3      2
features/050-ether-balance/260-withdraw-attack.feature:114
Given a file named "solidity/WithdrawalGame.sol" with:

   pragma solidity ^0.4.0;

   contract WithdrawalGame {
       address public richest;
       uint public mostSent;

       mapping (address => uint) pendingWithdrawals;

       function WithdrawalGame() payable {
           richest = msg.sender;
           mostSent = msg.value;
       }

       function becomeRichest() payable returns (bool) {
           if (msg.value >= mostSent) {
               pendingWithdrawals[richest] += msg.value;
               richest = msg.sender;
               mostSent = msg.value;
               return true;
           } else {
               return false;
           }
       }

       function withdraw() returns (bool) {
           uint amount = pendingWithdrawals[msg.sender];
           // Remember to zero the pending refund before
           pendingWithdrawals[msg.sender] = 0;

           // sending to prevent re-entrancy attacks
           if (msg.sender.send(amount)) {
               // open for re-entrant attack
               // pendingWithdrawals[msg.sender] = 0;
               return true;
           } else {
               pendingWithdrawals[msg.sender] = amount;
               return false;
           }
       }
   }

 // import "WithdrawalGame.sol";

  contract Attacker {

        WithdrawalGame game;

        function Attacker( WithdrawalGame g ) {
           game = g;
        }

        function play() {
           game.becomeRichest.value(2)();
        }

        function attack() {
           game.withdraw();
        }

        function send() {
           game.withdraw();
        }

  }
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:


     - domain: eth_address
       values:
          - acc1
          - acc2
          - acc3
          - acc4

       # Ether value range
     - domain: eth_value
       type: Int

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:

          # step 1,2: Create accounts acc1 with 10 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 1
                value: 10

          # step 3 : Account 'acc1' creates 'WithdrawalGame'
          # contract in address 'acc2', account 'acc1' becomes
          # richest (msg.value=1)

        - interface: WithdrawalGame()
          bindExact: true
          input:
              _default: 1
              value: 1
              sender: 1

        # step 4 : Account 'acc1' creates attacker in 'acc3'

        - interface: Attacker()
          bindExact: true
          input:
              _default: 1
              sender: 1
              value: 5
              g: 2

       # step 5: play withDrawal game. Notice 'acc1' calls
       # attacker in 'acc3', which calls 'game.becomeRichest.value(2)()'
       # on 'acc2'. Was previously richest, and now gets pending 
       # withdrawal to msg.value==2.

        - interface: Attacker(play)
          bindExact: true
          input:
              _default: 1
              recipient: 3
              sender: 1
              value: 0

       # step 6: play withDrawal game. Notice 'acc1' calls
       # attacker in 'acc3', which calls
       # 'game.becomeRichest.value(2)()' on 'acc2'. 'acc3' gets
       # pending withdrawal with value=2.

        - interface: Attacker(play)
          bindExact: true
          input:
              _default: 1
              recipient: 3
              sender: 1
              value: 0
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
3 step p_WithdrawalGame__
4 step p_Attacker__
5 step p_Attacker_play_
6 step p_Attacker_play_
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
2 eth_accounts acc1 balance 10
3 eth_accounts acc1 balance 9
3 eth_accounts acc2 balance 1
4 eth_accounts acc1 balance 4
4 eth_accounts acc2 balance 1
4 eth_accounts acc3 balance 5
5 eth_accounts acc1 balance 4
5 eth_accounts acc2 balance 3
5 eth_accounts acc3 balance 3
6 eth_accounts acc1 balance 4
6 eth_accounts acc2 balance 5
6 eth_accounts acc3 balance 1
Then State space extract `gen/setup1/tla/state.dump` contains
3 eth_storageRoot acc2 richest acc1
4 eth_storageRoot acc2 richest acc1
5 eth_storageRoot acc2 richest acc3
6 eth_storageRoot acc2 richest acc3
Then State space extract `gen/setup1/tla/state.dump` contains
3 eth_storageRoot acc2 mostSent 1
4 eth_storageRoot acc2 mostSent 1
5 eth_storageRoot acc2 mostSent 2
6 eth_storageRoot acc2 mostSent 2
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
5 eth_storageRoot pendingWithdrawals acc1 2
5 eth_storageRoot pendingWithdrawals acc2 0
5 eth_storageRoot pendingWithdrawals acc3 0
6 eth_storageRoot pendingWithdrawals acc1 2
6 eth_storageRoot pendingWithdrawals acc2 0
6 eth_storageRoot pendingWithdrawals acc3 2
- Scenario: Game implementation correct attacker fails in stealing
link
features/050-ether-balance/260-withdraw-attack.feature:330
Given a file named "solidity/WithdrawalGame.sol" with:

   pragma solidity ^0.4.0;

   contract WithdrawalGame {
       address public richest;
       uint public mostSent;

       mapping (address => uint) pendingWithdrawals;

       function WithdrawalGame() payable {
           richest = msg.sender;
           mostSent = msg.value;
       }

       function becomeRichest() payable returns (bool) {
           if (msg.value >= mostSent) {
               pendingWithdrawals[richest] += msg.value;
               richest = msg.sender;
               mostSent = msg.value;
               return true;
           } else {
               return false;
           }
       }

       function withdraw() returns (bool) {
           uint amount = pendingWithdrawals[msg.sender];
           // Remember to zero the pending refund before
           pendingWithdrawals[msg.sender] = 0;

           // sending to prevent re-entrancy attacks
           if (msg.sender.send(amount)) {
               // open for re-entrant attack
               // pendingWithdrawals[msg.sender] = 0;
               return true;
           } else {
               pendingWithdrawals[msg.sender] = amount;
               return false;
           }
       }
   }

 // import "WithdrawalGame.sol";

  contract Attacker {

        WithdrawalGame game;

        function Attacker( WithdrawalGame g ) {
           game = g;
        }

        function play() {
           game.becomeRichest.value(2)();
        }

        function attack() {
           game.withdraw();
        }

        function send() {
           game.withdraw();
        }

  }
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:


     - domain: eth_address
       values:
          - acc1
          - acc2
          - acc3
          - acc4

       # Ether value range
     - domain: eth_value
       type: Int

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:

          # step 1,2: Create accounts acc1 with 10 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 1
                value: 10

          # step 3 : Account 'acc1' creates 'WithdrawalGame'
          # contract in address 'acc2', account 'acc1' becomes
          # richest (msg.value=1)

        - interface: WithdrawalGame()
          bindExact: true
          input:
              _default: 1
              value: 1
              sender: 1

        # step 4 : Account 'acc1' creates attacker in 'acc3'

        - interface: Attacker()
          bindExact: true
          input:
              _default: 1
              sender: 1
              value: 5
              g: 2

       # step 5: play withDrawal game. Notice 'acc1' calls
       # attacker in 'acc3', which calls 'game.becomeRichest.value(2)()'
       # on 'acc2'. Was previously richest, and now gets pending 
       # withdrawal to msg.value==2.

        - interface: Attacker(play)
          bindExact: true
          input:
              _default: 1
              recipient: 3
              sender: 1
              value: 0

       # step 6: play withDrawal game. Notice 'acc1' calls
       # attacker in 'acc3', which calls
       # 'game.becomeRichest.value(2)()' on 'acc2'. 'acc3' gets
       # pending withdrawal with value=2.

        - interface: Attacker(play)
          bindExact: true
          input:
              _default: 1
              recipient: 3
              sender: 1
              value: 0

       # step 7: attack withDrawal game 

        - interface: Attacker(attack)
          bindExact: true
          input:
              recipient: 3
              sender: 1
              _default: 1
              value: 0
When I generate, translate, and model check setup `setup1` to find violation in `invariant_stack_ok`
- Scenario: Game implementation erronous, attacker steals value
link
features/050-ether-balance/260-withdraw-attack.feature:497
Given a file named "solidity/WithdrawalGame.sol" with:

   pragma solidity ^0.4.0;

   contract WithdrawalGame {
       address public richest;
       uint public mostSent;

       mapping (address => uint) pendingWithdrawals;

       function WithdrawalGame() payable {
           richest = msg.sender;
           mostSent = msg.value;
       }

       function becomeRichest() payable returns (bool) {
           if (msg.value >= mostSent) {
               pendingWithdrawals[richest] += msg.value;
               richest = msg.sender;
               mostSent = msg.value;
               return true;
           } else {
               return false;
           }
       }

       function withdraw() returns (bool) {
           uint amount = pendingWithdrawals[msg.sender];
           // Remember to zero the pending refund before
           // pendingWithdrawals[msg.sender] = 0;

           // sending to prevent re-entrancy attacks
           if (msg.sender.send(amount)) {
               // open for re-entrant attack
               pendingWithdrawals[msg.sender] = 0;
               return true;
           } else {
               // pendingWithdrawals[msg.sender] = amount;
               return false;
           }
       }
   }

 // import "WithdrawalGame.sol";

  contract Attacker {

        WithdrawalGame game;

        function Attacker( WithdrawalGame g ) {
           game = g;
        }

        function play() {
           game.becomeRichest.value(2)();
        }

        function attack() {
           game.withdraw();
        }

        function send() {
           game.withdraw();
        }

  }
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:


     - domain: eth_address
       values:
          - acc1
          - acc2
          - acc3
          - acc4

       # Ether value range
     - domain: eth_value
       type: Int

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:

          # step 1,2: Create accounts acc1 with 10 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 1
                value: 10

          # step 3 : Account 'acc1' creates 'WithdrawalGame'
          # contract in address 'acc2', account 'acc1' becomes
          # richest (msg.value=1)

        - interface: WithdrawalGame()
          bindExact: true
          input:
              _default: 1
              value: 1
              sender: 1

        # step 4 : Account 'acc1' creates attacker in 'acc3'

        - interface: Attacker()
          bindExact: true
          input:
              _default: 1
              sender: 1
              value: 5
              g: 2

       # step 5: play withDrawal game. Notice 'acc1' calls
       # attacker in 'acc3', which calls 'game.becomeRichest.value(2)()'
       # on 'acc2'. Was previously richest, and now gets pending 
       # withdrawal to msg.value==2.

        - interface: Attacker(play)
          bindExact: true
          input:
              _default: 1
              recipient: 3
              sender: 1
              value: 0

       # step 6: play withDrawal game. Notice 'acc1' calls
       # attacker in 'acc3', which calls
       # 'game.becomeRichest.value(2)()' on 'acc2'. 'acc3' gets
       # pending withdrawal with value=2.

        - interface: Attacker(play)
          bindExact: true
          input:
              _default: 1
              recipient: 3
              sender: 1
              value: 0

       # step 7: attack withDrawal game 

        - interface: Attacker(attack)
          bindExact: true
          input:
              recipient: 3
              sender: 1
              _default: 1
              value: 0
When I generate, translate, and model check setup `setup1` to find violation in `invariant_game_ok`