diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index f8268b97..d5090a00 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -25,7 +25,6 @@ def execute(statespace): if (call.node.function_name == "fallback"): stack = state.mstate.stack - meminstart = get_variable(stack[-3]) if meminstart.type == VarType.CONCRETE: diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py index 53fee4eb..f330423e 100644 --- a/mythril/analysis/modules/ether_send.py +++ b/mythril/analysis/modules/ether_send.py @@ -39,7 +39,7 @@ def execute(statespace): interesting = False - description = "In the function '" + call.node.function_name +"' " + description = "In the function '" + call.node.function_name + "' " if re.search(r'caller', str(call.to)): description += "a non-zero amount of Ether is sent to msg.sender.\n" @@ -55,10 +55,12 @@ def execute(statespace): if (m): idx = m.group(1) + description += "a non-zero amount of Ether is sent to an address taken from storage slot " + str(idx) + func = statespace.find_storage_write(idx) if (func): - description += "\nThere is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function '" + func + "'.\n" + 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: logging.debug("[ETHER_SEND] No storage writes to index " + str(idx)) @@ -108,12 +110,13 @@ def execute(statespace): try: model = solver.get_model(node.constraints) - logging.debug("[ETHER_SEND] MODEL: " + str(model)) 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, address, "Ether send", "Warning", description) + 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) issues.append(issue) except UnsatError: diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 762fc5c7..a55d4187 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -1,14 +1,14 @@ from mythril.analysis.report import Issue from mythril.exceptions import UnsatError from mythril.analysis import solver -from z3 import simplify import logging ''' MODULE DESCRIPTION: -Check for constraints on tx.origin (i.e., access to some functionality is restricted to a specific origin). +Checks whether any exception states are reachable. + ''' @@ -27,30 +27,18 @@ def execute(statespace): if(instruction['opcode'] == "ASSERT_FAIL"): - logging.debug("Opcode 0xfe detected.") - try: model = solver.get_model(node.constraints) - logging.debug("[EXCEPTIONS] MODEL: " + str(model)) - address = state.get_current_instruction()['address'] description = "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. " description += "This is acceptable in most situations. Note however that assert() should only be used to check invariants. Use require() for regular input checking. " - description += "The exception is triggered under the following conditions:\n\n" - - for d in model.decls(): - - try: - condition = hex(model[d].as_long()) - except: - condition = str(simplify(model[d])) - description += ("%s: %s\n" % (d.name(), condition)) + debug = "The exception is triggered under the following conditions:\n\n" - description += "\n" + debug += solver.pretty_print_model(model) - issues.append(Issue(node.contract_name, node.function_name, address, "Exception state", "Informational", description)) + issues.append(Issue(node.contract_name, node.function_name, address, "Exception state", "Informational", description, debug)) except UnsatError: logging.debug("[EXCEPTIONS] no model found") diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index c0d6db1b..59ca1e8e 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -1,6 +1,7 @@ from z3 import * from mythril.analysis.ops import * from mythril.analysis.report import Issue +from mythril.analysis import solver import re import logging diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 7b1a0bdc..b33d7d16 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -4,6 +4,7 @@ from mythril.analysis.ops import * from mythril.analysis.report import Issue from mythril.exceptions import UnsatError import re +import copy import logging @@ -14,6 +15,7 @@ Check for integer underflows. For every SUB instruction, check if there's a possible state where op1 > op0. ''' + def execute(statespace): logging.debug("Executing module: INTEGER") @@ -43,13 +45,11 @@ def execute(statespace): or (re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL)) \ or (re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL)): - # Filter for patterns that contain possible (but apparently non-exploitable) Integer underflows. + # Filter for patterns that contain bening nteger underflows. # Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large. # Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0 - # Both seem to be standard compiler outputs that exist in many contracts. - continue logging.debug("[INTEGER_UNDERFLOW] Checking SUB " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address'])) @@ -60,22 +60,18 @@ def execute(statespace): constraints.append(UGT(op1,op0)) try: - + model = solver.get_model(constraints) issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", "Warning") issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \ - "The SUB instruction at address " + str(instruction['address']) + " may result in a value < 0." - - issue.debug = "(" + str(op0) + ") - (" + str(op1) + ").]" + "The substraction may result in a value < 0." + issue.debug = solver.pretty_print_model(model) issues.append(issue) - for d in model.decls(): - logging.debug("[INTEGER_UNDERFLOW] model: %s = 0x%x" % (d.name(), model[d].as_long())) - except UnsatError: - logging.debug("[INTEGER_UNDERFLOW] no model found") + logging.debug("[INTEGER_UNDERFLOW] no model found") return issues diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 0c692ccc..0978fbe5 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -38,13 +38,13 @@ def execute(statespace): to = stack.pop() if ("caller" in str(to)): - description += "The remaining Ether is sent to the caller's address." + description += "The remaining Ether is sent to the caller's address.\n" elif ("storage" in str(to)): - description += "The remaining Ether is sent to a stored address." + description += "The remaining Ether is sent to a stored address.\n" elif ("calldata" in str(to)): - description += "The remaining Ether is sent to an address provided as a function argument." + description += "The remaining Ether is sent to an address provided as a function argument.\n" elif (type(to) == BitVecNumRef): - description += "The remaining Ether is sent to: " + hex(to.as_long()) + description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n" else: description += "The remaining Ether is sent to: " + str(to) + "\n" @@ -62,8 +62,6 @@ def execute(statespace): m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) - overwrite = False - if (m): constrained = True idx = m.group(1) @@ -80,11 +78,9 @@ def execute(statespace): can_solve = False break - # 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))): - can_solve = False - break + can_solve = False + break if not constrained: description += "\nIt seems that this function can be called without restrictions." @@ -93,18 +89,14 @@ def execute(statespace): try: - model = solver.get_model(node.constraints) - logging.debug("[UNCHECKED_SUICIDE] MODEL: " + str(model)) - - for d in model.decls(): - logging.debug("[UNCHECKED_SUICIDE] main model: %s = 0x%x" % (d.name(), model[d].as_long())) + debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model) - issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description) + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug) issues.append(issue) except UnsatError: - logging.debug("[UNCHECKED_SUICIDE] no model found") + logging.debug("[UNCHECKED_SUICIDE] no model found") return issues diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index 83b10ed2..9746df4f 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -68,7 +68,7 @@ class Report: text += "\n\n" + issue.code + "\n\n--------------------\n" if self.verbose and issue.debug: - text += "\nDEBUGGING INFORMATION:\n\n" + issue.debug + "\n\n--------------------\n" + text += "\nDEBUGGING INFORMATION:\n\n" + issue.debug + "\n--------------------\n" text += "\n" diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index b1543d4c..b52b4475 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -1,6 +1,7 @@ -from z3 import * +from z3 import Solver, simplify, sat from mythril.exceptions import UnsatError -import logging +import re + def get_model(constraints): s = Solver() @@ -14,4 +15,23 @@ def get_model(constraints): return s.model() else: - raise UnsatError \ No newline at end of file + raise UnsatError + + +def pretty_print_model(model): + + ret = "" + + for d in model.decls(): + + try: + if (re.match(r'^calldata_.*_(\d)+', d.name())): + condition = "%064x" % model[d].as_long() + else: + condition = str(model[d].as_long()) + except: + condition = str(simplify(model[d])) + + ret += ("%s: %s\n" % (d.name(), condition)) + + return ret diff --git a/solidity_examples/suicide.sol b/solidity_examples/suicide.sol new file mode 100644 index 00000000..1763365b --- /dev/null +++ b/solidity_examples/suicide.sol @@ -0,0 +1,7 @@ +contract Suicide { + + function kill(address addr) { + selfdestruct(addr); + } + +} \ No newline at end of file