Strange behavior in transferring a token (my_token.py in the tutorial)

moonhyeonah commented 4 years ago

OS / Environment

No LSB modules are available. Distributor ID: Ubuntu Description: Ubuntu 18.04.3 LTS Release: 18.04 Codename: bionic

Manticore version

Version: 0.3.3

Python version

Python 2.7.15+ Python 3.6.9

Dependencies

appdirs==1.4.3 attrdict==2.0.1 attrs==19.3.0 base58==1.0.3 black==19.10b0 capstone==4.0.1 certifi==2019.11.28 chardet==3.0.4 Click==7.0 crytic-compile==0.1.6 cytoolz==0.10.1 dataclasses==0.7 eth-abi==2.0.0 eth-account==0.4.0 eth-hash==0.2.0 eth-keyfile==0.5.1 eth-keys==0.2.4 eth-rlp==0.1.2 eth-typing==2.2.1 eth-utils==1.8.4 etheno==0.2.4 Flask==1.1.1 future==0.18.2 hexbytes==0.2.0 idna==2.8 importlib-metadata==1.1.0 ipfshttpclient==0.4.12 itsdangerous==1.1.0 Jinja2==2.10.3 jsonschema==3.2.0 lru-dict==1.1.6 manticore==0.3.3 MarkupSafe==1.1.1 more-itertools==8.0.0 multiaddr==0.0.8 mypy-extensions==0.4.3 netaddr==0.7.19 parsimonious==0.8.1 pathspec==0.6.0 ply==3.11 prettytable==0.7.2 protobuf==3.11.1 ptyprocess==0.6.0 pycryptodome==3.9.4 pyelftools==0.26 pyevmasm==0.2.1 pygobject==3.26.1 pyrsistent==0.15.6 pysha3==1.0.2 python-apt==1.6.4 PyYAML==5.3 regex==2019.11.1 requests==2.22.0 rlp==1.2.0 six==1.13.0 slither-analyzer==0.6.8 toml==0.10.0 toolz==0.10.0 typed-ast==1.4.0 unicorn==1.0.2rc1 urllib3==1.25.7 varint==1.0.2 wasm==1.2 web3==5.3.0 websockets==8.1 Werkzeug==0.16.0 wrapt==1.11.2 z3-solver==4.8.7.0 zipp==0.6.0

Summary of the problem

In a token example, I found that a transferred balance is different from a balance that I transfer. The token example is my_token.py whose source code is listed below.

I have only to add two statements (marked by <==) to print token balances before and after the transfer in the generated file, user_00000000.tx.
A balance that I transfer is : 27606985387162255149739023449108101809804435888681546220650096895197408 (See the log)
but the transferred balance is : 6402041168327817257759176981204103791588120218845874896962060288 (See the log)

Can you explain why I got this strange result?

==== my_token.py ============================

from manticore.ethereum import ManticoreEVM, ABI
from manticore.core.smtlib import Operators, solver

###### Initialization ######

m = ManticoreEVM()
with open('my_token.sol') as f:
    source_code = f.read()

# Create one user account
# And deploy the contract
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)

###### Exploration ######

# - Call balances[user]
# - Call transfer with symbolic values
# - Call balances[user]
# Later we will compare the result of the first call to balances to the second
contract_account.balances(user_account)

symbolic_val = m.make_symbolic_value()
symbolic_to = m.make_symbolic_value()
contract_account.balances(symbolic_to)                              <== I added
# Transfer is called with symbolic values
# Manticore will fork and create state at each condition executed
contract_account.transfer(symbolic_to, symbolic_val)

contract_account.balances(symbolic_to)                              <== I added    
contract_account.balances(user_account)

# Check of properties ######

bug_found = False
# Explore all the forks
for state in m.ready_states:

    # state.plateform.transactions returns the list of transactions
    # state.plateform.transactions[0] is the contract creation
    # state.plateform.transactions[1] is the first transaction
    # state.plateform.transactions[-1] is the last transaction

    balance_before = state.platform.transactions[1].return_data
    balance_before = ABI.deserialize("uint", balance_before)

    balance_after = state.platform.transactions[-1].return_data
    balance_after = ABI.deserialize("uint", balance_after)

    # Check if it is possible to have balance_after > balance_before
    state.constrain(Operators.UGT(balance_after, balance_before))
    if state.is_feasible():
        print("Bug found! see {}".format(m.workspace))
        m.generate_testcase(state, 'Bug')
        bug_found = True

if not bug_found:
    print('No bug were found')

====================================

Step to reproduce the behavior

$ python3 my_token.py

Expected behavior

The transferred balance is equal to a balance that I transfer.

Actual behavior

The two balances are not equal as I explained in the summary.

Any relevant logs

=== user_00000000.tx ============================
Transactions No. 0
Type: CREATE (0)
From: normal0(0x12d48395f01aa25788b837590af8cd0649869b94)
To: contract0(0x53ad6d453265749686a41933cf77a9136258126)
Value: 0
Gas used: 3000000
Data: 0x608060405234801561001057600080fd5b5060646000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061025b806100646000396000f30060806040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806327e235e314610051578063a9059cbb146100a8575b600080fd5b34801561005d57600080fd5b50610092600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506100f5565b6040518082815260200191505060405180910390f35b3480156100b457600080fd5b506100f3600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061010d565b005b60006020528060005260406000206000915090505481565b6000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020546000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410151561022b57806000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550806000808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825401925050819055505b50505600a165627a7a723058202b343adef9e35ef93e5bb0fae9f7cdf7717ffe13ba8c0e64490419418b909cf70029
Return_data: 0x60806040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806327e235e314610051578063a9059cbb146100a8575b600080fd5b34801561005d57600080fd5b50610092600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506100f5565b6040518082815260200191505060405180910390f35b3480156100b457600080fd5b506100f3600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061010d565b005b60006020528060005260406000206000915090505481565b6000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020546000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410151561022b57806000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550806000808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825401925050819055505b50505600a165627a7a723058202b343adef9e35ef93e5bb0fae9f7cdf7717ffe13ba8c0e64490419418b909cf70029 (*)
Function call:
Constructor() -> RETURN

Transactions No. 1
Type: CALL (0)
From: normal0(0x12d48395f01aa25788b837590af8cd0649869b94)
To: contract0(0x53ad6d453265749686a41933cf77a9136258126)
Value: 0
Gas used: 281474976710655
Data: 0x27e235e300000000000000000000000012d48395f01aa25788b837590af8cd0649869b94
Return_data: 0x0000000000000000000000000000000000000000000000000000000000000064 (*)

Function call:
balances(107501054587600346746564236233897387702746520468) -> RETURN
return: 100 (*)

Transactions No. 2
Type: CALL (0)
From: normal0(0x12d48395f01aa25788b837590af8cd0649869b94)
To: contract0(0x53ad6d453265749686a41933cf77a9136258126)
Value: 0
Gas used: 281474976710655
Data: 0x27e235e30000000000000000000000000000000000000000000000000000000000000000 (*)
Return_data: 0x0000000000000000000000000000000000000000000000000000000000000000 (*)

Function call:
balances(0) -> RETURN (*)
return: 0 (*)

Transactions No. 3
Type: CALL (0)
From: normal0(0x12d48395f01aa25788b837590af8cd0649869b94)
To: contract0(0x53ad6d453265749686a41933cf77a9136258126)
Value: 0
Gas used: 281474976710655
Data: 0xa9059cbb000000000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000e0 (*)
Return_data: 0x

Function call:
transfer(0,27606985387162255149739023449108101809804435888681546220650096895197408) <== the balance I transfer to the account 0
-> STOP (*)    

Transactions No. 4
Type: CALL (0)
From: normal0(0x12d48395f01aa25788b837590af8cd0649869b94)
To: contract0(0x53ad6d453265749686a41933cf77a9136258126)
Value: 0
Gas used: 281474976710655
Data: 0x27e235e30000000000000000000000000000000000000000000000000000000000000000 (*)
Return_data: 0x00000000000f9000000000000000000004000000000000000000000000000000 (*)

Function call:
balances(0) -> RETURN (*)
return: 6402041168327817257759176981204103791588120218845874896962060288 (*)  <== the transferred balance at the account 0

Transactions No. 5
Type: CALL (0)
From: normal0(0x12d48395f01aa25788b837590af8cd0649869b94)
To: contract0(0x53ad6d453265749686a41933cf77a9136258126)
Value: 0
Gas used: 281474976710655
Data: 0x27e235e300000000000000000000000012d48395f01aa25788b837590af8cd0649869b94
Return_data: 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe5 (*)

Function call:
balances(107501054587600346746564236233897387702746520468) -> RETURN
return: 115792089237316195423570985008687907853269984665640564039457584007913129639909 (*)

ehennenfent commented 4 years ago

The two values in question (276069... and 640204...) are concretizations of symbolic values, meaning that the number displayed isn't the one-and-only canonical value, just a possibility that Z3 found. I think what's happening when we generate the debug trace is this:

We encounter symbolic_val as an argument to transfer. We ask Z3 for a concrete value (for the sake of the trace) and it gives us 276069...
Manticore performs the transfer, creating another symbol that is constrained to have the same value as symbolic_val
We call balance on symbolic_to. The result is the symbol from step 2. Manticore knows that this should have the same value as symbolic_val, but it has "forgotten" about the previously concretized value for symbolic_val because we only generated it for the debug trace. Therefore, when it asks Z3 for the concretized value, it will most likely get a different possible value. To confirm that this is what's happening, you could try constraining symbolic_val to some specific value at the start of execution and seeing whether you still get the unexpected result.

@feliam does the above look right to you? Perhaps, for usability's sake, we could consider constraining symbols to be equal to their first concretized value whenever we generate the debug traces.

Your thinking at the end seems sound to me:

state.constrain(Operators.UGT(balance_after, balance_before))
    if state.is_feasible():
        print("Bug found! see {}".format(m.workspace))

In general, using the solver to check whether the property you want holds on your symbols will be more effective than concretizing the values and checking them manually.

feliam commented 4 years ago

@moonhyeonah thank you for reporting this! @ehennenfent thank you for looking into this! Yes it looks like the example solution/concretization is not locked into the path constraint so calling the solver different times to get different concrete parts of the state refer to different solution set. We need a contraint=True here: https://github.com/trailofbits/manticore/blob/d29bf0c3151deb500579bf0ae578ef8dfe8d4363/manticore/ethereum/manticore.py#L1601 And in some other places too. This needs some rework.

trailofbits / manticore