Quick & dirty fixes for analysis modules

myth

@@ -390,13 +390,13 @@ elif (args.graph) or (args.fire_lasers):
 
         for contract in contracts:
 
-            #try:
+            # try:
             if (args.dynld):
                 states = StateSpace([contract], dynloader=DynLoader(eth), max_depth=args.max_depth)
             else:
                 states = StateSpace([contract], max_depth=args.max_depth)
-            #except Exception as e:
-            #    exitWithError(args.outform, "Symbolic exection error: " + str(e))        
+            # except Exception as e:
+            #    exitWithError(args.outform, "Symbolic exection error: " + str(e))
 
             issues = fire_lasers(states)
 
@@ -413,6 +413,7 @@ elif (args.graph) or (args.fire_lasers):
                         if (issue.pc):
 
                             index = helper.get_instruction_index(disassembly.instruction_list, issue.pc)
+
                             solidity_file = contract.solidity_files[contract.mappings[index].solidity_file_idx]
 
                             issue.filename = solidity_file.filename

mythril/analysis/modules/call_to_dynamic_with_gas.py

@@ -19,6 +19,9 @@ def execute(statespace):
 
     for call in statespace.calls:
 
+        state = call.state
+        address = state.get_current_instruction()['address']
+
         if (call.type == "CALL"):
 
             logging.debug("[CALL_TO_DYNAMIC_WITH_GAS] Call to: " + str(call.to) + ", value " + str(call.value) + ", gas = " + str(call.gas))
@@ -44,29 +47,23 @@ def execute(statespace):
                     if (m):
                         index = m.group(1)
 
-                        try:
-
-                            for s in statespace.sstors[index]:
-
-                                if s.tainted:
+                        func = statespace.find_storage_write(index)
 
-                                    description += \
-                                        "an address found at storage position " + str(index) + ".\n" + \
-                                        "This storage position can be written to by calling the function '" + s.node.function_name + "'.\n" \
-                                        "Verify that the contract address cannot be set by untrusted users.\n"
+                        if func:
 
-                                    is_valid = True
-                                    break
+                            description += \
+                                "an address found at storage position " + str(index) + ".\n" + \
+                                "This storage position can be written to by calling the function '" + func + "'.\n" \
+                                "Verify that the contract address cannot be set by untrusted users.\n"
 
-                        except KeyError:
-                            logging.debug("[CALL_TO_DYNAMIC_WITH_GAS] No storage writes to index " + str(index))
-                            continue
+                            is_valid = True
+                            break
 
                 if is_valid:
 
                     description += "The available gas is forwarded to the called contract. Make sure that the logic of the calling contract is not adversely affected if the called contract misbehaves (e.g. reentrancy)." 
 
-                    issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "CALL with gas to dynamic address", "Warning", description)
+                    issue = Issue(call.node.contract_name, call.node.function_name, address, "CALL with gas to dynamic address", "Warning", description)
 
                     issues.append(issue)
 

mythril/analysis/modules/delegatecall_forward.py

@@ -21,12 +21,15 @@ def execute(statespace):
 
     for call in statespace.calls:
 
+        state = call.state
+        address = state.get_current_instruction()['address']
+
         # Only needs to be checked once per call instructions (essentially just static analysis)
 
-        if call.addr in visited:
+        if address in visited:
             continue
         else:
-            visited.append(call.addr)
+            visited.append(address)
 
         if (call.type == "DELEGATECALL") and (call.node.function_name == "fallback"):
 
@@ -36,9 +39,9 @@ def execute(statespace):
 
             if meminstart.type == VarType.CONCRETE:
 
-                if (re.search(r'calldata.*_0', str(call.state.mstate.memory[meminstart.val]))):
+                if (re.search(r'calldata.*_0', str(state.mstate.memory[meminstart.val]))):
 
-                    issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "CALLDATA forwarded with delegatecall()", "Informational")
+                    issue = Issue(call.node.contract_name, call.node.function_name, address, "CALLDATA forwarded with delegatecall()", "Informational")
 
                     issue.description = \
                         "This contract forwards its calldata via DELEGATECALL in its fallback function. " \

mythril/analysis/modules/delegatecall_to_dynamic.py

@@ -19,12 +19,15 @@ def execute(statespace):
 
     for call in statespace.calls:
 
+        state = call.state
+        address = state.get_current_instruction()['address']
+
         if (call.type == "DELEGATECALL" or call.type == "CALLCODE"):
 
             if (call.to.type == VarType.SYMBOLIC):
 
                 if ("calldata" in str(call.to)):
-                    issue = Issue(call.node.contract_name, call.node.function_name, call.addr, call.type + " to dynamic address")
+                    issue = Issue(call.node.contract_name, call.node.function_name, address, call.type + " to dynamic address")
 
                     issue.description = \
                         "The function " + call.node.function_name + " delegates execution to a contract address obtained from calldata.\n" \
@@ -56,7 +59,7 @@ def execute(statespace):
 
                     else:
 
-                        issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "DELEGATECALL to dynamic address", "Informational")
+                        issue = Issue(call.node.contract_name, call.node.function_name, address, "DELEGATECALL to dynamic address", "Informational")
 
                         issue.description = \
                             "The function " + call.node.function_name + " in contract '" + call.node.contract_name + " delegates execution to a contract with a dynamic address." \

mythril/analysis/modules/ether_send.py

@@ -23,6 +23,9 @@ def execute(statespace):
 
     for call in statespace.calls:
 
+        state = call.state
+        address = state.get_current_instruction()['address']
+
         if ("callvalue" in str(call.value)):
             logging.debug("[ETHER_SEND] Skipping refund function")
             continue
@@ -110,7 +113,7 @@ def execute(statespace):
                     for d in model.decls():
                         logging.debug("[ETHER_SEND] main model: %s = 0x%x" % (d.name(), model[d].as_long()))
 
-                    issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "Ether send", "Warning", description)
+                    issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning", description)
                     issues.append(issue)
 
                 except UnsatError:

mythril/analysis/modules/unchecked_retval.py

@@ -13,7 +13,7 @@ Test whether CALL return value is checked.
 
 For direct calls, the Solidity compiler auto-generates this check. E.g.:
 
-    Alice c = Alice(address);  
+    Alice c = Alice(address);
     c.ping(42);
 
 Here the CALL will be followed by IZSERO(retval), if retval = ZERO then state is reverted.
@@ -24,6 +24,7 @@ For low-level-calls this check is omitted. E.g.:
 
 '''
 
+
 def execute(statespace):
 
     logging.debug("Executing module: UNCHECKED_RETVAL")
@@ -33,15 +34,15 @@ def execute(statespace):
 
     for call in statespace.calls:
 
+        state = call.state
+        address = state.get_current_instruction()['address']
+
         # Only needs to be checked once per call instructions (it's essentially just static analysis)
 
-        if call.addr in visited:
+        if call.state.mstate.pc in visited:
             continue
         else:
-            visited.append(call.addr)
-
-        # The instructions executed in each node (basic block) are saved in node.instruction_list, e.g.:
-        # [{address: "132", opcode: "CALL"}, {address: "133", opcode: "ISZERO"}]
+            visited.append(call.state.mstate.pc)
 
         retval_checked = False
 
@@ -49,18 +50,20 @@ def execute(statespace):
 
         for i in range(0, 10):
 
+            _state = call.node.states[call.state_index + i]
+
             try:
-                instr = call.node.states[call.addr + i]
+                instr = _state.get_current_instruction()
             except IndexError:
                 break
 
-            if (instr['opcode'] == 'ISZERO' and re.search(r'retval', str(call.node.states[instr['address']].stack[-1]))):
+            if (instr['opcode'] == 'ISZERO' and re.search(r'retval', str(_state.mstate.stack[-1]))):
                 retval_checked = True
                 break
 
         if not retval_checked:
 
-            issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "Unchecked CALL return value")
+            issue = Issue(call.node.contract_name, call.node.function_name, address, "Unchecked CALL return value")
 
             if (call.to.type == VarType.CONCRETE):
                 receiver = hex(call.to.val)

mythril/analysis/modules/weak_random.py

@@ -37,7 +37,7 @@ def execute(statespace):
             if call.value.val == 0:
                 continue
 
-        description  = "In the function '" + call.node.function_name + "' "
+        description = "In the function '" + call.node.function_name + "' "
         description += "the following predictable state variables are used to determine Ether recipient:\n"
 
         # First check: look for predictable state variables in node & call recipient constraints
@@ -54,7 +54,7 @@ def execute(statespace):
             for item in found:
                 description += "- block.{}\n".format(item)
             if solve(call):
-                issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "Weak random", "Warning",
+                issue = Issue(call.node.contract_name, call.node.function_name, call.state.mstate.pc, "Weak random", "Warning",
                               description)
                 issues.append(issue)
 
@@ -74,7 +74,7 @@ def execute(statespace):
                                 ")' is used to determine Ether recipient"
                             if int(m.group(2)) > 255:
                                 description += ", this expression will always be equal to zero."
-                        elif "storage" in str(constraint): # block.blockhash(block.number - storage_0)
+                        elif "storage" in str(constraint):  # block.blockhash(block.number - storage_0)
                             description += "predictable expression 'block.blockhash(block.number - " + \
                                            "some_storage_var)' is used to determine Ether recipient"
                         else: # block.blockhash(block.number)
@@ -88,7 +88,7 @@ def execute(statespace):
                         break
                 else:
                     r = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
-                    if r: # block.blockhash(storage_0)
+                    if r:  # block.blockhash(storage_0)
 
                         '''
                         We actually can do better here by adding a constraint blockhash_block_storage_0 == 0

mythril/analysis/ops.py

@@ -18,19 +18,26 @@ class Variable:
         return str(self.val)
 
 
+def get_variable(i):
+    try:
+        return Variable(helper.get_concrete_int(i), VarType.CONCRETE)
+    except AttributeError:
+        return Variable(simplify(i), VarType.SYMBOLIC)
+
+
 class Op:
 
-    def __init__(self, node, state, addr):
+    def __init__(self, node, state, state_index):
         self.node = node
         self.state = state
-        self.addr = addr
+        self.state_index = state_index
 
 
 class Call(Op):
 
-    def __init__(self, node, state, addr, _type, to, gas, value=Variable(0, VarType.CONCRETE), data=None):
+    def __init__(self, node, state, state_index, _type, to, gas, value=Variable(0, VarType.CONCRETE), data=None):
 
-        super().__init__(node, state, addr)
+        super().__init__(node, state, state_index)
         self.to = to
         self.gas = gas
         self.type = _type
@@ -40,13 +47,8 @@ class Call(Op):
 
 class SStore(Op):
 
-    def __init__(self, node, state, addr, value):
-        super().__init__(node, state, addr)
+    def __init__(self, node, state, state_index, value):
+        super().__init__(node, state, state_index)
         self.value = value
 
 
-def get_variable(i):
-    try:
-        return Variable(helper.get_concrete_int(i), VarType.CONCRETE)
-    except AttributeError:
-        return Variable(simplify(i), VarType.SYMBOLIC)

mythril/analysis/symbolic.py

@@ -36,12 +36,16 @@ class StateSpace:
 
         for key in self.nodes:
 
+            state_index = 0
+
             for state in self.nodes[key].states:
 
                 instruction = state.get_current_instruction()
+
                 op = instruction['opcode']
 
                 if op in ('CALL', 'CALLCODE', 'DELEGATECALL', 'STATICCALL'):
+
                     stack = copy.deepcopy(state.mstate.stack)
 
                     if op in ('CALL', 'CALLCODE'):
@@ -54,14 +58,14 @@ class StateSpace:
                                 continue
 
                         if (meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE):
-                            self.calls.append(Call(self.nodes[key], state, instruction['address'], op, to, gas, value, state.mstate.memory[meminstart.val:meminsz.val*4]))
+                            self.calls.append(Call(self.nodes[key], state, state_index, op, to, gas, value, state.mstate.memory[meminstart.val:meminsz.val * 4]))
                         else:
-                            self.calls.append(Call(self.nodes[key], state, instruction['address'], op, to, gas, value))                     
+                            self.calls.append(Call(self.nodes[key], state, state_index, op, to, gas, value))
                     else:
                         gas, to, meminstart, meminsz, memoutstart, memoutsz = \
                             get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop())
 
-                        self.calls.append(Call(self.nodes[key], state, instruction['address'], op, to, gas))
+                        self.calls.append(Call(self.nodes[key], state, state_index, op, to, gas))
 
                 elif op == 'SSTORE':
                     stack = copy.deepcopy(state.mstate.stack)
@@ -69,13 +73,15 @@ class StateSpace:
                     index, value = stack.pop(), stack.pop()
 
                     try:
-                        self.sstors[str(index)].append(SStore(self.nodes[key], state, instruction['address'], value))
+                        self.sstors[str(index)].append(SStore(self.nodes[key], state, state_index, value))
                     except KeyError:
-                        self.sstors[str(index)] = [SStore(self.nodes[key], state, instruction['address'], value)]
+                        self.sstors[str(index)] = [SStore(self.nodes[key], state, state_index, value)]
+
+                state_index += 1
 
     def find_storage_write(self, index):
 
-        # Find a an unconstrained SSTOR that writes to storage index "index"
+        # Find an SSTOR not constrained by caller that writes to storage index "index"
 
         try:
             for s in self.sstors[index]:
@@ -86,6 +92,7 @@ class StateSpace:
                         taint = False
                         break
 
+                if taint:
                     return s.node.function_name
 
             return None