diff --git a/mythril/analysis/modules/integer_overflow.py b/mythril/analysis/modules/integer_overflow.py deleted file mode 100644 index ec3aad61..00000000 --- a/mythril/analysis/modules/integer_overflow.py +++ /dev/null @@ -1,110 +0,0 @@ -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 copy -import re -import logging - - -UINT_MAX = BitVecVal(2 ** 256 - 1, 256) - - -''' -MODULE DESCRIPTION: - -Check for integer overflows. -''' - -def execute(statespace): - - logging.debug("Executing module: INTEGER_OVERFLOW") - - issues = [] - - for k in statespace.nodes: - node = statespace.nodes[k] - - for instruction in node.instruction_list: - - ''' This generates a lot of noise. - - if(instruction['opcode'] == "ADD"): - - stack = node.states[instruction['address']].stack - - op0 = stack[-1] - op1 = stack[-2] - - if type(op0) == int and type(op1) == int: - continue - - logging.debug("[INTEGER_OVERFLOW] Checking ADD " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address'])) - - constraints = copy.deepcopy(node.constraints) - - constraints.append(UGT(op0, UINT_MAX - op1)) - - try: - - model = solver.get_model(constraints) - - issue = Issue(node.module_name, node.function_name, instruction['address'], "Integer Overflow", "Warning") - - issue.description = "A possible integer overflow exists in the function " + node.function_name + ".\n" \ - "The addition at address " + str(instruction['address']) + " may result in a value greater than UINT_MAX." - - issue.debug = "(" + str(op0) + ") + (" + str(op1) + ") > (" + hex(UINT_MAX.as_long()) + ")" - - issues.append(issue) - - for d in model.decls(): - logging.debug("[INTEGER_OVERFLOW] model: %s = 0x%x" % (d.name(), model[d].as_long())) - - except UnsatError: - logging.debug("[INTEGER_OVERFLOW] no model found") - - ''' - - if(instruction['opcode'] == "MUL"): - - stack = node.states[instruction['address']].stack - - op0 = stack[-1] - op1 = stack[-2] - - if (type(op0) == int and type(op1) == int) or type(op0) == BoolRef or type(op1) == BoolRef: - continue - - logging.debug("[INTEGER_OVERFLOW] Checking MUL " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address'])) - - if re.search(r'146150163733', str(op0), re.DOTALL) or re.search(r'146150163733', str(op1), re.DOTALL) or "(2 << 160 - 1)" in str(op0) or "(2 << 160 - 1)" in str(op1): - continue - - constraints = copy.deepcopy(node.constraints) - - constraints.append(UGT(op0, UDiv(UINT_MAX, op1))) - - try: - - model = solver.get_model(constraints) - - issue = Issue(node.module_name, node.function_name, instruction['address'], "Integer Overflow", "Warning") - - issue.description = "A possible integer overflow exists in the function " + node.function_name + ".\n" \ - "The multiplication at address " + str(instruction['address']) + " may result in a value greater than UINT_MAX." - - issue.debug = "(" + str(op0) + ") * (" + str(op1) + ") > (" + hex(UINT_MAX.as_long()) + ")" - - issues.append(issue) - - logging.debug("Constraints: " + str(constraints)) - - for d in model.decls(): - logging.debug("[INTEGER_OVERFLOW] model: %s = 0x%x" % (d.name(), model[d].as_long())) - - except UnsatError: - logging.debug("[INTEGER_OVERFLOW] no model found") - - return issues diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 04b9d7ad..c8f302ef 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -5,6 +5,11 @@ from .ops import * import logging +class SStorTaintStatus(Enum): + TAINTED = 1 + UNTAINTED = 2 + + class StateSpace: ''' @@ -34,6 +39,9 @@ class StateSpace: self.suicides = [] self.sstors = {} + self.sstor_taint_cache = [] + + for key in self.svm.nodes: for instruction in self.nodes[key].instruction_list: @@ -72,9 +80,10 @@ class StateSpace: except KeyError: self.sstors[str(index)] = [SStore(self.nodes[key], instruction['address'], value)] - self.sstor_analysis() + # self.sstor_analysis() + ''' def sstor_analysis(self): logging.info("Analyzing storage operations...") @@ -82,7 +91,7 @@ class StateSpace: for index in self.sstors: for s in self.sstors[index]: - # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender + # 'Taint' every 'store' instruction that is reachable without any constraint on msg.sender taint = True @@ -99,17 +108,25 @@ class StateSpace: s.tainted = True except UnsatError: s.tainted = False + ''' def find_storage_write(self, index): - # Find a tainted (unconstrained) SSTOR that writes to 'index' + # Find a an unconstrained SSTOR that writes to storage index "index" try: for s in self.sstors[index]: - if s.tainted: + taint = True + + for constraint in s.node.constraints: + if ("caller" in str(constraint)): + taint = False + break + return s.node.function_name + return None except KeyError: return None diff --git a/security_checks.md b/security_checks.md index 0bc2f171..8a21e95c 100644 --- a/security_checks.md +++ b/security_checks.md @@ -8,7 +8,7 @@ |Multiple sends in a single transaction| External calls can fail accidentally or deliberately. Avoid combining multiple send() calls in a single transaction. | | [Favor pull over push for external calls](https://consensys.github.io/smart-contract-best-practices/recommendations/#favor-pull-over-push-for-external-calls) | |Function call to untrusted contract| | [call to untrusted contract with gas](mythril/analysis/modules/call_to_dynamic_with_gas.py) | | |Delegatecall or callcode to untrusted contract| | [delegatecall_forward](mythril/analysis/modules/delegatecall_forward.py), [delegatecall_to_dynamic.py](mythril/analysis/modules/delegatecall_to_dynamic.py) | | -|Integer overflow/underflow| | [integer_underflow](mythril/analysis/modules/integer_underflow.py), [Integer overflow](/mythril/analysis/modules/integer_overflow.py) | | +|Integer overflow/underflow| | [integer_underflow](mythril/analysis/modules/integer_underflow.py) | | |Timestamp dependence| | | | |Payable transaction does not revert in case of failure | | | | |Call depth attack| | | |