diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 87dd5be0..65e5c8e8 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -6,10 +6,15 @@ from copy import copy from mythril.analysis import solver from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue -from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.symbolic import ( + ATTACKER_ADDRESS, + CREATOR_ADDRESS, +) from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.transaction import ContractCreationTransaction + from mythril.laser.smt import UGT, symbol_factory, UGE log = logging.getLogger(__name__) @@ -82,6 +87,14 @@ class EtherThief(DetectionModule): that the Ether sent to the attacker's address is greater than the amount of Ether the attacker sent. """ + for tx in state.world_state.transaction_sequence: + """ + Constraint: All transactions must originate from regular users (not the creator/owner). + This prevents false positives where the owner willingly transfers ownership to another address. + """ + if not isinstance(tx, ContractCreationTransaction): + constraints += [tx.caller != CREATOR_ADDRESS] + attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256) constraints += [ diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 9504c71a..b6959a82 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -196,7 +196,7 @@ def _set_minimisation_constraints( # Minimize minimize.append(transaction.call_data.calldatasize) - + minimize.append(transaction.call_value) constraints.append( UGE( symbol_factory.BitVecVal(1000000000000000000000, 256), @@ -204,14 +204,6 @@ def _set_minimisation_constraints( ) ) - # FIXME: This shouldn't be needed. - constraints.append( - UGE( - symbol_factory.BitVecVal(1000000000000000000000, 256), - transaction.call_value, - ) - ) - for account in world_state.accounts.values(): # Lazy way to prevent overflows and to ensure "reasonable" balances # Each account starts with less than 100 ETH