From 1ce6fbb588a8662f1e56393a989813929bea5846 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 9 Nov 2017 17:59:16 +0700 Subject: [PATCH] Update security checks --- mythril/analysis/modules/ether_send.py | 47 ++++++++++++------- mythril/analysis/modules/unchecked_suicide.py | 29 +++++------- mythril/analysis/solver.py | 16 +++++++ mythril/analysis/symbolic.py | 17 +++++-- mythril/exceptions.py | 3 ++ 5 files changed, 75 insertions(+), 37 deletions(-) create mode 100644 mythril/analysis/solver.py diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py index 52c2abcb..87b78e0f 100644 --- a/mythril/analysis/modules/ether_send.py +++ b/mythril/analysis/modules/ether_send.py @@ -1,6 +1,8 @@ from z3 import * from mythril.analysis.ops import * +from mythril.analysis import solver from mythril.analysis.report import Issue +from mythril.exceptions import UnsatError import re import logging @@ -41,6 +43,8 @@ def execute(statespace): issue.description += "a non-zero amount of Ether is sent to an address taken from function arguments.\n" interesting = True + issue.description += "Call value is " + str(call.value) + "\n" + if interesting: node = call.node @@ -48,33 +52,44 @@ def execute(statespace): can_solve = True for constraint in node.constraints: - m = re.search(r'storage_([0-9a-f])+', str(constraint)) - if (m): - index = m.group(1) + m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) - write_func = statespace.find_storage_write(index) + can_solve = True - if write_func is None: - can_solve = False - break + if (m): + index = m.group(1) - if can_solve: + try: + can_write = False - s = Solver() + for s in statespace.sstors[index]: - for constraint in node.constraints: - s.add(constraint) + if s.tainted: + can_write = True - if (s.check() == sat): + issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'." + break - m = s.model() + if not can_write: + logging.info("No storage writes to index " + str(index)) + can_solve = False + break - logging.debug("Model for node " + str(node.uid) + ", function " + node.function_name + ": ") + except KeyError: + logging.info("No storage writes to index " + str(index)) + can_solve = False + break - for d in m.decls(): - logging.debug("%s = 0x%x" % (d.name(), m[d].as_long())) + if can_solve: + try: + model = solver.get_model(node.constraints) issues.append(issue) + for d in model.decls(): + logging.debug("[UNCHECKED_SEND] %s = 0x%x" % (d.name(), model[d].as_long())) + except UnsatError: + logging.debug("[UNCHECKED_SEND] no model found") + return issues \ No newline at end of file diff --git a/mythril/analysis/modules/unchecked_suicide.py b/mythril/analysis/modules/unchecked_suicide.py index 93f470da..b1f7e5ae 100644 --- a/mythril/analysis/modules/unchecked_suicide.py +++ b/mythril/analysis/modules/unchecked_suicide.py @@ -1,10 +1,13 @@ from z3 import * +from mythril.analysis import solver from mythril.analysis.ops import * from mythril.analysis.report import Issue +from mythril.exceptions import UnsatError import re import logging + ''' MODULE DESCRIPTION: @@ -52,8 +55,9 @@ def execute(statespace): can_write = False for s in statespace.sstors[index]: + if s.tainted: - can_write = True + can_write = Trues issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'." break @@ -70,24 +74,13 @@ def execute(statespace): if can_solve: - s = Solver() - - for constraint in node.constraints: - s.add(constraint) - - if (s.check() == sat): - - m = s.model() - - logging.debug("Model for node " + str(node.uid) + ", function " + node.function_name + ": ") - - for d in m.decls(): - logging.debug("%s = 0x%x" % (d.name(), m[d].as_long())) - + try: + model = solver.get_model(node.constraints) issues.append(issue) - else: - logging.debug("unsat") - + for d in model.decls(): + logging.debug("[UNCHECKED_SUICIDE] main model: %s = 0x%x" % (d.name(), model[d].as_long())) + except UnsatError: + logging.debug("[UNCHECKED_SUICIDE] no model found") return issues diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py new file mode 100644 index 00000000..89b616a5 --- /dev/null +++ b/mythril/analysis/solver.py @@ -0,0 +1,16 @@ +from z3 import * +from mythril.exceptions import UnsatError + +def get_model(constraints): + s = Solver() + + for constraint in constraints: + s.add(constraint) + + if (s.check() == sat): + + return s.model() + + else: + raise UnsatError + diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 178beec7..41382e11 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -1,5 +1,8 @@ +from mythril.analysis import solver +from mythril.exceptions import UnsatError from laser.ethereum import svm from .ops import * +import logging class StateSpace: @@ -66,18 +69,26 @@ class StateSpace: def sstor_analysis(self): + logging.debug("Analyzing storage operations...") + for index in self.sstors: for s in self.sstors[index]: - s.tainted = True - - # For now we simply 'taint' every storage location that can be written to without any constraint on msg.sender + # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender for constraint in s.node.constraints: + logging.debug("Constraint: " + str(constraint)) if ("caller" in str(constraint)): s.tainted = False break + try: + solver.get_model(s.node.constraints) + s.tainted = True + except UnsatError: + s.tainted = False + + def find_storage_write(self, index): diff --git a/mythril/exceptions.py b/mythril/exceptions.py index 7915c482..3a0103b3 100644 --- a/mythril/exceptions.py +++ b/mythril/exceptions.py @@ -1,2 +1,5 @@ class CompilerError(Exception): + pass + +class UnsatError(Exception): pass \ No newline at end of file