diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py index e86edd45..7cb4cd0a 100644 --- a/mythril/analysis/modules/ether_send.py +++ b/mythril/analysis/modules/ether_send.py @@ -25,8 +25,6 @@ def execute(statespace): logging.debug("[ETHER_SEND] Skipping refund function") continue - issue = Issue("Ether send", "Warning") - # We're only interested in calls that send Ether if call.value.type == VarType.CONCRETE: @@ -35,10 +33,9 @@ def execute(statespace): interesting = False + issue = Issue("Ether send", "Warning") issue.description = "In the function '" + call.node.function_name +"' " - # Check the CALL target - if re.search(r'caller', str(call.to)): issue.description += "a non-zero amount of Ether is sent to msg.sender.\n" interesting = True diff --git a/mythril/analysis/modules/integer_underflow.py b/mythril/analysis/modules/integer_underflow.py index 65cc2c71..1f397591 100644 --- a/mythril/analysis/modules/integer_underflow.py +++ b/mythril/analysis/modules/integer_underflow.py @@ -46,6 +46,9 @@ def execute(statespace): issue = Issue("Integer Underflow", "Warning") + op0 = str(op0).replace("\n","") + op1 = str(op1).replace("\n","") + issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \ "There SUB instruction at address " + str(instruction['address']) + " performs the operation " + str(op0) + " - " + str(op1) + ". " \ "However, it is not verified that " + str(op0) + " >= " + str(op1) + "." diff --git a/mythril/analysis/modules/send_with_gas.py b/mythril/analysis/modules/send_with_gas.py new file mode 100644 index 00000000..26333d8b --- /dev/null +++ b/mythril/analysis/modules/send_with_gas.py @@ -0,0 +1,114 @@ +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 + + +''' +MODULE DESCRIPTION: + +Check for CALLs that send >0 Ether to either the transaction sender, or to an address provided as a function argument. +If msg.sender is checked against a value in storage, check whether that storage index is tainted (i.e. there's an unconstrained write +to that index). +''' + +def execute(statespace): + + issues = [] + + for call in statespace.calls: + + if ("callvalue" in str(call.value)): + logging.debug("[ETHER_SEND] Skipping refund function") + continue + + # We're only interested in calls that send Ether + + if call.value.type == VarType.CONCRETE: + if call.value.val == 0: + continue + + logging.debug("[SEND_WITH_GAS]: ") + + # Check the CALL target + + if re.search(r'caller', str(call.to)): + issue.description += "a non-zero amount of Ether is sent to msg.sender.\n" + interesting = True + + if re.search(r'calldata', str(call.to)): + issue.description += "a non-zero amount of Ether is sent to an address taken from function arguments.\n" + interesting = True + + if interesting: + + issue = Issue("Ether send", "Warning") + issue.description = "In the function '" + call.node.function_name +"' " + issue.description += "Call value is " + str(call.value) + "\n" + + node = call.node + + constrained = False + can_solve = True + + index = 0 + + while(can_solve and index < len(node.constraints)): + + constraint = node.constraints[index] + index += 1 + logging.debug("[ETHER_SEND] Constraint: " + str(constraint)) + + m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) + + overwrite = False + + if (m): + constrained = True + index = m.group(1) + + try: + + for s in statespace.sstors[index]: + + if s.tainted: + 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 + + if not overwrite: + logging.debug("[ETHER_SEND] No storage writes to index " + str(index)) + can_solve = False + break + + except KeyError: + logging.debug("[ETHER_SEND] No storage writes to index " + str(index)) + 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 + + + if not constrained: + issue.description += "\nIt seems that this function can be called without restrictions." + + if can_solve: + + try: + model = solver.get_model(node.constraints) + logging.debug("[ETHER_SEND] MODEL: " + str(model)) + issues.append(issue) + + for d in model.decls(): + logging.debug("[ETHER_SEND] main model: %s = 0x%x" % (d.name(), model[d].as_long())) + except UnsatError: + logging.debug("[ETHER_SEND] no model found") + + return issues diff --git a/mythril/analysis/security.py b/mythril/analysis/security.py index f162cf84..a4cfa9f6 100644 --- a/mythril/analysis/security.py +++ b/mythril/analysis/security.py @@ -1,5 +1,5 @@ from mythril.analysis.report import Report -from .modules import delegatecall_forward, unchecked_suicide, ether_send, unchecked_retval, integer_underflow, delegatecall_to_dynamic +from .modules import delegatecall_forward, unchecked_suicide, ether_send, unchecked_retval, delegatecall_to_dynamic, integer_underflow def fire_lasers(statespace): @@ -9,8 +9,8 @@ def fire_lasers(statespace): issues += delegatecall_forward.execute(statespace) issues += delegatecall_to_dynamic.execute(statespace) issues += unchecked_suicide.execute(statespace) - issues += ether_send.execute(statespace) issues += unchecked_retval.execute(statespace) + issues += ether_send.execute(statespace) issues += integer_underflow.execute(statespace) if (len(issues)):