From a250f40baaa13d6a8c7a331ca95145d0eb34aac6 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 5 Mar 2020 15:13:02 +0100 Subject: [PATCH] Revert Ether thief change & introduce symbolic starting balance --- mythril/analysis/module/modules/ether_thief.py | 12 ++++++------ mythril/laser/ethereum/state/world_state.py | 9 +++++++-- .../laser/ethereum/transaction/transaction_models.py | 2 +- 3 files changed, 14 insertions(+), 9 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index be3939df..f8d9424b 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -40,7 +40,7 @@ class EtherThief(DetectionModule): swc_id = UNPROTECTED_ETHER_WITHDRAWAL description = DESCRIPTION entry_point = EntryPoint.CALLBACK - pre_hooks = ["STOP"] + pre_hooks = ["CALL", "STATICCALL"] def reset_module(self): """ @@ -70,16 +70,16 @@ class EtherThief(DetectionModule): """ state = copy(state) instruction = state.get_current_instruction() + to = state.mstate.stack[-2] constraints = copy(state.world_state.constraints) - attacker_address_bitvec = ACTORS.attacker - constraints += [ + to == ACTORS.attacker, UGT( - state.world_state.balances[attacker_address_bitvec], - state.world_state.starting_balances[attacker_address_bitvec], - ) + state.world_state.balances[ACTORS.attacker], + state.world_state.starting_balances[ACTORS.attacker], + ), ] potential_issue = PotentialIssue( diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 89c9ed6e..9f86b6e5 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -125,7 +125,7 @@ class WorldState: def create_account( self, - balance=0, + balance=None, address=None, concrete_storage=False, dynamic_loader=None, @@ -157,7 +157,12 @@ class WorldState: if code: new_account.code = code - new_account.set_balance(symbol_factory.BitVecVal(balance, 256)) + if balance is not None: + new_account.set_balance(symbol_factory.BitVecVal(balance, 256)) + else: + new_account.set_balance( + symbol_factory.BitVecSym("initial)_balance_{}".format(address), 256) + ) self.put_account(new_account) return new_account diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 71630a07..280c154b 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -202,7 +202,7 @@ class ContractCreationTransaction(BaseTransaction): contract_address if isinstance(contract_address, int) else None ) callee_account = world_state.create_account( - 0, concrete_storage=True, creator=caller.value, address=contract_address + concrete_storage=True, creator=caller.value, address=contract_address ) callee_account.contract_name = contract_name or callee_account.contract_name # init_call_data "should" be false, but it is easier to model the calldata symbolically