From c930ed6ac286c4371ed2144075228fae5014f145 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 21 Feb 2020 11:13:58 +0700 Subject: [PATCH 1/2] Set origin to concrete creator address in creation tx --- mythril/laser/ethereum/transaction/symbolic.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 1a5178e3..a5ee883d 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -134,9 +134,7 @@ def execute_contract_creation( "gas_price{}".format(next_transaction_id), 256 ), gas_limit=8000000, # block gas limit - origin=symbol_factory.BitVecSym( - "origin{}".format(next_transaction_id), 256 - ), + origin=ACTORS["CREATOR"], code=Disassembly(contract_initialization_code), caller=ACTORS["CREATOR"], contract_name=contract_name, From a203cebffd4df94fbdf85e352ec18678cb64908d Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 21 Feb 2020 11:34:19 +0700 Subject: [PATCH 2/2] Add origin constraints to suicide & ether_thief mods --- mythril/analysis/modules/ether_thief.py | 5 ++++- mythril/analysis/modules/suicide.py | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index c0648167..798b48ca 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -14,6 +14,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction import ContractCreationTransaction from mythril.laser.smt import UGT, UGE +from mythril.laser.smt.bool import And log = logging.getLogger(__name__) @@ -90,7 +91,9 @@ class EtherThief(DetectionModule): This prevents false positives where the owner willingly transfers ownership to another address. """ if not isinstance(tx, ContractCreationTransaction): - constraints += [tx.caller != ACTORS.creator] + constraints.append( + And(tx.caller == ACTORS.attacker, tx.caller == tx.origin) + ) attacker_address_bitvec = ACTORS.attacker diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 6ef87d8e..6ab17315 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -5,6 +5,7 @@ from mythril.exceptions import UnsatError from mythril.analysis.modules.base import DetectionModule from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.symbolic import ACTORS +from mythril.laser.smt.bool import And from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) @@ -68,7 +69,9 @@ class SuicideModule(DetectionModule): for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ACTORS.attacker) + constraints.append( + And(tx.caller == ACTORS.attacker, tx.caller == tx.origin) + ) try: try: transaction_sequence = solver.get_transaction_sequence(