From cb07c584d4323423fe424062702008172229cfb6 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 23 Jan 2019 16:24:38 +0530 Subject: [PATCH 01/10] Remove unused imports in mythril.py --- mythril/mythril.py | 7 ------- 1 file changed, 7 deletions(-) diff --git a/mythril/mythril.py b/mythril/mythril.py index 824d4445..5c08ab8a 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -19,17 +19,10 @@ import solc from ethereum import utils from solc.exceptions import SolcError -from mythril.analysis.callgraph import generate_graph -from mythril.analysis.report import Report -from mythril.analysis.security import fire_lasers -from mythril.analysis.symbolic import SymExecWrapper -from mythril.analysis.traceexplore import get_serializable_statespace from mythril.ethereum import util from mythril.ethereum.evmcontract import EVMContract -from mythril.ethereum.interface.leveldb.client import EthLevelDB from mythril.ethereum.interface.rpc.client import EthJsonRpc from mythril.ethereum.interface.rpc.exceptions import ConnectionError -from mythril.exceptions import CompilerError, CriticalError, NoContractFoundError from mythril.solidity.soliditycontract import SolidityContract, get_contracts_from_file from mythril.support import signatures from mythril.support.source_support import Source From 1a0e65f4e43d2a5090c961f3e5fef6432cfaed4a Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 23 Jan 2019 16:25:01 +0530 Subject: [PATCH 02/10] Use the recent definitions of Memory() and Storage() --- mythril/analysis/traceexplore.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/traceexplore.py b/mythril/analysis/traceexplore.py index ce06f0e9..f88d6410 100644 --- a/mythril/analysis/traceexplore.py +++ b/mythril/analysis/traceexplore.py @@ -97,7 +97,7 @@ def get_serializable_statespace(statespace): account["balance"] = str(account["balance"]) storage = {} - for storage_key in account["storage"]: + for storage_key in account["storage"].keys(): storage[str(storage_key)] = str(account["storage"][storage_key]) state_accounts.append({"address": key, "storage": storage}) @@ -110,7 +110,10 @@ def get_serializable_statespace(statespace): for state in states: state["machine"]["stack"] = [str(s) for s in state["machine"]["stack"]] - state["machine"]["memory"] = [str(m) for m in state["machine"]["memory"]] + state["machine"]["memory"] = [ + str(m) + for m in state["machine"]["memory"][: len(state["machine"]["memory"])] + ] truncated_code = truncated_code.replace("\\n", "\n") code = code.replace("\\n", "\n") From c6b41223d82d0f0fbc9b561053c94b588240ce98 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 25 Jan 2019 18:00:59 +0530 Subject: [PATCH 03/10] Assert timeout to > 0 --- mythril/analysis/solver.py | 7 +++++-- .../laser/ethereum/plugins/mutation_pruner.py | 2 +- mythril/laser/ethereum/svm.py | 2 ++ mythril/laser/ethereum/time_handler.py | 17 +++++++++++++++++ mythril/laser/smt/bool.py | 1 + mythril/laser/smt/solver.py | 1 + 6 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 mythril/laser/ethereum/time_handler.py diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index eed24065..14d46c0b 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -3,6 +3,7 @@ from z3 import sat, unknown, FuncInterp import z3 from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory +from mythril.laser.ethereum.time_handler import time_handler from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, @@ -21,8 +22,10 @@ def get_model(constraints, minimize=(), maximize=()): :return: """ s = Optimize() - s.set_timeout(100000) - + timeout = min(100000, time_handler.time_remaining()-500) + if timeout < 0: + raise UnsatError + s.set_timeout(timeout) for constraint in constraints: if type(constraint) == bool and not constraint: raise UnsatError diff --git a/mythril/laser/ethereum/plugins/mutation_pruner.py b/mythril/laser/ethereum/plugins/mutation_pruner.py index 38ad1410..f777a85b 100644 --- a/mythril/laser/ethereum/plugins/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/mutation_pruner.py @@ -5,7 +5,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) -from mythril.laser.smt import And, symbol_factory +from mythril.laser.smt import And, symbol_factory, Bool class MutationAnnotation(StateAnnotation): diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 98ac87e6..3b74cc12 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -16,6 +16,7 @@ from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy +from mythril.laser.ethereum.time_handler import time_handler from mythril.laser.ethereum.plugins.signals import PluginSignal, PluginSkipWorldState from mythril.laser.ethereum.transaction import ( ContractCreationTransaction, @@ -121,6 +122,7 @@ class LaserEVM: log.debug("Starting LASER execution") try: + time_handler.start_execution(self.execution_timeout) alarm.start_timeout(self.execution_timeout) self.time = datetime.now() diff --git a/mythril/laser/ethereum/time_handler.py b/mythril/laser/ethereum/time_handler.py new file mode 100644 index 00000000..5b7f93e9 --- /dev/null +++ b/mythril/laser/ethereum/time_handler.py @@ -0,0 +1,17 @@ +import time + + +class TimeHandler: + def __init__(self): + self._start_time = None + self._execution_time = None + + def start_execution(self, execution_time): + self._start_time = int(time.time() * 1000) + self._execution_time = execution_time * 1000 + + def time_remaining(self): + return self._execution_time - (int(time.time() * 1000) - self._start_time) + + +time_handler = TimeHandler() diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py index fcf4a03f..c82e4f1f 100644 --- a/mythril/laser/smt/bool.py +++ b/mythril/laser/smt/bool.py @@ -84,6 +84,7 @@ class Bool(Expression[z3.BoolRef]): def And(*args: Bool) -> Bool: """Create an And expression.""" union = [] + args = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args] for arg in args: union.append(arg.annotations) return Bool(z3.And([a.raw for a in args]), union) diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index 1bc02543..c287d60c 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -20,6 +20,7 @@ class BaseSolver(Generic[T]): :param timeout: """ + assert timeout > 0 # timeout <= 0 isn't supported by z3 self.raw.set(timeout=timeout) def add(self, constraints: Union[Bool, List[Bool]]) -> None: From 7778e5fd0c5f75aba2dd6f7b796f479b53f31b18 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 25 Jan 2019 18:10:31 +0530 Subject: [PATCH 04/10] Add timer class and take min of that and solver timeout --- mythril/analysis/solver.py | 2 +- mythril/laser/smt/solver.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 14d46c0b..2a29f710 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -22,7 +22,7 @@ def get_model(constraints, minimize=(), maximize=()): :return: """ s = Optimize() - timeout = min(100000, time_handler.time_remaining()-500) + timeout = min(100000, time_handler.time_remaining() - 500) if timeout < 0: raise UnsatError s.set_timeout(timeout) diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index c287d60c..21c18195 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -20,7 +20,7 @@ class BaseSolver(Generic[T]): :param timeout: """ - assert timeout > 0 # timeout <= 0 isn't supported by z3 + assert timeout > 0 # timeout <= 0 isn't supported by z3 self.raw.set(timeout=timeout) def add(self, constraints: Union[Bool, List[Bool]]) -> None: From 5e7009700a6be7e3b5e72a24d18214026df66c3c Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 25 Jan 2019 18:12:12 +0530 Subject: [PATCH 05/10] Remove unused imports --- mythril/laser/ethereum/plugins/mutation_pruner.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/plugins/mutation_pruner.py b/mythril/laser/ethereum/plugins/mutation_pruner.py index f777a85b..38ad1410 100644 --- a/mythril/laser/ethereum/plugins/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/mutation_pruner.py @@ -5,7 +5,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) -from mythril.laser.smt import And, symbol_factory, Bool +from mythril.laser.smt import And, symbol_factory class MutationAnnotation(StateAnnotation): From 6322b4d3c71ca23d78f1ea0a32a304446f4475a6 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 25 Jan 2019 18:19:56 +0530 Subject: [PATCH 06/10] Fix the timelimit of calls.sol execution --- tests/laser/transaction/create_transaction_test.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/laser/transaction/create_transaction_test.py b/tests/laser/transaction/create_transaction_test.py index 9b2351e4..10a1f837 100644 --- a/tests/laser/transaction/create_transaction_test.py +++ b/tests/laser/transaction/create_transaction_test.py @@ -41,7 +41,10 @@ def test_sym_exec(): ) sym = SymExecWrapper( - contract, address=(util.get_indexed_address(0)), strategy="dfs" + contract, + address=(util.get_indexed_address(0)), + strategy="dfs", + execution_timeout=10, ) issues = fire_lasers(sym) From 1e296a7a1f680524c09596f3b917075786ae9014 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 25 Jan 2019 22:58:01 +0530 Subject: [PATCH 07/10] Move from z3 4.8.0.0 to 4.8.4 --- requirements.txt | 2 +- setup.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/requirements.txt b/requirements.txt index 815a2771..2189f7cc 100644 --- a/requirements.txt +++ b/requirements.txt @@ -25,5 +25,5 @@ pytest_mock requests rlp>=1.0.1 transaction>=2.2.1 -z3-solver>=4.8.0.0 +z3-solver-mythril>=4.8.4.1 pysha3 diff --git a/setup.py b/setup.py index ad60e07c..82a6fbed 100755 --- a/setup.py +++ b/setup.py @@ -75,7 +75,7 @@ setup( "coloredlogs>=10.0", "py_ecc==1.4.2", "ethereum>=2.3.2", - "z3-solver>=4.8.0.0", + "z3-solver-mythril>=4.8.4.1", "requests", "py-solc", "plyvel", From 9bee3c716c9726f5ce0ab1d1f3c3f0f09b7f65e2 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 29 Jan 2019 15:13:22 +0530 Subject: [PATCH 08/10] Make timehandler class Singleton --- mythril/laser/ethereum/time_handler.py | 3 ++- mythril/support/support_utils.py | 20 ++++++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/time_handler.py b/mythril/laser/ethereum/time_handler.py index 5b7f93e9..b8e1379b 100644 --- a/mythril/laser/ethereum/time_handler.py +++ b/mythril/laser/ethereum/time_handler.py @@ -1,7 +1,8 @@ import time +from mythril.support.support_utils import Singleton -class TimeHandler: +class TimeHandler(object, metaclass=Singleton): def __init__(self): self._start_time = None self._execution_time = None diff --git a/mythril/support/support_utils.py b/mythril/support/support_utils.py index 1d8c1013..9fe90a8f 100644 --- a/mythril/support/support_utils.py +++ b/mythril/support/support_utils.py @@ -1 +1,21 @@ """This module contains utility functions for the Mythril support package.""" + + +class Singleton(type): + """A metaclass type implementing the singleton pattern.""" + + _instances = {} + + def __call__(cls, *args, **kwargs): + """Delegate the call to an existing resource or a a new one. + + This is not thread- or process-safe by default. It must be protected with + a lock. + + :param args: + :param kwargs: + :return: + """ + if cls not in cls._instances: + cls._instances[cls] = super(Singleton, cls).__call__(*args, **kwargs) + return cls._instances[cls] From d594d08286210d74c12332a92b6be252af800fd5 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 29 Jan 2019 18:57:51 +0530 Subject: [PATCH 09/10] Remove alarm --- mythril/alarm.py | 25 ------------------ mythril/exceptions.py | 4 --- mythril/laser/ethereum/svm.py | 49 ++++++++++++++--------------------- 3 files changed, 20 insertions(+), 58 deletions(-) delete mode 100644 mythril/alarm.py diff --git a/mythril/alarm.py b/mythril/alarm.py deleted file mode 100644 index 4c546bf4..00000000 --- a/mythril/alarm.py +++ /dev/null @@ -1,25 +0,0 @@ -import signal -from types import FrameType -from mythril.exceptions import OutOfTimeError - - -def sigalrm_handler(signum: int, frame: FrameType) -> None: - raise OutOfTimeError - - -def start_timeout(timeout: int) -> None: - """ - Starts a timeout - :param timeout: Time in seconds to set the timeout for - :return: None - """ - signal.signal(signal.SIGALRM, sigalrm_handler) - signal.alarm(timeout) - - -def disable_timeout() -> None: - """ - Ensures that the timeout is disabled - :return: None - """ - signal.alarm(0) diff --git a/mythril/exceptions.py b/mythril/exceptions.py index 49a6ad3c..7988759b 100644 --- a/mythril/exceptions.py +++ b/mythril/exceptions.py @@ -7,10 +7,6 @@ class MythrilBaseException(Exception): pass -class OutOfTimeError(MythrilBaseException): - pass - - class CompilerError(MythrilBaseException): """A Mythril exception denoting an error during code compilation.""" diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 3b74cc12..7b2a39d8 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -6,8 +6,6 @@ from datetime import datetime, timedelta from functools import reduce from typing import Callable, Dict, List, Tuple, Union -from mythril import alarm -from mythril.exceptions import OutOfTimeError from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException @@ -121,37 +119,30 @@ class LaserEVM: """ log.debug("Starting LASER execution") - try: - time_handler.start_execution(self.execution_timeout) - alarm.start_timeout(self.execution_timeout) - self.time = datetime.now() + time_handler.start_execution(self.execution_timeout) + self.time = datetime.now() - if main_address: - log.info("Starting message call transaction to {}".format(main_address)) - self._execute_transactions(main_address) + if main_address: + log.info("Starting message call transaction to {}".format(main_address)) + self._execute_transactions(main_address) - elif creation_code: - log.info("Starting contract creation transaction") - created_account = execute_contract_creation( - self, creation_code, contract_name + elif creation_code: + log.info("Starting contract creation transaction") + created_account = execute_contract_creation( + self, creation_code, contract_name + ) + log.info( + "Finished contract creation, found {} open states".format( + len(self.open_states) ) - log.info( - "Finished contract creation, found {} open states".format( - len(self.open_states) - ) + ) + if len(self.open_states) == 0: + log.warning( + "No contract was created during the execution of contract creation " + "Increase the resources for creation execution (--max-depth or --create-timeout)" ) - if len(self.open_states) == 0: - log.warning( - "No contract was created during the execution of contract creation " - "Increase the resources for creation execution (--max-depth or --create-timeout)" - ) - - self._execute_transactions(created_account.address) - - except OutOfTimeError: - log.warning("Timeout occurred, ending symbolic execution") - finally: - alarm.disable_timeout() + + self._execute_transactions(created_account.address) log.info("Finished symbolic execution") if self.requires_statespace: From 8e4a70f093e46ff9bad475334fda9114cffbc2b5 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 29 Jan 2019 15:40:08 +0100 Subject: [PATCH 10/10] comparison should check for <= instead of < --- mythril/analysis/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 2a29f710..2eb057f6 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -23,7 +23,7 @@ def get_model(constraints, minimize=(), maximize=()): """ s = Optimize() timeout = min(100000, time_handler.time_remaining() - 500) - if timeout < 0: + if timeout <= 0: raise UnsatError s.set_timeout(timeout) for constraint in constraints: