Integrate security tests

myth

@@ -5,7 +5,7 @@
 """
 
 from mythril.ether import evm, util
-from mythril.disassembler.callgraph import generate_callgraph
+from mythril.disassembler.callgraph import generate_graph
 from mythril.ether.contractstorage import get_persistent_storage
 from mythril.ether.ethcontract import ETHContract
 from mythril.ether.util import compile_solidity
@@ -13,8 +13,9 @@ from mythril.rpc.client import EthJsonRpc
 from mythril.ipc.client import EthIpc
 from mythril.support.loader import DynLoader
 from mythril.exceptions import CompilerError
+from mythril.analysis.symbolic import StateSpace
+from mythril.analysis.security import fire_lasers
 from ethereum import utils
-from laser.ethereum import svm, laserfree
 from pathlib import Path
 import logging
 import sys
@@ -197,39 +198,29 @@ elif (args.xrefs):
 
 elif (args.graph) or (args.fire_lasers):
 
-    # Convert to LASER SVM format
-
-    modules = {}
-
-    for contract in contracts:
-        modules[contract.address] = contract.as_dict()
-
     if (args.dynld):
         loader = DynLoader(eth)
-        _svm = svm.SVM(modules, dynamic_loader=loader)
-    else:
-        _svm = svm.SVM(modules)
-
+ 
     if (args.graph):
 
-        _svm.simplify_model = True
+        states = StateSpace(contracts, dynamic_loader=loader, simplify_model=True)
 
         if args.enable_physics is not None:
             physics = True
 
-        html = generate_callgraph(_svm, contracts[0].address, args.enable_physics)
+        html = generate_graph(states, args.enable_physics)
 
         try:
             with open(args.graph, "w") as f:
                 f.write(html)
         except Exception as e:
-
             print("Error saving graph: " + str(e))
 
     else:
 
-        _svm.sym_exec(contracts[0].address)
-        laserfree.fire(_svm)
+        states = StateSpace(contracts, dynamic_loader=loader)
+
+        fire_lasers(states)
 
 else:
     parser.print_help()

mythril/analysis/modules/ether_send.py

@@ -0,0 +1,96 @@
+from z3 import *
+from laser.ethereum import helper
+import re
+import logging
+from enum import Enum
+
+
+class TransferType(Enum):
+    HARDCODED = 1
+    CALLDATA = 2
+    CALLER = 3
+    OTHER = 3
+
+
+def execute(svm):
+
+    for k in svm.nodes:
+        node = svm.nodes[k]
+
+        for instruction in node.instruction_list:
+
+            if(instruction['opcode'] == "CALL"):
+
+                state = node.states[instruction['address']]
+
+                gas, to, value, meminstart, meminsz, memoutstart, memoutsz = \
+                        state.stack.pop(), state.stack.pop(), state.stack.pop(), state.stack.pop(), state.stack.pop(), state.stack.pop(), state.stack.pop()
+
+                interesting = False
+
+                try:
+                    value = helper.get_concrete_int(value)
+                    if(value > 0):
+                        print ("Call with non-zero value: " + str(value))
+                        interesting = True
+                except AttributeError:
+                    print ("Call with symbolic value: " + str(value))
+                    interesting = True
+
+                if interesting:
+
+                    try:
+                        to = helper.get_concrete_int(to).hex()
+                    except AttributeError:
+                        to = str(simplify(to))
+
+                    print("Function name: " + str(node.function_name))
+
+                    m = re.search(r'calldata_(\d)', to)
+
+                    if m:
+                        cd_index = m.group(1)
+                        print("Transfer to [calldata_" + str(cd_index) + "] " + str(node.function_name))
+                        transfer_type = TransferType.CALLDATA
+                    else:
+                        m = re.search(r'caller', to)
+
+                        if m:
+                            print("Transfer to msg.sender")
+                            transfer_type = TransferType.CALLER
+                        else:
+                            m = re.match(r'0x[0-9a-f]+', to)
+                            if m:
+                                print("Transfer to address " + to)
+                                transfer_type = TransferType.HARDCODED
+                            else:
+                                print("Transfer to " + to)
+                                transfer_type = TransferType.OTHER
+
+
+                    for constraint in node.constraints:
+                        m = re.search(r'caller', str(constraint))
+                        n = re.search(r'storage_(\d+)', str(constraint))
+
+                        if (m and n):
+                            storage_index = n.group(1)
+
+                            print("constraint on caller == storage_" + str(storage_index))
+                            break
+
+                    s = Solver()
+
+                    s.set(timeout=5000)
+
+                    for constraint in node.constraints:
+                        s.add(constraint)
+
+                    if (s.check() == sat):
+
+                        m = s.model()
+
+                        for d in m.decls():
+                            print("%s = 0x%x" % (d.name(), m[d].as_long()))
+
+                    else:
+                        print("unsat")

mythril/analysis/modules/unchecked_suicide.py

@@ -0,0 +1,31 @@
+from z3 import *
+
+
+def execute(svm):
+
+    for k in svm.nodes:
+        node = svm.nodes[k]
+
+        for instruction in node.instruction_list:
+
+            if(instruction['opcode'] == "SUICIDE"):
+                state = node.states[instruction['address']]
+                to = state.stack.pop()
+
+                print("SUICIDE to: " + str(to))
+                print("function: " + str(node.function_name))
+
+                s = Solver()
+
+                for constraint in node.constraints:
+                    s.add(constraint)
+
+                if (s.check() == sat):
+                    print("MODEL:")
+
+                    m = s.model()
+
+                    for d in m.decls():
+                        print("%s = 0x%x" % (d.name(), m[d].as_long()))
+                else:
+                    print("unsat")

mythril/analysis/security.py

@@ -0,0 +1,3 @@
+def fire_lasers:
+	pass
+	

mythril/analysis/symbolic.py

@@ -0,0 +1,26 @@
+from laser.ethereum import svm
+from .modules import unchecked_suicide, ether_send
+import logging
+
+
+class StateSpace:
+
+    '''
+    Symbolic EVM wrapper
+    '''
+    
+    def __init__(self, contracts, main_contract, dynloader = None, simplify=True):
+
+        # Convert ETHContract objects to LASER SVM "modules"
+
+        modules = {}
+
+        for contract in contracts:
+            modules[contract.address] = contract.as_dict()
+
+        _svm = svm.SVM(modules, modules[0], dynamic_loader=dynloader, simplify=simplify)
+
+        _svm.sym_exec()
+
+        self.nodes = _svm.nodes
+        self.edges = _svm.edges

mythril/disassembler/callgraph.py

@@ -98,22 +98,22 @@ colors = [
 ]  
 
 
-def serialize(_svm, color_map):
+def serialize(statespace, color_map):
 
     nodes = []
     edges = []
 
-    for node_key in _svm.nodes:
+    for node_key in statespace.nodes:
 
-        code =  _svm.nodes[node_key].as_dict()['code']
+        code =  statespace.nodes[node_key].as_dict()['code']
 
         code = re.sub("([0-9a-f]{8})[0-9a-f]+",  lambda m: m.group(1) + "(...)", code)
 
-        color = color_map[_svm.nodes[node_key].as_dict()['module_name']]
+        color = color_map[statespace.nodes[node_key].as_dict()['module_name']]
 
         nodes.append("{id: '" + str(node_key) + "', color: " + color + ", size: 150, 'label': '" + code + "'}")
 
-    for edge in _svm.edges:
+    for edge in statespace.edges:
 
       if (edge.condition is None):
           label = ""
@@ -133,19 +133,17 @@ def serialize(_svm, color_map):
 
 
 
-def generate_callgraph(svm, main_address, physics):
-
-    svm.sym_exec(main_address)
+def generate_graph(statespace, physics):
 
     i = 0
 
     color_map = {}
 
-    for k in svm.modules:
-      color_map[svm.modules[k]['name']] = colors[i]
+    for k in statespace.modules:
+      color_map[statespace.modules[k]['name']] = colors[i]
       i += 1
 
-    html = graph_html.replace("[JS]", serialize(svm, color_map))
+    html = graph_html.replace("[JS]", serialize(statespace, color_map))
     html = html.replace("[ENABLE_PHYSICS]", str(physics).lower())
 
     return html