From 7b3c1528440549cb307ff6baac0203361021b245 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 Nov 2017 15:05:48 +0700 Subject: [PATCH] Improve reporting --- .../modules/call_to_dynamic_with_gas.py | 14 ++++---- .../analysis/modules/delegatecall_forward.py | 3 +- .../modules/delegatecall_to_dynamic.py | 10 +++--- mythril/analysis/modules/ether_send.py | 35 +++++++++---------- mythril/analysis/modules/integer_underflow.py | 10 +++--- mythril/analysis/modules/unchecked_retval.py | 11 +++--- mythril/analysis/modules/unchecked_suicide.py | 23 ++++++------ mythril/analysis/report.py | 21 +++++++++-- 8 files changed, 72 insertions(+), 55 deletions(-) diff --git a/mythril/analysis/modules/call_to_dynamic_with_gas.py b/mythril/analysis/modules/call_to_dynamic_with_gas.py index cabec5a2..9542bb3c 100644 --- a/mythril/analysis/modules/call_to_dynamic_with_gas.py +++ b/mythril/analysis/modules/call_to_dynamic_with_gas.py @@ -23,8 +23,7 @@ def execute(statespace): if (call.to.type == VarType.SYMBOLIC and (call.gas.type == VarType.CONCRETE and call.gas.val > 2300) or (call.gas.type == VarType.SYMBOLIC and "2300" not in str(call.gas))): - issue = Issue("CALL with gas to dynamic address", "Warning") - issue.description = "The function " + call.node.function_name + " contains a call.value() to " + description = "The function " + call.node.function_name + " contains a call.value() to " target = str(call.to) is_valid = False @@ -32,9 +31,9 @@ def execute(statespace): if ("calldata" in target or "caller" in target): if ("calldata" in target): - issue.description += "an address provided as a function argument. " + description += "an address provided as a function argument. " else: - issue.description += "the address of the transaction sender. " + description += "the address of the transaction sender. " is_valid = True else: @@ -49,7 +48,7 @@ def execute(statespace): if s.tainted: - issue.description += \ + description += \ "an address found at storage position " + str(index) + ".\n" + \ "This storage position can be written to by calling the function '" + s.node.function_name + "'.\n" \ "Verify that the contract address cannot be set by untrusted users.\n" @@ -62,7 +61,10 @@ def execute(statespace): continue if is_valid: - issue.description += "The available gas is forwarded to the called contract.\nMake sure that the logic of the calling contract is not adversely affected if the called contract misbehaves (e.g. reentrancy)." + + description += "The available gas is forwarded to the called contract.\nMake sure that the logic of the calling contract is not adversely affected if the called contract misbehaves (e.g. reentrancy)." + + issue = Issue(call.node.module_name, call.node.function_name, call.addr, "CALL with gas to dynamic address", "Warning", description) issues.append(issue) diff --git a/mythril/analysis/modules/delegatecall_forward.py b/mythril/analysis/modules/delegatecall_forward.py index cfd376e3..c9745c09 100644 --- a/mythril/analysis/modules/delegatecall_forward.py +++ b/mythril/analysis/modules/delegatecall_forward.py @@ -34,7 +34,8 @@ def execute(statespace): if (re.search(r'calldata.*_0', str(call.state.memory[meminstart.val]))): - issue = Issue("CALLDATA forwarded with delegatecall()", "Informational") + issue = Issue(call.node.module_name, call.node.function_name, call.addr, "CALLDATA forwarded with delegatecall()", "Informational") + issue.description = \ "The contract '" + str(call.node.module_name) + "' forwards its calldata via DELEGATECALL in its fallback function. " \ "This means that any function in the called contract can be executed. Note that the callee contract will have access to the storage of the calling contract.\n" diff --git a/mythril/analysis/modules/delegatecall_to_dynamic.py b/mythril/analysis/modules/delegatecall_to_dynamic.py index 7f0961a0..364ee924 100644 --- a/mythril/analysis/modules/delegatecall_to_dynamic.py +++ b/mythril/analysis/modules/delegatecall_to_dynamic.py @@ -21,14 +21,12 @@ def execute(statespace): if (call.to.type == VarType.SYMBOLIC): - logging.debug("[DELEGATECALL_TO_DYNAMIC] checking...") - if ("calldata" in str(call.to)): - issue = Issue(call.type + " to dynamic address", "Vulnerability") + issue = Issue(call.node.module_name, call.node.function_name, call.addr, call.type + " to dynamic address") issue.description = \ - "The function " + call.node.function_name + " in contract '" + call.node.module_name + "' delegates execution to a contract address obtained from calldata.\n" \ - "To address: " + str(call.to) + "The function " + call.node.function_name + " delegates execution to a contract address obtained from calldata.\n" \ + "Recipient address: " + str(call.to) issues.append(issue) else: @@ -56,7 +54,7 @@ def execute(statespace): else: - issue = Issue("DELEGATECALL to dynamic address", "Informational") + issue = Issue(call.node.module_name, call.node.function_name, call.addr, "DELEGATECALL to dynamic address", "Informational") issue.description = \ "The function " + call.node.function_name + " in contract '" + call.node.module_name + " delegates execution to a contract with a dynamic address." \ diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py index 7cb4cd0a..c460e246 100644 --- a/mythril/analysis/modules/ether_send.py +++ b/mythril/analysis/modules/ether_send.py @@ -33,32 +33,30 @@ def execute(statespace): interesting = False - issue = Issue("Ether send", "Warning") - issue.description = "In the function '" + call.node.function_name +"' " + description = "In the function '" + call.node.function_name +"' " if re.search(r'caller', str(call.to)): - issue.description += "a non-zero amount of Ether is sent to msg.sender.\n" + 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" + 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: + 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 + constraint = node.constraints[index] logging.debug("[ETHER_SEND] Constraint: " + str(constraint)) m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) @@ -66,15 +64,15 @@ def execute(statespace): overwrite = False if (m): - constrained = True - index = m.group(1) + idx = m.group(1) try: - for s in statespace.sstors[index]: + for s in statespace.sstors[idx]: 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 + "'." + 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 + "'." + overwrite = True break if not overwrite: @@ -93,21 +91,22 @@ def execute(statespace): 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." + else: + 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())) + + issue = Issue(call.node.module_name, call.node.function_name, call.addr, "Ether send", "Warning", description) + issues.append(issue) + except UnsatError: - logging.debug("[ETHER_SEND] no model found") + logging.debug("[ETHER_SEND] no model found") return issues diff --git a/mythril/analysis/modules/integer_underflow.py b/mythril/analysis/modules/integer_underflow.py index 017f5749..bc498dc8 100644 --- a/mythril/analysis/modules/integer_underflow.py +++ b/mythril/analysis/modules/integer_underflow.py @@ -39,6 +39,7 @@ def execute(statespace): if re.search(r'\d* \+ calldata', str(op0)) and re.search(r'\d+', str(op1)): # Filter for a common pattern that contains an possible (but Ion-exploitable) Integer overflow and subsequent underflow. # The pattern looks as follows: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would overflow if calldatasize is very large. + # There's a few other things that sometimes pop up which still need to be investigated. continue @@ -50,14 +51,15 @@ def execute(statespace): model = solver.get_model(node.constraints) - issue = Issue("Integer Underflow", "Warning") - op0 = str(op0).replace("\n","") op1 = str(op1).replace("\n","") + issue = Issue(node.module_name, node.function_name, instruction['address'], "Integer Underflow", "Warning") + 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) + ")." + "The SUB instruction at address " + str(instruction['address']) + " may result in a value < 0." + + issue.debug = "(" + str(op0) + ") - (" + str(op1) + ").]n" \ issues.append(issue) diff --git a/mythril/analysis/modules/unchecked_retval.py b/mythril/analysis/modules/unchecked_retval.py index 9050ee6b..4dd05a8c 100644 --- a/mythril/analysis/modules/unchecked_retval.py +++ b/mythril/analysis/modules/unchecked_retval.py @@ -30,7 +30,7 @@ def execute(statespace): for call in statespace.calls: - # Only needs to be checked once per call instructions (essentially just static analysis) + # Only needs to be checked once per call instructions (it's essentially just static analysis) if call.addr in visited: continue @@ -44,8 +44,7 @@ def execute(statespace): retval_checked = False - # ISZERO retval should be found within the next 10 instructions. - # The stack contents at a particular point of execution are found in node.states[address].stack + # ISZERO retval should be found within the next few instructions. for i in range(0, 10): @@ -60,9 +59,7 @@ def execute(statespace): if not retval_checked: - issue = Issue("Unchecked CALL return value") - - logging.info("TYPE: " + str(type(call.to))) + issue = Issue(call.node.module_name, call.node.function_name, call.addr, "Unchecked CALL return value") if (call.to.type == VarType.CONCRETE): receiver = hex(call.to.val) @@ -75,7 +72,7 @@ def execute(statespace): issue.description = \ - "The function " + call.node.function_name + " in contract '" + call.node.module_name + "' contains a call to " + receiver + ".\n" \ + "The function " + call.node.function_name + " contains a call to " + receiver + ".\n" \ "The return value of this call is not checked. Note that the function will continue to execute with a return value of '0' if the called contract throws." issues.append(issue) diff --git a/mythril/analysis/modules/unchecked_suicide.py b/mythril/analysis/modules/unchecked_suicide.py index 7b4c0f7b..0443ac4b 100644 --- a/mythril/analysis/modules/unchecked_suicide.py +++ b/mythril/analysis/modules/unchecked_suicide.py @@ -28,22 +28,21 @@ def execute(statespace): logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name) - issue = Issue("Unchecked SUICIDE", "Warning") - issue.description = "The function " + node.function_name + " executes the SUICIDE instruction." + description = "The function " + node.function_name + " executes the SUICIDE instruction." state = node.states[instruction['address']] to = state.stack.pop() if ("caller" in str(to)): - issue.description += "\nThe remaining Ether is sent to the caller's address.\n" + description += "\nThe remaining Ether is sent to the caller's address.\n" elif ("storage" in str(to)): - issue.description += "\nThe remaining Ether is sent to a stored address\n" + description += "\nThe remaining Ether is sent to a stored address\n" elif ("calldata" in str(to)): - issue.description += "\nThe remaining Ether is sent to an address provided as a function argument." + description += "\nThe remaining Ether is sent to an address provided as a function argument." elif (type(to) == BitVecNumRef): - issue.description += "\nThe remaining Ether is sent to: " + hex(to.as_long()) + description += "\nThe remaining Ether is sent to: " + hex(to.as_long()) else: - issue.description += "\nThe remaining Ether is sent to: " + str(to) + "\n" + description += "\nThe remaining Ether is sent to: " + str(to) + "\n" constrained = False can_solve = True @@ -68,7 +67,7 @@ def execute(statespace): 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 + "'." + 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: @@ -90,17 +89,21 @@ def execute(statespace): if not constrained: - issue.description += "\nIt seems that this function can be called without restrictions." + description += "\nIt seems that this function can be called without restrictions." if can_solve: try: model = solver.get_model(node.constraints) logging.debug("[UNCHECKED_SUICIDE] MODEL: " + str(model)) - issues.append(issue) + for d in model.decls(): logging.debug("[UNCHECKED_SUICIDE] main model: %s = 0x%x" % (d.name(), model[d].as_long())) + + issue = Issue(node.module_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description) + issues.append(issue) + except UnsatError: logging.debug("[UNCHECKED_SUICIDE] no model found") diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index f4d24cb4..4b323600 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -1,10 +1,14 @@ class Issue: - def __init__(self, title, _type = "Informational", description = ""): + def __init__(self, contract, function, pc, title, _type="Informational", description="", debug=""): self.title = title + self.contract = contract + self.function = function + self.pc = pc self.description = description self.type = _type + self.debug = debug def as_dict(self): @@ -22,9 +26,20 @@ class Report: text = "" for issue in self.issues: - text += "=== " + issue.title + " ===\n" + text += "==== " + issue.title + " ====\n" text += "Type: " + issue.type + "\n" - text += issue.description + "\n" + + if len(issue.contract): + text += "Contract: " + issue.contract + "\n" + else: + text += "Contract: Unknown\n" + + text += "Function name: " + issue.function + "\n" + text += "PC address: " + str(issue.pc) + "\n" + + text += "--------------------\n" + issue.description + "\n" + text += "++++ Debugging info ++++\n" + issue.debug + "\n" + return text