From 6b968ac4a5f3d7b1660248d1d34098098960156a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Apr 2018 16:44:16 +0200 Subject: [PATCH 1/8] Add constraint checking to search children function, as we only want to look at reachable children --- mythril/analysis/modules/integer.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 6e41ae29..f7d3c873 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -101,7 +101,7 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o """ Verifies existence of integer overflow """ # 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)) + interesting_usages = _search_children(statespace, node, expr, constraint=[constraint], index=node.states.index(state)) # Stop if it isn't if len(interesting_usages) == 0: @@ -246,7 +246,7 @@ def _check_sstore(state, 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, constraint=[], index=0, depth=0, max_depth=64): """ Checks the statespace for children states, with JUMPI or SSTORE instuctions, for dependency on expression @@ -273,7 +273,13 @@ def _search_children(statespace, node, expression, index=0, depth=0, max_depth=6 results += _check_usage(current_state, expression) # Recursively search children - children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid] + children = \ + [ + statespace.nodes[edge.node_to] + for edge in statespace.edges + if edge.node_from == node.uid and _try_constraints(node.constraints, constraint) + ] + for child in children: results += _search_children(statespace, child, expression, depth=depth + 1, max_depth=max_depth) From 07e07f549c9c40981538c0bf70d2de9ebe39f957 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Apr 2018 16:44:50 +0200 Subject: [PATCH 2/8] Add method that checks if an interesting state is actually caused by a requires check --- mythril/analysis/modules/integer.py | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index f7d3c873..f0ec4a7c 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -284,3 +284,22 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth results += _search_children(statespace, child, expression, depth=depth + 1, max_depth=max_depth) return results + + +def _check_requires(state, node, statespace, constraint): + """Checks if usage of overflowed statement results in a revert statement""" + instruction = state.get_current_instruction() + if instruction['opcode'] != 'JUMPI': + return False + + children = \ + [ + statespace.nodes[edge.node_to] + for edge in statespace.edges + if edge.node_from == node.uid and _try_constraints(node.constraints, [constraint]) + ] + for child in children: + opcodes = [s.get_current_instruction()['opcode'] for s in child.states] + if "REVERT" in opcodes: + return True + return False From a0b91da20afed481c77de4d612385ac46a7bb0f0 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Apr 2018 20:57:16 +0200 Subject: [PATCH 3/8] Add reacheability check and check if the expression is used in a requires statement --- mythril/analysis/modules/integer.py | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index f0ec4a7c..3b33a1b7 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -30,7 +30,7 @@ def execute(statespace): for state in node.states: logging.debug("Checking for integer underflow") - issues += _check_integer_underflow(statespace, state, node) + # issues += _check_integer_underflow(statespace, state, node) logging.debug("Checking for integer overflow") issues += _check_integer_overflow(statespace, state, node) @@ -270,14 +270,19 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth current_state = node.states[j] current_instruction = current_state.get_current_instruction() if current_instruction['opcode'] in ('JUMPI', 'SSTORE'): - results += _check_usage(current_state, expression) - - # Recursively search children + element = _check_usage(current_state, expression) + if len(element) < 1: + continue + if _check_requires(element[0], node, statespace, constraint): + continue + results += element + + # Recursively search children children = \ [ statespace.nodes[edge.node_to] for edge in statespace.edges - if edge.node_from == node.uid and _try_constraints(node.constraints, constraint) + if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None ] for child in children: @@ -289,17 +294,15 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth def _check_requires(state, node, statespace, constraint): """Checks if usage of overflowed statement results in a revert statement""" instruction = state.get_current_instruction() - if instruction['opcode'] != 'JUMPI': + if instruction['opcode'] is not "JUMPI": return False - - children = \ - [ + children = [ statespace.nodes[edge.node_to] for edge in statespace.edges - if edge.node_from == node.uid and _try_constraints(node.constraints, [constraint]) + if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None ] for child in children: opcodes = [s.get_current_instruction()['opcode'] for s in child.states] - if "REVERT" in opcodes: + if "REVERT" in opcodes or "ASSERT_FAIL" in opcodes: return True return False From 9258173b92201179eec68d86272b246c76d3ffb3 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Apr 2018 21:04:52 +0200 Subject: [PATCH 4/8] Reenable underflow check --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 3b33a1b7..988f7158 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -30,7 +30,7 @@ def execute(statespace): for state in node.states: logging.debug("Checking for integer underflow") - # issues += _check_integer_underflow(statespace, state, node) + issues += _check_integer_underflow(statespace, state, node) logging.debug("Checking for integer overflow") issues += _check_integer_overflow(statespace, state, node) From 8d109b728ff3c1092a645cf9d3423e7c17b8690c Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Apr 2018 22:07:55 +0200 Subject: [PATCH 5/8] Add len(children) check, in case we have come to the end of the analysis tree --- mythril/analysis/modules/integer.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 988f7158..48434822 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -299,10 +299,14 @@ def _check_requires(state, node, statespace, constraint): children = [ statespace.nodes[edge.node_to] for edge in statespace.edges - if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None + if edge.node_from == node.uid ] + for child in children: opcodes = [s.get_current_instruction()['opcode'] for s in child.states] if "REVERT" in opcodes or "ASSERT_FAIL" in opcodes: return True + # I added the following case, bc of false positives if the max depth is not high enough + if len(children) == 0: + return True return False From 57fae13156b63d4929302d24b4ad730a904f659a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 1 May 2018 13:54:30 +0200 Subject: [PATCH 6/8] Don't do fp detection for mul statements --- .circleci/config.yml | 2 +- mythril/analysis/modules/integer.py | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index def4ffc7..08ea558e 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -12,7 +12,7 @@ jobs: # Uncomment, for local testing with circleci command, as it ignores # path param in checkout command, and this symlink compenstates for that. - # - run: ln -s /root/project /home/mythril + - run: ln -s /root/project /home/mythril - run: name: Installing mythril tools diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 48434822..406751f3 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -82,7 +82,7 @@ def _check_integer_overflow(statespace, state, node): logging.debug("[INTEGER_OVERFLOW] no model found") return issues - if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1): + if instruction['opcode'] != "MUL" and not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1) : return issues # Build issue @@ -277,12 +277,13 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth continue results += element - # Recursively search children + # Recursively search children children = \ [ statespace.nodes[edge.node_to] for edge in statespace.edges - if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None + if edge.node_from == node.uid + and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None ] for child in children: From e87dc5c454a328b8a04a4e4453ca472445617b36 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 1 May 2018 14:02:03 +0200 Subject: [PATCH 7/8] Revert change --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 406751f3..3163e0a1 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -82,7 +82,7 @@ def _check_integer_overflow(statespace, state, node): logging.debug("[INTEGER_OVERFLOW] no model found") return issues - if instruction['opcode'] != "MUL" and not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1) : + if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1) : return issues # Build issue From 5f7418721a32be45b70c866054140e378d949a4a Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Tue, 1 May 2018 14:10:09 +0200 Subject: [PATCH 8/8] Revert change on config.yml --- .circleci/config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 08ea558e..def4ffc7 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -12,7 +12,7 @@ jobs: # Uncomment, for local testing with circleci command, as it ignores # path param in checkout command, and this symlink compenstates for that. - - run: ln -s /root/project /home/mythril + # - run: ln -s /root/project /home/mythril - run: name: Installing mythril tools