Merge branch 'bugfix/bectoken' into bugfix/taint_active_account

# Conflicts:
#	mythril/laser/ethereum/taint_analysis.py

.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

mythril/analysis/modules/ether_send.py

@@ -27,14 +27,13 @@ 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:
+        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:

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

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

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)

mythril/disassembler/disassembly.py

@@ -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

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

mythril/laser/ethereum/cfg.py

@@ -8,6 +8,7 @@ class JumpType(Enum):
     UNCONDITIONAL = 2
     CALL = 3
     RETURN = 4
+    Transaction = 5
 
 
 class NodeFlags(Flags):

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.")

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

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
+        transaction = MessageCall(main_address)
+        transaction.run(self.open_states, self)
 
-        global_state = GlobalState(self.accounts, environment, initial_node)
-        global_state.environment.active_function_name = "fallback()"
-        initial_node.states.append(global_state)
-
-        # 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

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)

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

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
@@ -18,18 +16,21 @@ blockHashPrefix = b'H'  # blockHashPrefix + hash -> num (uint64 big endian)
 # known geth keys
 headHeaderKey = b'LastBlock'  # head (latest) header hash
 
+
 def _formatBlockNumber(number):
     '''
     formats block number to uint64 big endian
     '''
     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

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'])

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'])