From 1ffcbe09bfc9541ae54d9499d670c9a93249b30b Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 20 Apr 2018 12:50:28 +0700 Subject: [PATCH] Integers: Add type check, change operator in assert conditions --- myth | 6 ++-- mythril/analysis/modules/integer.py | 51 ++++++++++++++++------------- 2 files changed, 31 insertions(+), 26 deletions(-) diff --git a/myth b/myth index 00b274e6..16e99a61 100755 --- a/myth +++ b/myth @@ -413,11 +413,11 @@ elif args.graph or args.fire_lasers: 'markdown': report.as_markdown() or "The analysis was completed successfully. No issues were detected." } print(outputs[args.outform]) - -elif args.statespace_json: + +elif args.statespace_json: if not contracts: exitWithError(args.outform, "input files do not contain any valid contracts") - + if args.dynld: sym = SymExecWrapper(contracts[0], address, dynloader=DynLoader(eth), max_depth=args.max_depth) else: diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index d4528af6..7892af97 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -62,33 +62,37 @@ def _check_integer_overflow(statespace, state, node): # An integer overflow is possible if op0 + op1 or op0 * op1 > MAX_UINT - if instruction['opcode'] == "ADD": - expr = op0 + op1 - else: - expr = op0 * op1 + allowed_types = [int, BitVecRef, BitVecNumRef] - constraints.append(UGT(expr, MAX_UINT)) + if type(op0) in allowed_types and type(op1) in allowed_types: - try: - model = solver.get_model(constraints) + if instruction['opcode'] == "ADD": + expr = op0 + op1 + else: + expr = op0 * op1 - # If we get to this point then there has been an integer overflow - # Find out if the overflowed value is actually used - interesting_usages = _search_children(statespace, node, expr, index=node.states.index(state)) + constraints.append(UGT(expr, MAX_UINT)) - # Stop if it isn't - if len(interesting_usages) == 0: - return issues + try: + model = solver.get_model(constraints) - issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning") + # If we get to this point then there has been an integer overflow + # Find out if the overflowed value is actually used + interesting_usages = _search_children(statespace, node, expr, index=node.states.index(state)) - issue.description = "A possible integer overflow exists in the function `{}`.\n" \ - "The addition or multiplication may result in a value higher than the maximum representable integer.".format(node.function_name) - issue.debug = solver.pretty_print_model(model) - issues.append(issue) + # Stop if it isn't + if len(interesting_usages) == 0: + return issues + + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning") - except UnsatError: - logging.debug("[INTEGER_OVERFLOW] no model found") + issue.description = "A possible integer overflow exists in the function `{}`.\n" \ + "The addition or multiplication may result in a value higher than the maximum representable integer.".format(node.function_name) + issue.debug = solver.pretty_print_model(model) + issues.append(issue) + + except UnsatError: + logging.debug("[INTEGER_OVERFLOW] no model found") return issues @@ -127,7 +131,6 @@ def _check_integer_underflow(statespace, state, node): logging.debug("[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(str(op0), str(op1), str(instruction['address']))) - allowed_types = [int, BitVecRef, BitVecNumRef] if type(op0) in allowed_types and type(op1) in allowed_types: @@ -175,14 +178,16 @@ def _check_usage(state, expression): def _check_jumpi(state, expression): """ Check if conditional jump is dependent on the result of expression""" - assert state.get_current_instruction()['opcode'] is 'JUMPI' + logging.info(state.get_current_instruction()['opcode']) + assert state.get_current_instruction()['opcode'] == 'JUMPI' condition = state.mstate.stack[-2] return str(expression) in str(condition) def _check_sstore(state, expression): """ Check if store operation is dependent on the result of expression""" - assert state.get_current_instruction()['opcode'] is 'SSTORE' + logging.info(state.get_current_instruction()['opcode']) + assert state.get_current_instruction()['opcode'] == 'SSTORE' value = state.mstate.stack[-2] return str(expression) in str(value)