From c36afcc487a00c54dfdc8a9962b4ec4459fcd0d8 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sun, 29 Apr 2018 11:40:51 +0200 Subject: [PATCH] Remove spaces from check taint ( as these can mess with taint checking ). And swap op0 and op1 as it seems that z3 does this as well --- mythril/analysis/modules/integer.py | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index abe9dece..8cdf2ab0 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -72,7 +72,7 @@ def _check_integer_overflow(statespace, state, node): if instruction['opcode'] == "ADD": expr = op0 + op1 else: - expr = op0 * op1 + expr = op1 * op0 # Check satisfiable constraint = Or(ULT(expr, op0), ULT(expr, op1)) @@ -216,17 +216,20 @@ def _check_usage(state, expression): return [state] return [] + def _check_taint(statement, expression): """Checks if statement is influenced by tainted expression""" - found = str(expression) in str(statement) + _expression, _statement = str(expression).replace(' ', ''), str(statement).replace(' ', '') + found = _expression in _statement if found: - i = str(statement).index(str(expression)) - char = str(statement)[i - 1] + i = _statement.index(_expression) + char = _statement[i - 1] if char == '_': return False return found + def _check_jumpi(state, expression): """ Check if conditional jump is dependent on the result of expression""" logging.info(state.get_current_instruction()['opcode']) @@ -242,6 +245,7 @@ def _check_sstore(state, expression): value = state.mstate.stack[-2] return _check_taint(value, expression) + def _search_children(statespace, node, expression, index=0, depth=0, max_depth=64): """ Checks the statespace for children states, with JUMPI or SSTORE instuctions,