From d29159e212d7566558820589e11d1d3cba568b17 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 12 Feb 2019 18:10:33 +0530 Subject: [PATCH 01/15] Find issues for EXP operation --- mythril/analysis/modules/integer.py | 92 ++++++++++++-------- mythril/laser/ethereum/instructions.py | 8 +- mythril/laser/ethereum/state/global_state.py | 6 +- 3 files changed, 66 insertions(+), 40 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 7df300ec..2bffe802 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -2,6 +2,8 @@ underflows.""" import json + +from math import log2, ceil from typing import Dict, cast, List from mythril.analysis import solver from mythril.analysis.report import Issue @@ -31,22 +33,22 @@ class OverUnderflowAnnotation: """ Symbol Annotation used if a BitVector can overflow""" def __init__( - self, overflowing_state: GlobalState, operator: str, constraint + self, overflowing_state: GlobalState, operator: str, constraints ) -> None: self.overflowing_state = overflowing_state self.operator = operator - self.constraint = constraint + self.constraints = constraints class OverUnderflowStateAnnotation(StateAnnotation): """ State Annotation used if an overflow is both possible and used in the annotated path""" def __init__( - self, overflowing_state: GlobalState, operator: str, constraint + self, overflowing_state: GlobalState, operator: str, constraints ) -> None: self.overflowing_state = overflowing_state self.operator = operator - self.constraint = constraint + self.constraints = constraints class IntegerOverflowUnderflowModule(DetectionModule): @@ -63,7 +65,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): "there's a possible state where op1 + op0 > 2^32 - 1" ), entrypoint="callback", - pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"], + pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"], ) self._overflow_cache = {} # type: Dict[int, bool] self._underflow_cache = {} # type: Dict[int, bool] @@ -88,25 +90,29 @@ class IntegerOverflowUnderflowModule(DetectionModule): has_underflow = self._underflow_cache.get(address, False) if has_overflow or has_underflow: return - if state.get_current_instruction()["opcode"] == "ADD": - self._handle_add(state) - elif state.get_current_instruction()["opcode"] == "MUL": - self._handle_mul(state) - elif state.get_current_instruction()["opcode"] == "SUB": - self._handle_sub(state) - elif state.get_current_instruction()["opcode"] == "SSTORE": - self._handle_sstore(state) - elif state.get_current_instruction()["opcode"] == "JUMPI": - self._handle_jumpi(state) - elif state.get_current_instruction()["opcode"] in ("RETURN", "STOP"): - self._handle_transaction_end(state) - - def _handle_add(self, state): + opcode = state.get_current_instruction()["opcode"] + func = { + "ADD": self._handle_add, + "SUB": self._handle_sub, + "MUL": self._handle_mul, + "SSTORE": self._handle_sstore, + "JUMPI": self._handle_jumpi, + "RETURN": self._handle_transaction_end, + "STOP": self._handle_transaction_end, + "EXP": self._handle_exp, + } + func[opcode](state) + + def _get_args(self, state): stack = state.mstate.stack op0, op1 = ( self._make_bitvec_if_not(stack, -1), self._make_bitvec_if_not(stack, -2), ) + return op0, op1 + + def _handle_add(self, state): + op0, op1 = self._get_args(state) c = Not(BVAddNoOverflow(op0, op1, False)) # Check satisfiable @@ -114,16 +120,11 @@ class IntegerOverflowUnderflowModule(DetectionModule): if model is None: return - annotation = OverUnderflowAnnotation(state, "addition", c) + annotation = OverUnderflowAnnotation(state, "addition", [c]) op0.annotate(annotation) def _handle_mul(self, state): - stack = state.mstate.stack - op0, op1 = ( - self._make_bitvec_if_not(stack, -1), - self._make_bitvec_if_not(stack, -2), - ) - + op0, op1 = self._get_args(state) c = Not(BVMulNoOverflow(op0, op1, False)) # Check satisfiable @@ -131,15 +132,11 @@ class IntegerOverflowUnderflowModule(DetectionModule): if model is None: return - annotation = OverUnderflowAnnotation(state, "multiplication", c) + annotation = OverUnderflowAnnotation(state, "multiplication", [c]) op0.annotate(annotation) def _handle_sub(self, state): - stack = state.mstate.stack - op0, op1 = ( - self._make_bitvec_if_not(stack, -1), - self._make_bitvec_if_not(stack, -2), - ) + op0, op1 = self._get_args(state) c = Not(BVSubNoUnderflow(op0, op1, False)) # Check satisfiable @@ -147,7 +144,29 @@ class IntegerOverflowUnderflowModule(DetectionModule): if model is None: return - annotation = OverUnderflowAnnotation(state, "subtraction", c) + annotation = OverUnderflowAnnotation(state, "subtraction", [c]) + op0.annotate(annotation) + + def _handle_exp(self, state): + op0, op1 = self._get_args(state) + if op0.symbolic and op1.symbolic: + c1, c2 = ( + op1 > symbol_factory.BitVecVal(256, 256), + op0 > symbol_factory.BitVecVal(1, 256), + ) + constraints = [c1, c2] + elif op1.symbolic: + c1 = op1 > symbol_factory.BitVecVal(256 // log2(op0.value), 256) + constraints = [c1] + elif op0.symbolic: + c1 = op0 > 2 ** symbol_factory.BitVecVal(ceil(256 / op1.value), 256) + constraints = [c1] + else: + constraints = [op0.value ** op1.value > 2 ** 256] + model = self._try_constraints(state.node.constraints, constraints) + if model is None: + return + annotation = OverUnderflowAnnotation(state, "exponentiation", constraints) op0.annotate(annotation) @staticmethod @@ -185,7 +204,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): def _handle_sstore(state: GlobalState) -> None: stack = state.mstate.stack value = stack[-2] - if not isinstance(value, Expression): return for annotation in value.annotations: @@ -195,7 +213,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): OverUnderflowStateAnnotation( annotation.overflowing_state, annotation.operator, - annotation.constraint, + annotation.constraints, ) ) @@ -211,7 +229,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): OverUnderflowStateAnnotation( annotation.overflowing_state, annotation.operator, - annotation.constraint, + annotation.constraints, ) ) @@ -253,7 +271,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): try: transaction_sequence = solver.get_transaction_sequence( - state, node.constraints + [annotation.constraint] + state, node.constraints + annotation.constraints ) issue.debug = json.dumps(transaction_sequence, indent=4) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 72d17e5d..dee8fcba 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -519,16 +519,22 @@ class Instruction: base, exponent = util.pop_bitvec(state), util.pop_bitvec(state) if base.symbolic or exponent.symbolic: + state.stack.append( global_state.new_bitvec( "(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256, + base.annotations + exponent.annotations, ) ) else: state.stack.append( - symbol_factory.BitVecVal(pow(base.value, exponent.value, 2 ** 256), 256) + symbol_factory.BitVecVal( + pow(base.value, exponent.value, 2 ** 256), + 256, + annotations=base.annotations + exponent.annotations, + ) ) return [global_state] diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index aa931606..5423aaf8 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -111,7 +111,7 @@ class GlobalState: """ return self.get_current_instruction() - def new_bitvec(self, name: str, size=256) -> BitVec: + def new_bitvec(self, name: str, size=256, annotations=None) -> BitVec: """ :param name: @@ -119,7 +119,9 @@ class GlobalState: :return: """ transaction_id = self.current_transaction.id - return symbol_factory.BitVecSym("{}_{}".format(transaction_id, name), size) + return symbol_factory.BitVecSym( + "{}_{}".format(transaction_id, name), size, annotations=annotations + ) def annotate(self, annotation: StateAnnotation) -> None: """ From 5d72c29b99cc690eb6212c219954d4c7bfd6b998 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 12 Feb 2019 18:36:22 +0530 Subject: [PATCH 02/15] Fix the case for symbol ** const --- 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 2bffe802..d53044db 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -159,7 +159,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): c1 = op1 > symbol_factory.BitVecVal(256 // log2(op0.value), 256) constraints = [c1] elif op0.symbolic: - c1 = op0 > 2 ** symbol_factory.BitVecVal(ceil(256 / op1.value), 256) + c1 = op0 > symbol_factory.BitVecVal(2 ** ceil(256 / op1.value), 256) constraints = [c1] else: constraints = [op0.value ** op1.value > 2 ** 256] From e6999766d94c8f82e2b22b21fbcefb50235f7a92 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 12 Feb 2019 20:33:12 +0530 Subject: [PATCH 03/15] add = cases --- mythril/analysis/modules/integer.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index d53044db..3379e313 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -156,10 +156,10 @@ class IntegerOverflowUnderflowModule(DetectionModule): ) constraints = [c1, c2] elif op1.symbolic: - c1 = op1 > symbol_factory.BitVecVal(256 // log2(op0.value), 256) + c1 = op1 >= symbol_factory.BitVecVal(ceil(256 / log2(op0.value)), 256) constraints = [c1] elif op0.symbolic: - c1 = op0 > symbol_factory.BitVecVal(2 ** ceil(256 / op1.value), 256) + c1 = op0 >= symbol_factory.BitVecVal(2 ** ceil(256 / op1.value), 256) constraints = [c1] else: constraints = [op0.value ** op1.value > 2 ** 256] From 089aa799bff9bb7254084c586229b5547de6a56a Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Fri, 15 Feb 2019 08:31:37 +0530 Subject: [PATCH 04/15] Update mythril/analysis/modules/integer.py Co-Authored-By: norhh --- 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 3379e313..a3c2f500 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -162,7 +162,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): c1 = op0 >= symbol_factory.BitVecVal(2 ** ceil(256 / op1.value), 256) constraints = [c1] else: - constraints = [op0.value ** op1.value > 2 ** 256] + constraints = [op0.value ** op1.value >= 2 ** 256] model = self._try_constraints(state.node.constraints, constraints) if model is None: return From 28960665c29fe00928d372bcab3926b7b06eb431 Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Fri, 15 Feb 2019 09:41:18 +0530 Subject: [PATCH 05/15] Update mythril/analysis/modules/integer.py Co-Authored-By: norhh --- 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 a3c2f500..b4905dac 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -150,7 +150,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): def _handle_exp(self, state): op0, op1 = self._get_args(state) if op0.symbolic and op1.symbolic: - c1, c2 = ( + constraint = And( op1 > symbol_factory.BitVecVal(256, 256), op0 > symbol_factory.BitVecVal(1, 256), ) From a362f39e6f435bcc5b2dbefa3b06cf12b03569b8 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 15 Feb 2019 14:06:17 +0530 Subject: [PATCH 06/15] Revert the use of constraints list --- mythril/analysis/modules/integer.py | 38 +++++++++++++++-------------- 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index b4905dac..7e62975b 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -21,6 +21,7 @@ from mythril.laser.smt import ( symbol_factory, Not, Expression, + Bool, ) import logging @@ -33,22 +34,22 @@ class OverUnderflowAnnotation: """ Symbol Annotation used if a BitVector can overflow""" def __init__( - self, overflowing_state: GlobalState, operator: str, constraints + self, overflowing_state: GlobalState, operator: str, constraint: Bool ) -> None: self.overflowing_state = overflowing_state self.operator = operator - self.constraints = constraints + self.constraint = constraint class OverUnderflowStateAnnotation(StateAnnotation): """ State Annotation used if an overflow is both possible and used in the annotated path""" def __init__( - self, overflowing_state: GlobalState, operator: str, constraints + self, overflowing_state: GlobalState, operator: str, constraint: Bool ) -> None: self.overflowing_state = overflowing_state self.operator = operator - self.constraints = constraints + self.constraint = constraint class IntegerOverflowUnderflowModule(DetectionModule): @@ -120,7 +121,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): if model is None: return - annotation = OverUnderflowAnnotation(state, "addition", [c]) + annotation = OverUnderflowAnnotation(state, "addition", c) op0.annotate(annotation) def _handle_mul(self, state): @@ -132,7 +133,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): if model is None: return - annotation = OverUnderflowAnnotation(state, "multiplication", [c]) + annotation = OverUnderflowAnnotation(state, "multiplication", c) op0.annotate(annotation) def _handle_sub(self, state): @@ -144,7 +145,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): if model is None: return - annotation = OverUnderflowAnnotation(state, "subtraction", [c]) + annotation = OverUnderflowAnnotation(state, "subtraction", c) op0.annotate(annotation) def _handle_exp(self, state): @@ -154,19 +155,20 @@ class IntegerOverflowUnderflowModule(DetectionModule): op1 > symbol_factory.BitVecVal(256, 256), op0 > symbol_factory.BitVecVal(1, 256), ) - constraints = [c1, c2] elif op1.symbolic: - c1 = op1 >= symbol_factory.BitVecVal(ceil(256 / log2(op0.value)), 256) - constraints = [c1] + constraint = op1 >= symbol_factory.BitVecVal( + ceil(256 / log2(op0.value)), 256 + ) elif op0.symbolic: - c1 = op0 >= symbol_factory.BitVecVal(2 ** ceil(256 / op1.value), 256) - constraints = [c1] + constraint = op0 >= symbol_factory.BitVecVal( + 2 ** ceil(256 / op1.value), 256 + ) else: - constraints = [op0.value ** op1.value >= 2 ** 256] - model = self._try_constraints(state.node.constraints, constraints) + constraint = op0.value ** op1.value >= 2 ** 256 + model = self._try_constraints(state.node.constraints, [constraint]) if model is None: return - annotation = OverUnderflowAnnotation(state, "exponentiation", constraints) + annotation = OverUnderflowAnnotation(state, "exponentiation", constraint) op0.annotate(annotation) @staticmethod @@ -213,7 +215,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): OverUnderflowStateAnnotation( annotation.overflowing_state, annotation.operator, - annotation.constraints, + annotation.constraint, ) ) @@ -229,7 +231,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): OverUnderflowStateAnnotation( annotation.overflowing_state, annotation.operator, - annotation.constraints, + annotation.constraint, ) ) @@ -271,7 +273,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): try: transaction_sequence = solver.get_transaction_sequence( - state, node.constraints + annotation.constraints + state, node.constraints + [annotation.constraint] ) issue.debug = json.dumps(transaction_sequence, indent=4) From 8fe9b7ae81642d1fad9bd0fe9a44c566149d7e86 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 19 Feb 2019 20:46:57 +0530 Subject: [PATCH 07/15] Handle edge case for exp --- mythril/analysis/modules/integer.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 7e62975b..c57343f4 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -22,6 +22,7 @@ from mythril.laser.smt import ( Not, Expression, Bool, + And, ) import logging @@ -156,10 +157,14 @@ class IntegerOverflowUnderflowModule(DetectionModule): op0 > symbol_factory.BitVecVal(1, 256), ) elif op1.symbolic: + if op0.value < 2: + return constraint = op1 >= symbol_factory.BitVecVal( ceil(256 / log2(op0.value)), 256 ) elif op0.symbolic: + if op1.value == 0: + return constraint = op0 >= symbol_factory.BitVecVal( 2 ** ceil(256 / op1.value), 256 ) From fd2436ddb7d0a3b0305a66d311ee8bc0c90fc3d0 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sun, 24 Feb 2019 16:55:48 +0530 Subject: [PATCH 08/15] handle for integer module --- mythril/analysis/modules/integer.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 7df300ec..5c5d1adf 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -8,6 +8,7 @@ from mythril.analysis.report import Issue from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.util import get_concrete_int from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.analysis.modules.base import DetectionModule @@ -99,6 +100,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): elif state.get_current_instruction()["opcode"] == "JUMPI": self._handle_jumpi(state) elif state.get_current_instruction()["opcode"] in ("RETURN", "STOP"): + if state.get_current_instruction()["opcode"] == "RETURN": + self._handle_return(state) self._handle_transaction_end(state) def _handle_add(self, state): @@ -215,6 +218,25 @@ class IntegerOverflowUnderflowModule(DetectionModule): ) ) + @staticmethod + def _handle_return(state: GlobalState) -> None: + stack = state.mstate.stack + try: + offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2]) + except TypeError: + return + for element in state.mstate.memory[offset : offset + length]: + if isinstance(element, Expression): + for annotation in element.annotations: + if isinstance(annotation, OverUnderflowAnnotation): + state.annotate( + OverUnderflowStateAnnotation( + annotation.overflowing_state, + annotation.operator, + annotation.constraint, + ) + ) + def _handle_transaction_end(self, state: GlobalState) -> None: for annotation in cast( List[OverUnderflowStateAnnotation], From 2e1f1fd5d2d61a9c7638aff9dc2162a2a1031c7a Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 25 Feb 2019 15:03:10 +0530 Subject: [PATCH 09/15] Add documentation for _handle_return function --- mythril/analysis/modules/integer.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 5c5d1adf..3c39d144 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -220,6 +220,11 @@ class IntegerOverflowUnderflowModule(DetectionModule): @staticmethod def _handle_return(state: GlobalState) -> None: + """ + Adds all the annotations into the state which correspond to the + locations in the memory returned by RETURN opcode. + :param state: The Global State + """ stack = state.mstate.stack try: offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2]) From 19b8d9092f39c950c10ac72ca1f5f612047f6430 Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Mon, 25 Feb 2019 18:01:21 +0530 Subject: [PATCH 10/15] Update mythril/analysis/modules/integer.py Co-Authored-By: norhh --- mythril/analysis/modules/integer.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 3c39d144..22418123 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -231,7 +231,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): except TypeError: return for element in state.mstate.memory[offset : offset + length]: - if isinstance(element, Expression): + if not isinstance(element, Expression): + return for annotation in element.annotations: if isinstance(annotation, OverUnderflowAnnotation): state.annotate( From 6d03ef353616a42239bea0f6ebcc074624dda03b Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 25 Feb 2019 18:54:02 +0530 Subject: [PATCH 11/15] Fix the indentation --- mythril/analysis/modules/integer.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 22418123..e811551c 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -233,15 +233,15 @@ class IntegerOverflowUnderflowModule(DetectionModule): for element in state.mstate.memory[offset : offset + length]: if not isinstance(element, Expression): return - for annotation in element.annotations: - if isinstance(annotation, OverUnderflowAnnotation): - state.annotate( - OverUnderflowStateAnnotation( - annotation.overflowing_state, - annotation.operator, - annotation.constraint, - ) + for annotation in element.annotations: + if isinstance(annotation, OverUnderflowAnnotation): + state.annotate( + OverUnderflowStateAnnotation( + annotation.overflowing_state, + annotation.operator, + annotation.constraint, ) + ) def _handle_transaction_end(self, state: GlobalState) -> None: for annotation in cast( From 99ca850baf572fdc5ce6d0a52df1b1b7cf0a2221 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 28 Feb 2019 02:07:07 +0530 Subject: [PATCH 12/15] Add the discovery time to Issue class --- mythril/analysis/modules/integer.py | 36 ++++++++++++++--------------- mythril/analysis/report.py | 25 +++++++++++--------- mythril/mythril.py | 3 +++ mythril/start_time.py | 7 ++++++ 4 files changed, 41 insertions(+), 30 deletions(-) create mode 100644 mythril/start_time.py diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 7df300ec..db5eb6b8 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -222,22 +222,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): ): ostate = annotation.overflowing_state - node = ostate.node - - _type = "Underflow" if annotation.operator == "subtraction" else "Overflow" - issue = Issue( - contract=node.contract_name, - function_name=node.function_name, - address=ostate.get_current_instruction()["address"], - swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW, - bytecode=ostate.environment.code.bytecode, - title=self._get_title(_type), - severity="High", - description_head=self._get_description_head(annotation, _type), - description_tail=self._get_description_tail(annotation, _type), - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - ) - address = _get_address_from_state(ostate) if annotation.operator == "subtraction" and self._underflow_cache.get( @@ -250,17 +234,31 @@ class IntegerOverflowUnderflowModule(DetectionModule): ): continue + node = ostate.node try: transaction_sequence = solver.get_transaction_sequence( state, node.constraints + [annotation.constraint] ) - - issue.debug = json.dumps(transaction_sequence, indent=4) - except UnsatError: continue + _type = "Underflow" if annotation.operator == "subtraction" else "Overflow" + issue = Issue( + contract=node.contract_name, + function_name=node.function_name, + address=ostate.get_current_instruction()["address"], + swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW, + bytecode=ostate.environment.code.bytecode, + title=self._get_title(_type), + severity="High", + description_head=self._get_description_head(annotation, _type), + description_tail=self._get_description_tail(annotation, _type), + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + ) + + issue.debug = json.dumps(transaction_sequence, indent=4) + if annotation.operator == "subtraction": self._underflow_cache[address] = True else: diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index 075dbdb1..b8a9faf1 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -9,7 +9,8 @@ import hashlib from mythril.solidity.soliditycontract import SolidityContract from mythril.analysis.swc_data import SWC_TO_TITLE from mythril.support.source_support import Source - +from mythril.start_time import StartTime +from time import time log = logging.getLogger(__name__) @@ -33,16 +34,17 @@ class Issue: ): """ - :param contract: - :param function_name: - :param address: - :param swc_id: - :param title: - :param bytecode: - :param gas_used: - :param _type: - :param description: - :param debug: + :param contract: The contract + :param function_name: Function name where the issue is detected + :param address: The address of the issue + :param swc_id: Issue's corresponding swc-id + :param title: Title + :param bytecode: bytecode of the issue + :param gas_used: amount of gas used + :param severity: The severity of the issue + :param description_head: The top part of description + :param description_tail: The bottom part of the description + :param debug: The transaction sequence """ self.title = title self.contract = contract @@ -59,6 +61,7 @@ class Issue: self.code = None self.lineno = None self.source_mapping = None + self.discovery_time = time() - StartTime().global_start_time try: keccak = sha3.keccak_256() diff --git a/mythril/mythril.py b/mythril/mythril.py index 2f082ba0..507cd920 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -36,8 +36,11 @@ from mythril.analysis.report import Report from mythril.support.truffle import analyze_truffle_project from mythril.ethereum.interface.leveldb.client import EthLevelDB from mythril.laser.smt import SolverStatistics +from mythril.start_time import StartTime + log = logging.getLogger(__name__) +start_time = StartTime() class Mythril(object): diff --git a/mythril/start_time.py b/mythril/start_time.py new file mode 100644 index 00000000..4e86326e --- /dev/null +++ b/mythril/start_time.py @@ -0,0 +1,7 @@ +from time import time +from mythril.support.support_utils import Singleton + + +class StartTime(metaclass=Singleton): + def __init__(self): + self.global_start_time = time() From e1c29a1c8321abb02a596bc6a928cfdb8c08b3da Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 1 Mar 2019 18:50:13 +0530 Subject: [PATCH 13/15] Fix address length and mstore8_ opcode --- mythril/laser/ethereum/instructions.py | 2 +- mythril/laser/ethereum/state/world_state.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 79ab0749..a99fd982 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1296,7 +1296,7 @@ class Instruction: try: value_to_write = ( - util.get_concrete_int(value) ^ 0xFF + util.get_concrete_int(value) % 256 ) # type: Union[int, BitVec] except TypeError: # BitVec value_to_write = Extract(7, 0, value) diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 9b5bdcaa..9e616934 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -117,7 +117,7 @@ class WorldState: :return: """ while True: - address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(20)]) + address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(40)]) if address not in self.accounts.keys(): return address From 0ed11a2bf210220970c73f37bbb8eeeb27cc2500 Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Mon, 4 Mar 2019 19:10:03 +0530 Subject: [PATCH 14/15] Update mythril/analysis/modules/integer.py Co-Authored-By: norhh --- 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 e811551c..13b6d6c8 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -232,7 +232,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): return for element in state.mstate.memory[offset : offset + length]: if not isinstance(element, Expression): - return + continue for annotation in element.annotations: if isinstance(annotation, OverUnderflowAnnotation): state.annotate( From 84d5c8652e73965c4f57e6760228d46e2a9e7946 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 6 Mar 2019 02:00:17 +0530 Subject: [PATCH 15/15] Move start_time.py to support and reinitialize the start_time to every contract --- mythril/analysis/report.py | 2 +- mythril/mythril.py | 4 ++-- mythril/{ => support}/start_time.py | 2 ++ 3 files changed, 5 insertions(+), 3 deletions(-) rename mythril/{ => support}/start_time.py (70%) diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index b8a9faf1..46795b8d 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -9,7 +9,7 @@ import hashlib from mythril.solidity.soliditycontract import SolidityContract from mythril.analysis.swc_data import SWC_TO_TITLE from mythril.support.source_support import Source -from mythril.start_time import StartTime +from mythril.support.start_time import StartTime from time import time log = logging.getLogger(__name__) diff --git a/mythril/mythril.py b/mythril/mythril.py index 507cd920..4654b235 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -36,11 +36,10 @@ from mythril.analysis.report import Report from mythril.support.truffle import analyze_truffle_project from mythril.ethereum.interface.leveldb.client import EthLevelDB from mythril.laser.smt import SolverStatistics -from mythril.start_time import StartTime +from mythril.support.start_time import StartTime log = logging.getLogger(__name__) -start_time = StartTime() class Mythril(object): @@ -572,6 +571,7 @@ class Mythril(object): all_issues = [] SolverStatistics().enabled = True for contract in contracts or self.contracts: + StartTime() # Reinitialize start time for new contracts try: sym = SymExecWrapper( contract, diff --git a/mythril/start_time.py b/mythril/support/start_time.py similarity index 70% rename from mythril/start_time.py rename to mythril/support/start_time.py index 4e86326e..52b6714f 100644 --- a/mythril/start_time.py +++ b/mythril/support/start_time.py @@ -3,5 +3,7 @@ from mythril.support.support_utils import Singleton class StartTime(metaclass=Singleton): + """Maintains the start time of the current contract in execution""" + def __init__(self): self.global_start_time = time()