Merge pull request #1338 from ConsenSys/creator_origin_fix

Add constraints on tx.origin

mythril/analysis/module/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__)
 
@@ -86,7 +87,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
 

mythril/analysis/module/modules/suicide.py

@@ -5,6 +5,7 @@ from mythril.exceptions import UnsatError
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 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(

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,