diff --git a/.circleci/config.yml b/.circleci/config.yml index 13e9d790..0a295470 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -57,6 +57,10 @@ jobs: command: python3 setup.py install working_directory: /home/mythril + - run: + name: Sonar analysis + command: if [ -z "CIRCLE_PR_NUMBER" ]; then sonar-scanner -Dsonar.projectKey=$SONAR_PROJECT_KEY -Dsonar.organization=$SONAR_ORGANIZATION -Dsonar.sources=/home/mythril -Dsonar.host.url=$SONAR_HOST_URL -Dsonar.login=$(SONAR_LOGIN); fi + - run: name: Integration tests command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py index d6bf850c..b7a4dce0 100644 --- a/mythril/analysis/modules/ether_send.py +++ b/mythril/analysis/modules/ether_send.py @@ -27,15 +27,14 @@ def execute(statespace): state = call.state address = state.get_current_instruction()['address'] - if ("callvalue" in str(call.value)): + if "callvalue" in str(call.value): logging.debug("[ETHER_SEND] Skipping refund function") continue # We're only interested in calls that send Ether - if call.value.type == VarType.CONCRETE: - if call.value.val == 0: - continue + if call.value.type == VarType.CONCRETE and call.value.val == 0: + continue interesting = False @@ -52,14 +51,14 @@ def execute(statespace): else: m = re.search(r'storage_([a-z0-9_&^]+)', str(call.to)) - if (m): + if m: idx = m.group(1) description += "a non-zero amount of Ether is sent to an address taken from storage slot " + str(idx) + ".\n" func = statespace.find_storage_write(state.environment.active_account.address, idx) - if (func): + if func: description += "There is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function `" + func + "`.\n" interesting = True else: @@ -74,7 +73,7 @@ def execute(statespace): index = 0 - while(can_solve and index < len(node.constraints)): + while can_solve and index < len(node.constraints): constraint = node.constraints[index] index += 1 @@ -82,14 +81,14 @@ def execute(statespace): m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) - if (m): + if m: constrained = True idx = m.group(1) func = statespace.find_storage_write(state.environment.active_account.address, idx) - if (func): + if func: description += "\nThere is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function `" + func + "`." else: logging.debug("[ETHER_SEND] No storage writes to index " + str(idx)) @@ -98,7 +97,7 @@ def execute(statespace): # CALLER may also be constrained to hardcoded address. I.e. 'caller' and some integer - elif (re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint))): + elif re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint)): constrained = True can_solve = False break @@ -116,7 +115,8 @@ def execute(statespace): debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model) - issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning", description, debug) + issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning", + description, debug) issues.append(issue) except UnsatError: diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 507bbd49..fc287948 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -24,9 +24,7 @@ def execute(statespace): for state in node.states: instruction = state.get_current_instruction() - if(instruction['opcode'] == "ASSERT_FAIL"): - try: model = solver.get_model(node.constraints) address = state.get_current_instruction()['address'] diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index e21dbb58..f89c0781 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -108,7 +108,6 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o return _try_constraints(node.constraints, [Not(constraint)]) is not None - def _try_constraints(constraints, new_constraints): """ Tries new constraints diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 0f6703e6..9c5a2dd0 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -4,7 +4,7 @@ import logging def get_model(constraints): s = Solver() - s.set("timeout", 10000) + s.set("timeout", 100000) for constraint in constraints: s.add(constraint) diff --git a/mythril/disassembler/disassembly.py b/mythril/disassembler/disassembly.py index a20d4ffe..2f7aec4c 100644 --- a/mythril/disassembler/disassembly.py +++ b/mythril/disassembler/disassembly.py @@ -1,4 +1,4 @@ -from mythril.ether import asm,util +from mythril.ether import asm, util from mythril.support.signatures import SignatureDb import logging @@ -7,7 +7,7 @@ class Disassembly(object): def __init__(self, code): self.instruction_list = asm.disassemble(util.safe_decode(code)) - self.xrefs = [] + self.func_hashes = [] self.func_to_addr = {} self.addr_to_func = {} self.bytecode = code @@ -24,6 +24,7 @@ class Disassembly(object): for i in jmptable_indices: func_hash = self.instruction_list[i]['argument'] + self.func_hashes.append(func_hash) try: # tries local cache, file and optional online lookup # may return more than one function signature. since we cannot probe for the correct one we'll use the first @@ -38,7 +39,7 @@ class Disassembly(object): func_name = "_function_" + func_hash try: - offset = self.instruction_list[i+2]['argument'] + offset = self.instruction_list[i + 2]['argument'] jump_target = int(offset, 16) self.func_to_addr[func_name] = jump_target diff --git a/mythril/ether/ethcontract.py b/mythril/ether/ethcontract.py index 197376b0..8e19c746 100644 --- a/mythril/ether/ethcontract.py +++ b/mythril/ether/ethcontract.py @@ -31,12 +31,12 @@ class ETHContract(persistent.Persistent): def get_easm(self): - return Disassembly(self.code).get_easm() + return self.disassembly.get_easm() def matches_expression(self, expression): - easm_code = self.get_easm() str_eval = '' + easm_code = None matches = re.findall(r'func#([a-zA-Z0-9\s_,(\\)\[\]]+)#', expression) @@ -58,6 +58,9 @@ class ETHContract(persistent.Persistent): m = re.match(r'^code#([a-zA-Z0-9\s,\[\]]+)#', token) if (m): + if easm_code is None: + easm_code = self.get_easm() + code = m.group(1).replace(",", "\\n") str_eval += "\"" + code + "\" in easm_code" continue @@ -65,21 +68,8 @@ class ETHContract(persistent.Persistent): m = re.match(r'^func#([a-fA-F0-9]+)#$', token) if (m): - str_eval += "\"" + m.group(1) + "\" in easm_code" + str_eval += "\"" + m.group(1) + "\" in self.disassembly.func_hashes" continue return eval(str_eval.strip()) - - -class InstanceList(persistent.Persistent): - - def __init__(self): - self.addresses = [] - self.balances = [] - pass - - def add(self, address, balance=0): - self.addresses.append(address) - self.balances.append(balance) - self._p_changed = True diff --git a/mythril/laser/ethereum/cfg.py b/mythril/laser/ethereum/cfg.py index f462f5cf..a8a4fe82 100644 --- a/mythril/laser/ethereum/cfg.py +++ b/mythril/laser/ethereum/cfg.py @@ -8,6 +8,7 @@ class JumpType(Enum): UNCONDITIONAL = 2 CALL = 3 RETURN = 4 + Transaction = 5 class NodeFlags(Flags): diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 2db3adf7..ae7ef8fe 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -707,13 +707,8 @@ class Instruction: index = str(index) try: - # Create a fresh copy of the account object before modifying storage - - for k in global_state.accounts: - if global_state.accounts[k] == global_state.environment.active_account: - global_state.accounts[k] = deepcopy(global_state.accounts[k]) - global_state.environment.active_account = global_state.accounts[k] - break + global_state.environment.active_account = deepcopy(global_state.environment.active_account) + global_state.accounts[global_state.environment.active_account.address] = global_state.environment.active_account global_state.environment.active_account.storage[index] = value except KeyError: @@ -778,7 +773,7 @@ class Instruction: new_state = copy(global_state) new_state.mstate.pc = index new_state.mstate.depth += 1 - new_state.mstate.constraints.append(condi) + new_state.mstate.constraints.append(simplify(condi)) states.append(new_state) else: @@ -786,12 +781,11 @@ class Instruction: # False case negated = Not(condition) if type(condition) == BoolRef else condition == 0 - sat = not is_false(simplify(negated)) if type(condi) == BoolRef else not negated - if sat: + if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(simplify(negated))): new_state = copy(global_state) new_state.mstate.depth += 1 - new_state.mstate.constraints.append(negated) + new_state.mstate.constraints.append(simplify(negated)) states.append(new_state) else: logging.debug("Pruned unreachable states.") diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 206bd084..032cf66e 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -1,12 +1,13 @@ from z3 import BitVec, BitVecVal from copy import copy, deepcopy from enum import Enum - +from random import random class CalldataType(Enum): CONCRETE = 1 SYMBOLIC = 2 + class Account: """ Account class representing ethereum accounts @@ -31,8 +32,20 @@ class Account: def __str__(self): return str(self.as_dict) - def get_storage(self, index): - return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256) + def set_balance(self, balance): + self.balance = balance + + def add_balance(self, balance): + self.balance += balance + + # def get_storage(self, index): + # return BitVec("storage_" + str(index), 256) + # if index in self.storage.keys(): + # return self.storage[index] + # else: + # symbol = BitVec("storage_" + str(index), 256) + # self.storage[index] = symbol + # return symbol @property def as_dict(self): @@ -71,6 +84,7 @@ class Environment: def __str__(self): return str(self.as_dict) + @property def as_dict(self): return dict(active_account=self.active_account, sender=self.sender, calldata=self.calldata, @@ -138,7 +152,7 @@ class GlobalState: def __copy__(self): - accounts = self.accounts + accounts = copy(self.accounts) environment = copy(self.environment) mstate = deepcopy(self.mstate) call_stack = copy(self.call_stack) @@ -149,3 +163,55 @@ class GlobalState: """ Gets the current instruction for this GlobalState""" instructions = self.environment.code.instruction_list return instructions[self.mstate.pc] + + +class WorldState: + """ + The WorldState class represents the world state as described in the yellow paper + """ + def __init__(self): + """ + Constructor for the world state. Initializes the accounts record + """ + self.accounts = {} + self.node = None + + def __getitem__(self, item): + """ + Gets an account from the worldstate using item as key + :param item: Address of the account to get + :return: Account associated with the address + """ + return self.accounts[item] + + def create_account(self, balance=0): + """ + Create non-contract account + :param balance: Initial balance for the account + :return: The new account + """ + new_account = Account(self._generate_new_address(), balance=balance) + self._put_account(new_account) + return new_account + + def create_initialized_contract_account(self, contract_code, storage): + """ + Creates a new contract account, based on the contract code and storage provided + The contract code only includes the runtime contract bytecode + :param contract_code: Runtime bytecode for the contract + :param storage: Initial storage for the contract + :return: The new account + """ + new_account = Account(self._generate_new_address(), code=contract_code, balance=0) + new_account.storage = storage + self._put_account(new_account) + + def _generate_new_address(self): + """ Generates a new address for the global state""" + while True: + address = '0x' + ''.join([str(hex(random(0, 16)))[-1] for _ in range(20)]) + if address not in self.accounts.keys(): + return address + + def _put_account(self, account): + self.accounts[account.address] = account diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index ad1d5e2f..61899681 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -1,6 +1,7 @@ from z3 import BitVec import logging -from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account +from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState +from mythril.laser.ethereum.transaction import MessageCall from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy @@ -28,7 +29,12 @@ class LaserEVM: def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, strategy=DepthFirstSearchStrategy): self.instructions_covered = [] - self.accounts = accounts + + world_state = WorldState() + world_state.accounts = accounts + # this sets the initial world state + self.world_state = world_state + self.open_states = [world_state] self.nodes = {} self.edges = [] @@ -51,35 +57,12 @@ class LaserEVM: logging.debug("Starting LASER execution") self.time = datetime.now() - # Initialize the execution environment - environment = Environment( - self.accounts[main_address], - BitVec("caller", 256), - [], - BitVec("gasprice", 256), - BitVec("callvalue", 256), - BitVec("origin", 256), - calldata_type=CalldataType.SYMBOLIC, - ) - - self.instructions_covered = [False for _ in environment.code.instruction_list] - - initial_node = Node(environment.active_account.contract_name) - self.nodes[initial_node.uid] = initial_node - - global_state = GlobalState(self.accounts, environment, initial_node) - global_state.environment.active_function_name = "fallback()" - initial_node.states.append(global_state) + transaction = MessageCall(main_address) + transaction.run(self.open_states, self) - # Empty the work_list before starting an execution - self.work_list.append(global_state) - self._sym_exec() - - logging.info("Execution complete") - logging.info("Achieved {0:.3g}% coverage".format(self.coverage)) logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states) - def _sym_exec(self): + def exec(self): for global_state in self.strategy: if self.execution_timeout: if self.time + timedelta(seconds=self.execution_timeout) <= datetime.now(): @@ -87,9 +70,16 @@ class LaserEVM: try: new_states, op_code = self.execute_state(global_state) except NotImplementedError: - logging.debug("Encountered unimplemented instruction") + logging.info("Encountered unimplemented instruction: {}".format(op_code)) continue + if len(new_states) == 0: + # TODO: let global state use worldstate + open_world_state = WorldState() + open_world_state.accounts = global_state.accounts + open_world_state.node = global_state.node + self.open_states.append(open_world_state) + self.manage_cfg(op_code, new_states) self.work_list += new_states @@ -147,7 +137,7 @@ class LaserEVM: except IndexError: new_node.flags |= NodeFlags.FUNC_ENTRY address = state.environment.code.instruction_list[state.mstate.pc - 1]['address'] - + environment = state.environment disassembly = environment.code if address in state.environment.code.addr_to_func: diff --git a/mythril/laser/ethereum/taint_analysis.py b/mythril/laser/ethereum/taint_analysis.py index 37f546a0..441d9e23 100644 --- a/mythril/laser/ethereum/taint_analysis.py +++ b/mythril/laser/ethereum/taint_analysis.py @@ -118,7 +118,7 @@ class TaintRunner: direct_children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid] children = [] for child in direct_children: - if child.states[0].environment.active_account == environment.active_account: + if child.states[0].environment.active_account.address == environment.active_account.address: children.append(child) else: children += TaintRunner.children(child, statespace, environment) diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py new file mode 100644 index 00000000..a1416b5e --- /dev/null +++ b/mythril/laser/ethereum/transaction.py @@ -0,0 +1,60 @@ +import logging +from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType +from mythril.laser.ethereum.cfg import Node, Edge, JumpType +from z3 import BitVec + + +class MessageCall: + + """ Represents a call value transaction """ + def __init__(self, callee_address): + """ + Constructor for Call transaction, sets up all symbolic parameters + :param callee_address: Address of the contract that will be called + """ + self.callee_address = callee_address + self.caller = BitVec("caller", 256) + self.gas_price = BitVec("gasprice", 256) + self.call_value = BitVec("callvalue", 256) + self.origin = BitVec("origin", 256) + + self.open_states = None + + @property + def has_ran(self): + return self.open_states is not None + + def run(self, open_world_states: list, evm): + """ Runs this transaction on the evm starting from the open world states """ + # Consume the open states + open_states = open_world_states[:] + del open_world_states[:] + + for open_world_state in open_states: + + # Initialize the execution environment + environment = Environment( + open_world_state[self.callee_address], + self.caller, + [], + self.gas_price, + self.call_value, + self.origin, + calldata_type=CalldataType.SYMBOLIC, + ) + + new_node = Node(environment.active_account.contract_name) + evm.instructions_covered = [False for _ in environment.code.instruction_list] + + evm.nodes[new_node.uid] = new_node + if open_world_state.node: + evm.edges.append(Edge(open_world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction, condition=None)) + + global_state = GlobalState(open_world_state.accounts, environment, new_node) + new_node.states.append(global_state) + + evm.work_list.append(global_state) + + evm.exec() + logging.info("Execution complete") + logging.info("Achieved {0:.3g}% coverage".format(evm.coverage)) diff --git a/mythril/leveldb/client.py b/mythril/leveldb/client.py index 5f1e4221..bbed33a4 100644 --- a/mythril/leveldb/client.py +++ b/mythril/leveldb/client.py @@ -1,13 +1,11 @@ -import plyvel import binascii import rlp -import hashlib import logging from ethereum import utils from ethereum.block import BlockHeader, Block -from mythril.leveldb.state import State, Account +from mythril.leveldb.state import State from mythril.leveldb.eth_db import ETH_DB -from mythril.ether.ethcontract import ETHContract, InstanceList +from mythril.ether.ethcontract import ETHContract # Per https://github.com/ethereum/go-ethereum/blob/master/core/database_util.go # prefixes and suffixes for keys in geth @@ -16,7 +14,8 @@ bodyPrefix = b'b' # bodyPrefix + num (uint64 big endian) + hash -> block b numSuffix = b'n' # headerPrefix + num (uint64 big endian) + numSuffix -> hash blockHashPrefix = b'H' # blockHashPrefix + hash -> num (uint64 big endian) # known geth keys -headHeaderKey = b'LastBlock' # head (latest) header hash +headHeaderKey = b'LastBlock' # head (latest) header hash + def _formatBlockNumber(number): ''' @@ -24,12 +23,14 @@ def _formatBlockNumber(number): ''' return utils.zpad(utils.int_to_big_endian(number), 8) + def _encode_hex(v): ''' encodes hash as hex ''' return '0x' + utils.encode_hex(v) + class EthLevelDB(object): ''' Go-Ethereum LevelDB client class diff --git a/tests/native_test.py b/tests/native_test.py index 8deb4d39..374c8cbf 100644 --- a/tests/native_test.py +++ b/tests/native_test.py @@ -47,7 +47,7 @@ IDENTITY_TEST[3] = (83269476937987, False) def _all_info(laser): accounts = {} - for address, _account in laser.accounts.items(): + for address, _account in laser.world_state.accounts.items(): account = _account.as_dict account["code"] = account["code"].instruction_list account['balance'] = str(account['balance']) diff --git a/tests/svm_test.py b/tests/svm_test.py index e8ffabeb..57f2d171 100644 --- a/tests/svm_test.py +++ b/tests/svm_test.py @@ -18,7 +18,7 @@ class LaserEncoder(json.JSONEncoder): def _all_info(laser): accounts = {} - for address, _account in laser.accounts.items(): + for address, _account in laser.world_state.accounts.items(): account = _account.as_dict account["code"] = account["code"].instruction_list account['balance'] = str(account['balance'])