Sbuilder Ethereum Example

Install sbuilder-ethereum

Pre-requisites

Ruby

sbuilder-ethereum requires Ruby version later than 2.3.1. Use the command

ruby --version

to show the version of Ruby interpreter.

For example, this blog post uses Ruby version

ruby 2.3.1p112 (2016-04-26 revision 54768) [x86_64-linux]

Solidity solc compile

Sbuilder-ethereum uses Abstract Syntax Tree (AST) created Solidity solc compiler. Installation instruction for solc compiler can be found Ethrereum Solidity documentation

TLA+ tools

To run the formal model created by tla-sbuilder -tool, you must have Java and TLA+tools installed. TLA+ Tools jar can be obtained from download page, see TLA+ documentation for instructions on installing these tools.

Create Gemfile and install sbuilder-ethereum GEM

Create a Gemfile with the following content

source "https://rubygems.org"
gem 'sbuilder-ethereum'

and run

bundle install

to install sbuilder-ethereum GEM.

Version used in this blog entry

cat Gemfile.lock | grep sbuilder-ethereum
  sbuilder-ethereum (0.0.6)
sbuilder-ethereum

Initialize and Configure Environment

Create Directory Structure

Create directory structure for sbuilder

bundle exec sbuilder.rb init

and a directory for solidity source files

mkdir solidity

The directory structure after these commands is

.
├── cache
├── cnf
├── gen
├── solidity
└── src

5 directories

Following table summarizes the use of these directories:

Directory Use
cache working directory used internally by tla-sbuilder
gen working directory where formal model is created
cnf configuration directory
src TLA+ snippet repository, in this example used to store invariant operators
solidity Solidity source code files

Configure tla-sbuilder

tla-sbuilder uses configuration file cnf/sbuilder.yaml to

Refer chapter Configuration file cnf/sbuilder.yaml for the complete sbuilder.yaml configuration file.

Define Plugins

tla-sbuilder uses section extend.loaders in cnf/sbuilder.yaml configuration file to define extension plugins.

The following entry adds sbuilder-ethereum plugin to tla-sbuilder:

- className: Sbuilder::Ethereum::Plugin
  gem: sbuilder-ethereum
  configuration:
    solc_command: "/home/jj/work/sbuilder-ethereum/bin/solc"
  objects:
  - objectName: solcLoader
    configuration:

The plugin class is Sbuilder::Ethereum::Plugin in GEM sbuilder-ethereum. The location location of solc compiler is given using solc_command property.

The configuration also defines solcLoader object name, which is later used to refer to an object instance in Sbuilder::Ethereum::Plugin class.

Activate API Loader Extension Point

API interfaces in TLA+ formal model are loaded using interfaces section in cnf/sbuilder.yaml configuration file. Entries in this section activate API Loader Extension Point of tla-sbuilder.

In this example, interfaces section refers to solcLoader object name, defined in chapter Define Plugins, to invoke sbuilder-ethereum plugin.

- objectName: solcLoader
  url:

The url property accepts array of path names. For example, interfaces in Solidity file solidity/WithdrawalGame1.sol (ref. chapter Game 1 Solidity Implementation solidity/WithdrawalGame1.sol) are loaded when url array includes the following an entry:

- solidity/WithdrawalGame1.sol

Refer chapter Configuration file cnf/sbuilder.yaml for the complete sbuilder.yaml configuration file.

Activate Snippet Loader Extension Point

TLA+ Snippets are loaded into tla-sbuilder using Snippet Loader Extension Point. This extension point is activated using snippets section in cnf/sbuilder.yaml configuration file.

In this example, snippets implementing services for API interfaces configured in chapter Activate API Loader Extension Point are loading using entry:

- objectName: solcLoader
  snippets:

Snippet loader extension point is also used to load operators for checking implementation correctness (see chapters Invariant src/stack_ok and Invariant src/game_ok). Loading of these operators use SnippetLoaderSimple plugin, which is part of tla-sbuilder framework.

The example defines following entry in snippets section:

- className: Sbuilder::SnippetLoaderSimple
  snippets:
  - metatype: invariants
    appName: stack_ok
    url: src/stack_ok.tla
  - metatype: invariants
    appName: game_ok
    url: src/game_ok.tla

SnippetLoaderSimple uses properties

  • url : to point the file containing TLA+ code of the snippet
  • appName to give application domain name for the snippet
  • metatype to defined name space, where the snippet is mapped to in formal model context. metatype configuration allows one appName to mapped several elements in formal model.

The configuration above instantiates an un-named object for Sbuilder::SnippetLoaderSimple class, because there is no need to share context between API load step and snippet load step.

Refer chapter Configuration file cnf/sbuilder.yaml for the complete sbuilder.yaml configuration file.

Define Setups

To complete the runnable formal model Sbuilder uses setups. A setup is a sequence of interface operations, and their input parameters. Setup also define domain cardinalities, or domain values.

Setups are defined in setups section in cnf/sbuilder.yaml configuration file. Setup game1, with configuration in cnf/game1.yaml given chapter Setup Configuration cnf/game1.yaml, is defined using the following entry:

- setupDirectory: game1
  extensions:
  - url: cnf/game1.yaml

Activate Invariant

Invariant are activated using entries in invariants section in cnf/sbuilder.yaml. sbuilder-ethereum defines a few framework related invariant, which can be activated as shown below:

- accounts_type: account type valid
- accounts_unique: unique entries in eth_accounts
- storageRoot_unique: unique entries in eth_storageRoot
- accounts_valid: account id valid && account value valid
- total_value: SUM( accounts.balance ) + mined must be 0

Invariant loaded in chapter Activate Snippet Loader Extension Point are activated using the following entries in invariants section:

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

Game1 – Correct Implementation with Fair Player

Create Solidity Implementation for game1

This chapter presents elements in Solidity implementation for game1, show in chapter Game 1 Solidity Implementation solidity/WithdrawalGame1.sol.

WithdrawalGame state

address public richest;
uint public mostSent;
mapping (address => uint) pendingWithdrawals;

WithdrawalGame constructor

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

WithdrawalGame function becomeRichest

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

WithdrawalGame function withdraw is the target of attack. Correct implementation uses local variable amount and zeros refund before sending withdrawal amount to msg.sender.

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

A FairPlayer contract uses game member variable to point to WithdrawalGame contract:

WithdrawalGame game;

Constructor of FairPlayer initializes game member variable:

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

Functions play and endGame access methods becomeRichest and withdraw of WithdrawalGame

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

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

Configure Setup game1

A setup defines domains for contract data elements, and steps accessing contract function, mapped to formal model interfaces.

Define Domains

  # Define four account addresses acc1,acc2,acc3 and acc4

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

  # Ether value allow any integer value

- domain: eth_value
  type: Int

Steps in setup game1

  # 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: FairPlayer()
  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: FairPlayer(play)
  bindExact: true
  input:
      _default: 1
      recipient: 3
      sender: 1
      value: 0

  # step 6: play withDrawal game. Notice sender 'acc1' calls contract
  # 'FairPlayer' in address 'acc3'. FairPlayer calls
  # 'game.becomeRichest.value(2)()' on 'acc2', hence 'acc3' gets
  # pending withdrawal with value=2.

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

  # step 7: FairPlayer ends game (and retriever pending refunds)

- interface: FairPlayer(endGame)
  bindExact: true
  input:
      recipient: 3
      sender: 1
      _default: 1
      value: 0

Generate TLA+ Formal Model for game1

To generate a formal model for setup game1 run

bundle exec sbuilder.rb generate game1

The output shows some statistics.

generate setup: game1
Unmustache  src/ --> cache/unmustache - start
Unmustache  src/ --> cache/unmustache - done
Parse snippet from repository cache/unmustache - start
 Initialize parserResolver context symbols
   4 TLA+ symbols
   6 SBuilder symbols
   24 model symbols
 Initialize parserResolver context symbols - done

Parse snippet from repository cache/unmustache - done: parsed 0 snippets

Run Model Checking for game1

Running TLA+tools model checking on setup game1 with the following commands

export TLATOOLS_JAR=~/java/tla/tla2tools.jar
export SETUP=game1
cd gen/$SETUP/tla; 

java -cp $TLATOOLS_JAR pcal.trans model 
java -cp $TLATOOLS_JAR tlc2.TLC setup | tail -10

results to an output with the message Model checking completed. No error has been found. indicating that all invariant are respected.

pcal.trans Version 1.8 of 2 Apr 2013
Parsing completed.
Warning: symbols were renamed.
Translation completed.
New file model.tla written.
New file model.cfg written.
<<"ABORT x3_WithdrawalGame_withdraw_">>
<<"ABORT x3_FairPlayer_endGame_">>
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.1E-15
  based on the actual fingerprints:  val = 4.9E-14
619 states generated, 585 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 128.
Finished. (2016-12-08 13:54:30)

Game2 – Correct Implementation with Attacker

Create Solidity Implementation for game2

The following code send method launches re-entrant attack by using re-entrant call to function withdraw:

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

See chapter Game 2 solidity Implementation solidity/WithdrawalGame2.sol for full game2 Solidity implementation.

Configure game2

Setup game2 uses the same domain configuration as setup game1 in chapter Define Domains.

Steps in game2 create WithdrawalGame and Attacker contract, which includes the attack code presented in chapter Create Solidity Implementation for game2.

  # 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 sender 'acc1' calls contract
  # Attacker in recipient address 'acc3'. Attacker further 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: Attacker in recipient address 'acc3' run endGame. Attacker
  # implements 'send' -method, which run re-entrant attack to
  # WithdrawalGame. Attack results to infinite loop, which should be
  # detected by 'stack_ok' invariant.

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

See chapter Setup Configuration cnf/game2.yaml for full setup configuration.

Add setup game2 to sbuilder.yaml

Setup game2 is included to tla-sbuilder generation using the following entry in setups -section in cnf/sbuilder.yaml configuration file:

- setupDirectory: game2
  extensions:
  - url: cnf/game2.yaml

Generate TLA+ Formal Model for game2

To generate a formal model for setup game2 run

bundle exec sbuilder.rb generate game2

Run Model Checking for game2

Running TLA+tools model checking on setup game2 with the following commands

export TLATOOLS_JAR=~/java/tla/tla2tools.jar
export SETUP=game2
cd gen/$SETUP/tla; 

java -cp $TLATOOLS_JAR pcal.trans model 
java -cp $TLATOOLS_JAR tlc2.TLC setup | grep Error

results to invariant stack_ok violated. The violation is due to the re-entrant attack, where stack grows larger than allowed by stack_ok invariant, defined in chapter Invariant src/stack_ok.

pcal.trans Version 1.8 of 2 Apr 2013
Parsing completed.
Warning: symbols were renamed.
Translation completed.
New file model.tla written.
New file model.cfg written.
Error: Invariant invariant__stack_ok is violated.
Error: The behavior up to this point is:

Game3 – In-correct Implementation with Attacker

Create Solidity Implementation for game3

Re-entrant vulnerability is demonstrated using WithdrawalGameInErr contract

The error is present in withdraw function, where pendingWithdrawals is updated after calling send function.

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

For full Solidity implementation in game3 see chapter Game 3 solidity Implementation solidity/WithdrawalGame3.sol.

Configure Setup game3

Setup game3 uses the same domain configuration as setup game1 in chapter Define Domains.

Steps in game3 create vulnerable contract WithdrawalGameInErr, shown in chapter Create Solidity Implementation for game3, and an Attacker contract implementing re-entrant attack, shown in chapter Create Solidity Implementation for game2.

  # 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: WithdrawalGameInErr()
  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: Attacker in recipient address 'acc3' runs
  # endGame. Attacker implements 'send' -method, which runs
  # re-entrant attack to WithdrawalGameInErr. The vulnerability
  # in 'WithdrawalGameInErr' allows attacker to steal money,
  # which is detected by invariant 'game_ok'.

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

For full game3 setup configuration see chapter Setup Configuration cnf/game3.yaml

Add setup game3 to sbuilder.yaml

Setup game3 is included to tla-sbuilder generation using the following entry in setups -section in cnf/sbuilder.yaml configuration file:

- setupDirectory: game3
  extensions:
  - url: cnf/game3.yaml

Generate TLA+ Formal Model for game3

To generate a formal model for setup game3 run

bundle exec sbuilder.rb generate game3

Run Model Checking for game3

To run TLA+tools model checking for setup game3 use following commands

export TLATOOLS_JAR=~/java/tla/tla2tools.jar
export SETUP=game3
cd gen/$SETUP/tla; 

java -cp $TLATOOLS_JAR pcal.trans model 
java -cp $TLATOOLS_JAR tlc2.TLC setup | grep Error

The output shows how re-entrant attack succeeds in stealing value, resulting violation of stack_ok invariant, defined in chapter Invariant src/game_ok.

pcal.trans Version 1.8 of 2 Apr 2013
Parsing completed.
Warning: symbols were renamed.
Translation completed.
New file model.tla written.
New file model.cfg written.
Error: Invariant invariant__game_ok is violated.
Error: The behavior up to this point is:

Files

This chapter lists all files used in this example. The files and their directory location is shown in the following diagram:

.
├── cnf
│   ├── game1.yaml
│   ├── game2.yaml
│   ├── game3.yaml
│   └── sbuilder.yaml
├── Gemfile
├── Gemfile.lock
├── solidity
│   ├── WithdrawalGame1.sol
│   ├── WithdrawalGame2.sol
│   └── WithdrawalGame3.sol
└── src
    ├── game_ok.tla
    └── stack_ok.tla

3 directories, 11 files

Gemfile

source "https://rubygems.org"
gem 'sbuilder-ethereum'

Configuration file cnf/sbuilder.yaml

preferences:
  debug-output: false
extend:
  loaders:
     - className: Sbuilder::Ethereum::Plugin
       gem: sbuilder-ethereum
       configuration:
         solc_command: "/home/jj/work/sbuilder-ethereum/bin/solc"
       objects:
       - objectName: solcLoader
         configuration:
interfaces:
     - objectName: solcLoader
       url:
         - solidity/WithdrawalGame1.sol
         - solidity/WithdrawalGame2.sol
         - solidity/WithdrawalGame3.sol
snippets:
     - objectName: solcLoader
       snippets: 
     - className: Sbuilder::SnippetLoaderSimple
       snippets:
       - metatype: invariants
         appName: stack_ok
         url: src/stack_ok.tla
       - metatype: invariants
         appName: game_ok
         url: src/game_ok.tla
setups:
     - setupDirectory: game1
       extensions:
       - url: cnf/game1.yaml
     - setupDirectory: game2
       extensions:
       - url: cnf/game2.yaml
     - setupDirectory: game3
       extensions:
       - url: cnf/game3.yaml
invariants:
     - accounts_type: account type valid
     - accounts_unique: unique entries in eth_accounts
     - storageRoot_unique: unique entries in eth_storageRoot
     - accounts_valid: account id valid && account value valid
     - total_value: SUM( accounts.balance ) + mined must be 0
     - invariant__stack_ok: stack is not allowed grow to deep
     - invariant__game_ok: value in game enough to pay pending withdrawals

Invariant src/game_ok

(* operator 'invariant__game_ok' validates that 'WithdrawalGame' posesses enough value to 
 * pay all 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 \in {  "WithdrawalGame", "WithdrawalGameInErr" }   : game contract
 * a.address = s.address                                         : join
 * 
 * a.balance > SumOfFunction( s.pendingWithdrawals :  enough value to pay all pending withdrawals
 *
*)

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 \in {  "WithdrawalGame", "WithdrawalGameInErr" }  /\ a.address = s.address => a.balance > SumOfFunction( s.pendingWithdrawals )

Invariant src/stack_ok

(* 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 means that a infinite recusion (is most likely) encountered.
 *
 *)

invariant__stack_ok == \A se \in DOMAIN stack: Len(stack[se]) <= 20

Game 1 Solidity Implementation solidity/WithdrawalGame1.sol

Solidity implementation for setup game1 in file solidity/WithdrawalGame1.sol

 pragma solidity ^0.4.0;

 contract WithdrawalGame {
     address public richest;
     uint public mostSent;
     mapping (address => uint) pendingWithdrawals;

     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 WithdrawalGame() payable {
         richest = msg.sender;
         mostSent = msg.value;
     }

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

 }


contract FairPlayer {

     WithdrawalGame game;

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

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

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

}

Game 2 solidity Implementation solidity/WithdrawalGame2.sol

Solidity implementation for setup game2 in file solidity/WithdrawalGame2.sol

 pragma solidity ^0.4.0;

 contract WithdrawalGame {
     address public richest;
     uint public mostSent;
     mapping (address => uint) pendingWithdrawals;

     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 WithdrawalGame() payable {
         richest = msg.sender;
         mostSent = msg.value;
     }

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

 }


contract Attacker {

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

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

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

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

}

Game 3 solidity Implementation solidity/WithdrawalGame3.sol

Solidity implementation for setup game3 in file solidity/WithdrawalGame3.sol.

pragma solidity ^0.4.0;

contract WithdrawalGameInErr {
    address public richest;
    uint public mostSent;
    mapping (address => uint) pendingWithdrawals;

    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 WithdrawalGameInErr() payable {
        richest = msg.sender;
        mostSent = msg.value;
    }


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

}

Notice that game3 uses Attacker defined in game2.

Setup Configuration cnf/game1.yaml

- domain-extension:

         # Define four account addresses acc1,acc2,acc3 and acc4

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

         # Ether value allow any integer value

       - domain: eth_value
         type: Int

- 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: FairPlayer()
         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: FairPlayer(play)
         bindExact: true
         input:
             _default: 1
             recipient: 3
             sender: 1
             value: 0

         # step 6: play withDrawal game. Notice sender 'acc1' calls contract
         # 'FairPlayer' in address 'acc3'. FairPlayer calls
         # 'game.becomeRichest.value(2)()' on 'acc2', hence 'acc3' gets
         # pending withdrawal with value=2.

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

         # step 7: FairPlayer ends game (and retriever pending refunds)

       - interface: FairPlayer(endGame)
         bindExact: true
         input:
             recipient: 3
             sender: 1
             _default: 1
             value: 0

Setup Configuration cnf/game2.yaml

- domain-extension:

         # Define four account addresses acc1,acc2,acc3 and acc4

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

         # Ether value allow any integer value

       - domain: eth_value
         type: Int

- 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 sender 'acc1' calls contract
         # Attacker in recipient address 'acc3'. Attacker further 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: Attacker in recipient address 'acc3' run endGame. Attacker
         # implements 'send' -method, which run re-entrant attack to
         # WithdrawalGame. Attack results to infinite loop, which should be
         # detected by 'stack_ok' invariant.

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

Setup Configuration cnf/game3.yaml

- domain-extension:

         # Define four account addresses acc1,acc2,acc3 and acc4

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

         # Ether value allow any integer value

       - domain: eth_value
         type: Int

- 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: WithdrawalGameInErr()
         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: Attacker in recipient address 'acc3' runs
         # endGame. Attacker implements 'send' -method, which runs
         # re-entrant attack to WithdrawalGameInErr. The vulnerability
         # in 'WithdrawalGameInErr' allows attacker to steal money,
         # which is detected by invariant 'game_ok'.

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

Fin

This post has presented, how tla-sbuilder with sbuilder-ethererum plugin can be used to check correctness of Ethereum Solidity language contracts. The topics covered are

  • configuration of TLA-sbuilder
  • definition of correctness criteria using TLA+ language operators
  • use of tla-sbuilder API loader extension point to load interfaces corresponding Solidity contract function signatures
  • use of tla-sbuilder snippet loader extension point to load TLA+ snippets corresponding Solidity contract function implementation
  • creating tla-sbuilder setups corresponding to application environment
  • translation of Solidity implementation to formal model in TLA+ language
  • model checking of the formal model using TLA+tools
Advertisements

2 thoughts on “Sbuilder Ethereum Example

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s