diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index ac03303f..c9431257 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -14,7 +14,7 @@ class SymExecWrapper: """ def __init__(self, contract, address, strategy, dynloader=None, max_depth=22, - execution_timeout=None, create_timeout=None): + execution_timeout=None, create_timeout=None, max_transaction_count=3): s_strategy = None if strategy == 'dfs': @@ -30,7 +30,8 @@ class SymExecWrapper: self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth, execution_timeout=execution_timeout, strategy=s_strategy, - create_timeout=create_timeout) + create_timeout=create_timeout, + max_transaction_count=max_transaction_count) if isinstance(contract, SolidityContract): self.laser.sym_exec(creation_code=contract.creation_code, contract_name=contract.name) diff --git a/mythril/leveldb/__init__.py b/mythril/ethereum/__init__.py similarity index 100% rename from mythril/leveldb/__init__.py rename to mythril/ethereum/__init__.py diff --git a/mythril/rpc/__init__.py b/mythril/ethereum/interface/__init__.py similarity index 100% rename from mythril/rpc/__init__.py rename to mythril/ethereum/interface/__init__.py diff --git a/mythril/ethereum/interface/leveldb/__init__.py b/mythril/ethereum/interface/leveldb/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/mythril/leveldb/accountindexing.py b/mythril/ethereum/interface/leveldb/accountindexing.py similarity index 100% rename from mythril/leveldb/accountindexing.py rename to mythril/ethereum/interface/leveldb/accountindexing.py diff --git a/mythril/leveldb/client.py b/mythril/ethereum/interface/leveldb/client.py similarity index 96% rename from mythril/leveldb/client.py rename to mythril/ethereum/interface/leveldb/client.py index 81c3f9e4..a1b4323b 100644 --- a/mythril/leveldb/client.py +++ b/mythril/ethereum/interface/leveldb/client.py @@ -1,12 +1,12 @@ import binascii import rlp -from mythril.leveldb.accountindexing import CountableList -from mythril.leveldb.accountindexing import ReceiptForStorage, AccountIndexer +from mythril.ethereum.interface.leveldb.accountindexing import CountableList +from mythril.ethereum.interface.leveldb.accountindexing import ReceiptForStorage, AccountIndexer import logging from ethereum import utils from ethereum.block import BlockHeader, Block -from mythril.leveldb.state import State -from mythril.leveldb.eth_db import ETH_DB +from mythril.ethereum.interface.leveldb.state import State +from mythril.ethereum.interface.leveldb.eth_db import ETH_DB from mythril.ether.ethcontract import ETHContract from mythril.exceptions import AddressNotFoundError diff --git a/mythril/leveldb/eth_db.py b/mythril/ethereum/interface/leveldb/eth_db.py similarity index 100% rename from mythril/leveldb/eth_db.py rename to mythril/ethereum/interface/leveldb/eth_db.py diff --git a/mythril/leveldb/state.py b/mythril/ethereum/interface/leveldb/state.py similarity index 100% rename from mythril/leveldb/state.py rename to mythril/ethereum/interface/leveldb/state.py diff --git a/mythril/ethereum/interface/rpc/__init__.py b/mythril/ethereum/interface/rpc/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/mythril/rpc/base_client.py b/mythril/ethereum/interface/rpc/base_client.py similarity index 100% rename from mythril/rpc/base_client.py rename to mythril/ethereum/interface/rpc/base_client.py diff --git a/mythril/rpc/client.py b/mythril/ethereum/interface/rpc/client.py similarity index 100% rename from mythril/rpc/client.py rename to mythril/ethereum/interface/rpc/client.py diff --git a/mythril/rpc/constants.py b/mythril/ethereum/interface/rpc/constants.py similarity index 100% rename from mythril/rpc/constants.py rename to mythril/ethereum/interface/rpc/constants.py diff --git a/mythril/rpc/exceptions.py b/mythril/ethereum/interface/rpc/exceptions.py similarity index 100% rename from mythril/rpc/exceptions.py rename to mythril/ethereum/interface/rpc/exceptions.py diff --git a/mythril/rpc/utils.py b/mythril/ethereum/interface/rpc/utils.py similarity index 100% rename from mythril/rpc/utils.py rename to mythril/ethereum/interface/rpc/utils.py diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index be6cec59..1784add4 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -5,7 +5,7 @@ http://www.github.com/ConsenSys/mythril """ -import logging +import logging, coloredlogs import json import sys import argparse @@ -69,6 +69,7 @@ def main(): options = parser.add_argument_group('options') options.add_argument('-m', '--modules', help='Comma-separated list of security analysis modules', metavar='MODULES') options.add_argument('--max-depth', type=int, default=22, help='Maximum recursion depth for symbolic execution') + options.add_argument('--max-transaction-count', type=int, default=3, help='Maximum number of transactions issued by laser') options.add_argument('--strategy', choices=['dfs', 'bfs'], default='dfs', help='Symbolic execution strategy') options.add_argument('--execution-timeout', type=int, default=600, help="The amount of seconds to spend on symbolic execution") options.add_argument('--create-timeout', type=int, default=10, help="The amount of seconds to spend on " @@ -103,7 +104,10 @@ def main(): if args.v: if 0 <= args.v < 3: - logging.basicConfig(level=[logging.NOTSET, logging.INFO, logging.DEBUG][args.v]) + coloredlogs.install( + fmt='%(name)s[%(process)d] %(levelname)s %(message)s', + level=[logging.NOTSET, logging.INFO, logging.DEBUG][args.v] + ) else: exit_with_error(args.outform, "Invalid -v value, you can find valid values in usage") @@ -215,7 +219,8 @@ def main(): modules=[m.strip() for m in args.modules.strip().split(",")] if args.modules else [], verbose_report=args.verbose_report, max_depth=args.max_depth, execution_timeout=args.execution_timeout, - create_timeout=args.create_timeout) + create_timeout=args.create_timeout, + max_transaction_count=args.max_transaction_count) outputs = { 'json': report.as_json(), 'text': report.as_text(), diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 31e6990e..fd5e24bb 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -49,7 +49,7 @@ def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symb try: callee_address = hex(util.get_concrete_int(symbolic_to_address)) except AttributeError: - logging.info("Symbolic call encountered") + logging.debug("Symbolic call encountered") match = re.search(r'storage_(\d+)', str(simplify(symbolic_to_address))) logging.debug("CALL to: " + str(simplify(symbolic_to_address))) @@ -58,7 +58,7 @@ def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symb raise ValueError() index = int(match.group(1)) - logging.info("Dynamic contract address at storage index {}".format(index)) + logging.debug("Dynamic contract address at storage index {}".format(index)) # attempt to read the contract address from instance storage try: @@ -89,22 +89,22 @@ def get_callee_account(global_state, callee_address, dynamic_loader): return global_state.accounts[callee_address] except KeyError: # We have a valid call address, but contract is not in the modules list - logging.info("Module with address " + callee_address + " not loaded.") + logging.debug("Module with address " + callee_address + " not loaded.") if dynamic_loader is None: raise ValueError() - logging.info("Attempting to load dependency") + logging.debug("Attempting to load dependency") try: code = dynamic_loader.dynld(environment.active_account.address, callee_address) except Exception as e: - logging.info("Unable to execute dynamic loader.") + logging.debug("Unable to execute dynamic loader.") raise ValueError() if code is None: - logging.info("No code returned, not a contract account?") + logging.debug("No code returned, not a contract account?") raise ValueError() - logging.info("Dependency loaded: " + callee_address) + logging.debug("Dependency loaded: " + callee_address) callee_account = Account(callee_address, code, callee_address, dynamic_loader=dynamic_loader) accounts[callee_address] = callee_account diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 57315bb3..d1abbf35 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1003,7 +1003,14 @@ class Instruction: @StateTransition() def revert_(self, global_state): - return [] + state = global_state.mstate + offset, length = state.stack.pop(), state.stack.pop() + return_data = [global_state.new_bitvec("return_data", 256)] + try: + return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] + except AttributeError: + logging.debug("Return with symbolic length or offset. Not supported") + global_state.current_transaction.end(global_state, return_data=return_data, revert=True) @StateTransition() def assert_fail_(self, global_state): @@ -1028,7 +1035,7 @@ class Instruction: callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader, True) except ValueError as e: - logging.info( + logging.debug( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) # TODO: decide what to do in this case diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index cdf85484..f1bd80b5 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -28,7 +28,7 @@ class LaserEVM: """ def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, create_timeout=10, - strategy=DepthFirstSearchStrategy): + strategy=DepthFirstSearchStrategy, max_transaction_count=3): world_state = WorldState() world_state.accounts = accounts # this sets the initial world state @@ -45,6 +45,7 @@ class LaserEVM: self.work_list = [] self.strategy = strategy(self.work_list, max_depth) self.max_depth = max_depth + self.max_transaction_count = max_transaction_count self.execution_timeout = execution_timeout self.create_timeout = create_timeout @@ -77,12 +78,16 @@ class LaserEVM: # Reset code coverage self.coverage = {} - self.time = datetime.now() - logging.info("Starting message call transaction") - execute_message_call(self, created_account.address) + for i in range(self.max_transaction_count): + initial_coverage = self._get_covered_instructions() - self.time = datetime.now() - execute_message_call(self, created_account.address) + self.time = datetime.now() + logging.info("Starting message call transaction, iteration: {}".format(i)) + execute_message_call(self, created_account.address) + + end_coverage = self._get_covered_instructions() + if end_coverage == initial_coverage: + break logging.info("Finished symbolic execution") logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states) @@ -90,6 +95,13 @@ class LaserEVM: cov = reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1]) / float(coverage[0]) * 100 logging.info("Achieved {} coverage for code: {}".format(cov, code)) + def _get_covered_instructions(self) -> int: + """ Gets the total number of covered instructions for all accounts in the svm""" + total_covered_instructions = 0 + for _, cv in self.coverage.items(): + total_covered_instructions += reduce(lambda sum_, val: sum_ + 1 if val else sum_, cv[1]) + return total_covered_instructions + def exec(self, create=False): for global_state in self.strategy: if self.execution_timeout and not create: @@ -138,30 +150,31 @@ class LaserEVM: new_global_states = self._end_message_call(return_global_state, global_state, revert_changes=True, return_data=None) - except TransactionStartSignal as e: + except TransactionStartSignal as start_signal: # Setup new global state - new_global_state = e.transaction.initial_global_state() + new_global_state = start_signal.transaction.initial_global_state() - new_global_state.transaction_stack = copy(global_state.transaction_stack) + [(e.transaction, global_state)] + new_global_state.transaction_stack = copy(global_state.transaction_stack) + [(start_signal.transaction, global_state)] new_global_state.node = global_state.node new_global_state.mstate.constraints = global_state.mstate.constraints return [new_global_state], op_code - except TransactionEndSignal as e: - transaction, return_global_state = e.global_state.transaction_stack.pop() + except TransactionEndSignal as end_signal: + transaction, return_global_state = end_signal.global_state.transaction_stack.pop() if return_global_state is None: - if not isinstance(transaction, ContractCreationTransaction) or transaction.return_data: - e.global_state.world_state.node = global_state.node - self.open_states.append(e.global_state.world_state) + if (not isinstance(transaction, ContractCreationTransaction) or transaction.return_data) and not end_signal.revert: + end_signal.global_state.world_state.node = global_state.node + self.open_states.append(end_signal.global_state.world_state) new_global_states = [] else: # First execute the post hook for the transaction ending instruction - self._execute_post_hook(op_code, [e.global_state]) + self._execute_post_hook(op_code, [end_signal.global_state]) new_global_states = self._end_message_call(return_global_state, global_state, - revert_changes=False, return_data=transaction.return_data) + revert_changes=False or end_signal.revert, + return_data=transaction.return_data) self._execute_post_hook(op_code, new_global_states) @@ -252,7 +265,7 @@ class LaserEVM: environment.active_function_name = disassembly.addr_to_func[address] new_node.flags |= NodeFlags.FUNC_ENTRY - logging.info( + logging.debug( "- Entering function " + environment.active_account.contract_name + ":" + new_node.function_name) elif address == 0: environment.active_function_name = "fallback" diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index fa60599d..35826bcd 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -12,10 +12,12 @@ def get_next_transaction_id(): _next_transaction_id += 1 return _next_transaction_id + class TransactionEndSignal(Exception): """ Exception raised when a transaction is finalized""" - def __init__(self, global_state): + def __init__(self, global_state, revert=False): self.global_state = global_state + self.revert = revert class TransactionStartSignal(Exception): @@ -70,9 +72,9 @@ class MessageCallTransaction: return global_state - def end(self, global_state, return_data=None): + def end(self, global_state, return_data=None, revert=False): self.return_data = return_data - raise TransactionEndSignal(global_state) + raise TransactionEndSignal(global_state, revert) class ContractCreationTransaction: @@ -125,7 +127,7 @@ class ContractCreationTransaction: return global_state - def end(self, global_state, return_data=None): + def end(self, global_state, return_data=None, revert=False): if not all([isinstance(element, int) for element in return_data]): self.return_data = None @@ -136,4 +138,6 @@ class ContractCreationTransaction: global_state.environment.active_account.code = Disassembly(contract_code) self.return_data = global_state.environment.active_account.address - raise TransactionEndSignal(global_state) + raise TransactionEndSignal(global_state, revert=revert) + + diff --git a/mythril/mythril.py b/mythril/mythril.py index 9cdeb0fd..123ab904 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -20,8 +20,8 @@ import platform from mythril.ether import util from mythril.ether.ethcontract import ETHContract from mythril.ether.soliditycontract import SolidityContract, get_contracts_from_file -from mythril.rpc.client import EthJsonRpc -from mythril.rpc.exceptions import ConnectionError +from mythril.ethereum.interface.rpc.client import EthJsonRpc +from mythril.ethereum.interface.rpc.exceptions import ConnectionError from mythril.support import signatures from mythril.support.truffle import analyze_truffle_project from mythril.support.loader import DynLoader @@ -31,7 +31,7 @@ from mythril.analysis.callgraph import generate_graph from mythril.analysis.traceexplore import get_serializable_statespace from mythril.analysis.security import fire_lasers from mythril.analysis.report import Report -from mythril.leveldb.client import EthLevelDB +from mythril.ethereum.interface.leveldb.client import EthLevelDB # logging.basicConfig(level=logging.DEBUG) @@ -360,14 +360,16 @@ class Mythril(object): return generate_graph(sym, physics=enable_physics, phrackify=phrackify) def fire_lasers(self, strategy, contracts=None, address=None, - modules=None, verbose_report=False, max_depth=None, execution_timeout=None, create_timeout=None): + modules=None, verbose_report=False, max_depth=None, execution_timeout=None, create_timeout=None, + max_transaction_count=None): all_issues = [] for contract in (contracts or self.contracts): sym = SymExecWrapper(contract, address, strategy, dynloader=DynLoader(self.eth) if self.dynld else None, max_depth=max_depth, execution_timeout=execution_timeout, - create_timeout=create_timeout) + create_timeout=create_timeout, + max_transaction_count=max_transaction_count) issues = fire_lasers(sym, modules) diff --git a/requirements.txt b/requirements.txt index 53a4a086..30162f8d 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,3 +1,4 @@ +coloredlogs>=10.0 configparser>=3.5.0 coverage eth_abi>=1.0.0 diff --git a/setup.py b/setup.py index cfb6cb7b..2c92ce4a 100755 --- a/setup.py +++ b/setup.py @@ -82,6 +82,7 @@ setup( packages=find_packages(exclude=['contrib', 'docs', 'tests']), install_requires=[ + 'coloredlogs>=10.0', 'ethereum>=2.3.2', 'z3-solver>=4.5', 'requests', diff --git a/tests/rpc_test.py b/tests/rpc_test.py index 89621b64..564c7da8 100644 --- a/tests/rpc_test.py +++ b/tests/rpc_test.py @@ -1,6 +1,6 @@ from unittest import TestCase -from mythril.rpc.client import EthJsonRpc +from mythril.ethereum.interface.rpc.client import EthJsonRpc class RpcTest(TestCase): client = None