Merge branch 'master' of github.com:ConsenSys/mythril into HEAD

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)

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
 

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

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

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

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,19 +78,30 @@ 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()
+                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)
         for code, coverage in self.coverage.items():
             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"

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)
+
+

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)
 

requirements.txt

@@ -1,3 +1,4 @@
+coloredlogs>=10.0
 configparser>=3.5.0
 coverage
 eth_abi>=1.0.0

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',

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