diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py index e86edd45..3b9814a6 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,8 +33,6 @@ def execute(statespace): interesting = False - issue.description = "In the function '" + call.node.function_name +"' " - # Check the CALL target if re.search(r'caller', str(call.to)): @@ -47,10 +43,12 @@ 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: + 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 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