Merge remote-tracking branch 'origin/develop' into feature/enable_detection_plugins

.pre-commit-config.yaml

@@ -0,0 +1,7 @@
+# See https://pre-commit.com for more information
+# See https://pre-commit.com/hooks.html for more hooks
+repos:
+-   repo: https://github.com/psf/black
+    rev: 19.3b0
+    hooks:
+    -   id: black

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/base.py

@@ -45,7 +45,7 @@ class DetectionModule(ABC):
     name = "Detection Module Name"
     swc_id = "SWC-000"
     description = "Detection module description"
-    entry_point = EntryPoint.POST  # type: EntryPoint
+    entry_point = EntryPoint.CALLBACK  # type: EntryPoint
     pre_hooks = []  # type: List[str]
     post_hooks = []  # type: List[str]
 

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/analysis/module/modules/user_assertions.py

@@ -28,7 +28,7 @@ assertion_failed_hash = (
 class UserAssertions(DetectionModule):
     """This module searches for user supplied exceptions: emit AssertionFailed("Error")."""
 
-    name = "External calls"
+    name = "User assertions"
     swc_id = ASSERT_VIOLATION
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK

mythril/laser/ethereum/instructions.py

@@ -1697,20 +1697,37 @@ class Instruction:
         gas_price = environment.gasprice
         origin = environment.origin
 
-        contract_address = None
-        if create2_salt:
-            salt = hex(create2_salt)[2:]
-            salt = "0" * (64 - len(salt)) + salt
+        contract_address = None  # type: Union[BitVec, int]
+        Instruction._sha3_gas_helper(global_state, len(code_str[2:]) // 2)
 
-            addr = hex(caller.value)[2:]
-            addr = "0" * (40 - len(addr)) + addr
+        if create2_salt:
+            if create2_salt.symbolic:
+                if create2_salt.size() != 256:
+                    pad = symbol_factory.BitVecVal(0, 256 - create2_salt.size())
+                    create2_salt = Concat(pad, create2_salt)
+                address, constraint = keccak_function_manager.create_keccak(
+                    Concat(
+                        symbol_factory.BitVecVal(255, 8),
+                        caller,
+                        create2_salt,
+                        symbol_factory.BitVecVal(int(get_code_hash(code_str), 16), 256),
+                    )
+                )
+                contract_address = Extract(255, 96, address)
+                global_state.world_state.constraints.append(constraint)
+            else:
+                salt = hex(create2_salt.value)[2:]
+                salt = "0" * (64 - len(salt)) + salt
 
-            Instruction._sha3_gas_helper(global_state, len(code_str[2:]) // 2)
+                addr = hex(caller.value)[2:]
+                addr = "0" * (40 - len(addr)) + addr
 
-            contract_address = int(
-                get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:],
-                16,
-            )
+                contract_address = int(
+                    get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[
+                        26:
+                    ],
+                    16,
+                )
         transaction = ContractCreationTransaction(
             world_state=world_state,
             caller=caller,

mythril/laser/ethereum/keccak_function_manager.py

@@ -35,6 +35,7 @@ class KeccakFunctionManager:
         self._index_counter = TOTAL_PARTS - 34534
         self.hash_result_store = {}  # type: Dict[int, List[BitVec]]
         self.quick_inverse = {}  # type: Dict[BitVec, BitVec]  # This is for VMTests
+        self.concrete_hashes = {}  # type: Dict[BitVec, BitVec]
 
     @staticmethod
     def find_concrete_keccak(data: BitVec) -> BitVec:
@@ -85,8 +86,14 @@ class KeccakFunctionManager:
         length = data.size()
         func, inverse = self.get_function(length)
 
+        if data.symbolic is False:
+            concrete_hash = self.find_concrete_keccak(data)
+            self.concrete_hashes[data] = concrete_hash
+            # This condition is essential to avoid some edge cases
+            condition = And(func(data) == concrete_hash, inverse(func(data)) == data)
+            return concrete_hash, condition
+
         condition = self._create_condition(func_input=data)
-        self.quick_inverse[func(data)] = data
         self.hash_result_store[length].append(func(data))
         return func(data), condition
 
@@ -132,7 +139,11 @@ class KeccakFunctionManager:
             ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)),
             URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0,
         )
-        return cond
+        concrete_cond = symbol_factory.Bool(False)
+        for key, keccak in self.concrete_hashes.items():
+            hash_eq = And(func(func_input) == keccak, key == func_input,)
+            concrete_cond = Or(concrete_cond, hash_eq)
+        return And(inv(func(func_input)) == func_input, Or(cond, concrete_cond))
 
 
 keccak_function_manager = KeccakFunctionManager()

mythril/laser/ethereum/strategy/extensions/bounded_loops.py

@@ -14,11 +14,13 @@ class JumpdestCountAnnotation(StateAnnotation):
     """State annotation that counts the number of jumps per destination."""
 
     def __init__(self) -> None:
-        self._reached_count = {}  # type: Dict[str, int]
+        self._reached_count = {}  # type: Dict[int, int]
+        self.trace = []  # type: List[int]
 
     def __copy__(self):
         result = JumpdestCountAnnotation()
         result._reached_count = copy(self._reached_count)
+        result.trace = copy(self.trace)
         return result
 
 
@@ -43,6 +45,39 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
             self, super_strategy.work_list, super_strategy.max_depth
         )
 
+    def calculate_hash(self, i, j, trace):
+        """
+        calculate hash(trace[i: j])
+        :param i:
+        :param j:
+        :param trace:
+        :return: hash(trace[i: j])
+        """
+        key = 0
+        size = 0
+        for itr in range(i, j):
+            key |= trace[itr] << ((itr - i) * 8)
+            size += 1
+
+        return key
+
+    def count_key(self, trace, key, start, size):
+        """
+        Count continuous loops in the trace.
+        :param trace:
+        :param key:
+        :param size:
+        :return:
+        """
+        count = 0
+        i = start
+        while i >= 0:
+            if self.calculate_hash(i, i + size, trace) != key:
+                break
+            count += 1
+            i -= size
+        return count
+
     def get_strategic_global_state(self) -> GlobalState:
         """ Returns the next state
 
@@ -66,34 +101,40 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
 
             cur_instr = state.get_current_instruction()
 
-            if (
-                cur_instr["opcode"].upper() != "JUMPDEST"
-                or state.environment.code.instruction_list[state.mstate.prev_pc][
-                    "opcode"
-                ]
-                != "JUMPI"
-            ):
+            annotation.trace.append(cur_instr["address"])
+
+            if cur_instr["opcode"].upper() != "JUMPDEST":
                 return state
 
             # create unique instruction identifier
-            key = "{};{};{}".format(
-                cur_instr["opcode"], cur_instr["address"], state.mstate.prev_pc
-            )
 
-            if key in annotation._reached_count:
-                annotation._reached_count[key] += 1
+            found = False
+            for i in range(len(annotation.trace) - 3, 0, -1):
+                if (
+                    annotation.trace[i] == annotation.trace[-2]
+                    and annotation.trace[i + 1] == annotation.trace[-1]
+                ):
+                    found = True
+                    break
+
+            if found:
+                key = self.calculate_hash(
+                    i, len(annotation.trace) - 1, annotation.trace
+                )
+                size = len(annotation.trace) - i - 1
+                count = self.count_key(annotation.trace, key, i, size)
             else:
-                annotation._reached_count[key] = 1
+                count = 0
 
             # The creation transaction gets a higher loop bound to give it a better chance of success.
             # TODO: There's probably a nicer way to do this
 
             if isinstance(
                 state.current_transaction, ContractCreationTransaction
-            ) and annotation._reached_count[key] < max(8, self.bound):
+            ) and count < max(8, self.bound):
                 return state
 
-            elif annotation._reached_count[key] > self.bound:
+            elif count > self.bound:
                 log.debug("Loop bound reached, skipping state")
                 continue
 

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,

requirements.txt

@@ -31,3 +31,4 @@ z3-solver>=4.8.5.0
 pysha3
 matplotlib
 pythx
+pre-commit

tests/instructions/create2_test.py

@@ -9,6 +9,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
     TransactionStartSignal,
 )
+from mythril.laser.smt import symbol_factory
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.support.support_utils import get_code_hash
 
@@ -20,7 +21,7 @@ def generate_salted_address(code_str, salt, caller):
     addr = hex(caller.value)[2:]
     addr = "0" * (40 - len(addr)) + addr
 
-    salt = hex(salt)[2:]
+    salt = hex(salt.value)[2:]
     salt = "0" * (64 - len(salt)) + salt
 
     contract_address = int(
@@ -46,9 +47,14 @@ def test_create2():
     og_state.transaction_stack.append(
         (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
     )
-    value = 3
-    salt = 10
-    og_state.mstate.stack = [salt, 6, 0, value]
+    value = symbol_factory.BitVecVal(3, 256)
+    salt = symbol_factory.BitVecVal(10, 256)
+    og_state.mstate.stack = [
+        salt,
+        symbol_factory.BitVecVal(6, 256),
+        symbol_factory.BitVecVal(0, 256),
+        value,
+    ]
     instruction = Instruction("create2", dynamic_loader=None)
 
     # Act + Assert

tests/laser/evm_testsuite/evm_test.py

@@ -177,15 +177,7 @@ def test_vmtest(
                 expected = int(value, 16)
                 actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)]
                 if isinstance(actual, Expression):
-                    if (
-                        actual.symbolic
-                        and actual in keccak_function_manager.quick_inverse
-                    ):
-                        actual = keccak_function_manager.find_concrete_keccak(
-                            keccak_function_manager.quick_inverse[actual]
-                        )
-                    else:
-                        actual = actual.value
+                    actual = actual.value
                     actual = 1 if actual is True else 0 if actual is False else actual
                 else:
                     if type(actual) == bytes: