Improve reporting

pull/30/head
Bernhard Mueller 7 years ago
parent 2a8dd80c97
commit 7b3c152844
  1. 14
      mythril/analysis/modules/call_to_dynamic_with_gas.py
  2. 3
      mythril/analysis/modules/delegatecall_forward.py
  3. 10
      mythril/analysis/modules/delegatecall_to_dynamic.py
  4. 33
      mythril/analysis/modules/ether_send.py
  5. 10
      mythril/analysis/modules/integer_underflow.py
  6. 11
      mythril/analysis/modules/unchecked_retval.py
  7. 23
      mythril/analysis/modules/unchecked_suicide.py
  8. 21
      mythril/analysis/report.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)

@ -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"

@ -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." \

@ -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,20 +91,21 @@ 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")

@ -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)

@ -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)

@ -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")

@ -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

Loading…
Cancel
Save