|
|
@ -72,7 +72,7 @@ def _check_integer_overflow(statespace, state, node): |
|
|
|
if instruction['opcode'] == "ADD": |
|
|
|
if instruction['opcode'] == "ADD": |
|
|
|
expr = op0 + op1 |
|
|
|
expr = op0 + op1 |
|
|
|
else: |
|
|
|
else: |
|
|
|
expr = op0 * op1 |
|
|
|
expr = op1 * op0 |
|
|
|
|
|
|
|
|
|
|
|
# Check satisfiable |
|
|
|
# Check satisfiable |
|
|
|
constraint = Or(ULT(expr, op0), ULT(expr, op1)) |
|
|
|
constraint = Or(ULT(expr, op0), ULT(expr, op1)) |
|
|
@ -216,17 +216,20 @@ def _check_usage(state, expression): |
|
|
|
return [state] |
|
|
|
return [state] |
|
|
|
return [] |
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def _check_taint(statement, expression): |
|
|
|
def _check_taint(statement, expression): |
|
|
|
"""Checks if statement is influenced by tainted 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: |
|
|
|
if found: |
|
|
|
i = str(statement).index(str(expression)) |
|
|
|
i = _statement.index(_expression) |
|
|
|
char = str(statement)[i - 1] |
|
|
|
char = _statement[i - 1] |
|
|
|
if char == '_': |
|
|
|
if char == '_': |
|
|
|
return False |
|
|
|
return False |
|
|
|
return found |
|
|
|
return found |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def _check_jumpi(state, expression): |
|
|
|
def _check_jumpi(state, expression): |
|
|
|
""" Check if conditional jump is dependent on the result of expression""" |
|
|
|
""" Check if conditional jump is dependent on the result of expression""" |
|
|
|
logging.info(state.get_current_instruction()['opcode']) |
|
|
|
logging.info(state.get_current_instruction()['opcode']) |
|
|
@ -242,6 +245,7 @@ def _check_sstore(state, expression): |
|
|
|
value = state.mstate.stack[-2] |
|
|
|
value = state.mstate.stack[-2] |
|
|
|
return _check_taint(value, expression) |
|
|
|
return _check_taint(value, expression) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def _search_children(statespace, node, expression, index=0, depth=0, max_depth=64): |
|
|
|
def _search_children(statespace, node, expression, index=0, depth=0, max_depth=64): |
|
|
|
""" |
|
|
|
""" |
|
|
|
Checks the statespace for children states, with JUMPI or SSTORE instuctions, |
|
|
|
Checks the statespace for children states, with JUMPI or SSTORE instuctions, |
|
|
|