From a203cebffd4df94fbdf85e352ec18678cb64908d Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 21 Feb 2020 11:34:19 +0700 Subject: [PATCH] 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(