Merge branch 'develop' into modules_usability

README.md

@@ -12,7 +12,7 @@
 [![Pypi Installs](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril)
 [![DockerHub Pulls](https://img.shields.io/docker/pulls/mythril/myth.svg?label=DockerHub Pulls)](https://cloud.docker.com/u/mythril/repository/docker/mythril/myth)
 
-Mythril is a security analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains. It uses symbolic execution, SMT solving and taint analysis detect a variety of security vulnerabilities. It's also used (in combination with other tools and techniques) in the [MythX](https://mythx.io) security analysis platform.
+Mythril is a security analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains. It uses symbolic execution, SMT solving and taint analysis detect a variety of security vulnerabilities. It's also used (in combination with other tools and techniques) in the [MythX](https://mythx.io) security analysis platform.
 
 If you are a smart contract developer, we recommend using [MythX tools](https://github.com/b-mueller/awesome-mythx-smart-contract-security) which are optimized for usability and cover a wider range of security issues.
 

mythril/analysis/module/module_helpers.py

@@ -0,0 +1,6 @@
+import traceback
+
+
+def is_prehook() -> bool:
+    """Check if we are in prehook.  One of Bernhard's trademark hacks!"""
+    return "pre_hook" in traceback.format_stack()[-5]

mythril/analysis/module/modules/dependence_on_predictable_vars.py

@@ -9,10 +9,10 @@ from mythril.exceptions import UnsatError
 from mythril.analysis import solver
 from mythril.laser.smt import ULT, symbol_factory
 from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS
+from mythril.analysis.module.module_helpers import is_prehook
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from typing import cast, List
-import traceback
 
 log = logging.getLogger(__name__)
 
@@ -20,11 +20,6 @@ predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"]
 final_ops = ["CALL", "SUICIDE", "STOP", "RETURN"]
 
 
-def is_prehook() -> bool:
-    """Check if we are in prehook.  One of Bernhard's trademark hacks!"""
-    return "pre_hook" in traceback.format_stack()[-5]
-
-
 class PredictableValueAnnotation:
     """Symbol annotation used if a variable is initialized from a predictable environment variable."""
 

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 AccidentallyKillable(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,