From 1b73ddec1293f1d1e2f22396bf189b187f61b3a9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 12 Jun 2019 09:53:59 +0200 Subject: [PATCH 1/4] Norhh suggestion + some refactoring --- mythril/analysis/modules/integer.py | 64 +++++++++++------------------ 1 file changed, 24 insertions(+), 40 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index ac825904..13d2eaa3 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -222,16 +222,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): if not isinstance(value, Expression): return - state_annotations = cast( - List[OverUnderflowStateAnnotation], - list(state.get_annotations(OverUnderflowStateAnnotation)), - ) - - if len(state_annotations) == 0: - state_annotation = OverUnderflowStateAnnotation() - state.annotate(state_annotation) - else: - state_annotation = state_annotations[0] + state_annotation = _get_overflowunderflow_state_annotation(state) for annotation in value.annotations: if ( @@ -249,16 +240,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): stack = state.mstate.stack value = stack[-2] - state_annotations = cast( - List[OverUnderflowStateAnnotation], - list(state.get_annotations(OverUnderflowStateAnnotation)), - ) - - if len(state_annotations) == 0: - state_annotation = OverUnderflowStateAnnotation() - state.annotate(state_annotation) - else: - state_annotation = state_annotations[0] + state_annotation = _get_overflowunderflow_state_annotation(state) for annotation in value.annotations: if ( @@ -283,35 +265,21 @@ class IntegerOverflowUnderflowModule(DetectionModule): except TypeError: return - """ TODO: Rewrite this for element in state.mstate.memory[offset : offset + length]: if not isinstance(element, Expression): continue + + state_annotation = _get_overflowunderflow_state_annotation(state) + for annotation in element.annotations: if isinstance(annotation, OverUnderflowAnnotation): - - state.annotate( - OverUnderflowStateAnnotation( - annotation.overflowing_state, - annotation.operator, - annotation.constraint, - ) - ) - """ + state_annotation.overflowing_state_annotations.append(annotation) def _handle_transaction_end(self, state: GlobalState) -> None: - state_annotations = cast( - List[OverUnderflowStateAnnotation], - list(state.get_annotations(OverUnderflowStateAnnotation)), - ) - - if len(state_annotations) == 0: - return + state_annotation = _get_overflowunderflow_state_annotation(state) - annotations = state_annotations[0].overflowing_state_annotations - - for annotation in annotations: + for annotation in state_annotation.overflowing_state_annotations: ostate = annotation.overflowing_state @@ -371,3 +339,19 @@ detector = IntegerOverflowUnderflowModule() def _get_address_from_state(state): return state.get_current_instruction()["address"] + + +def _get_overflowunderflow_state_annotation( + state: GlobalState +) -> OverUnderflowStateAnnotation: + state_annotations = cast( + List[OverUnderflowStateAnnotation], + list(state.get_annotations(OverUnderflowStateAnnotation)), + ) + + if len(state_annotations) == 0: + state_annotation = OverUnderflowStateAnnotation() + state.annotate(state_annotation) + return state_annotation + else: + return state_annotations[0] From 58cf0c6efc5d72f2061e705b571bfa1c89dad18e Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 12 Jun 2019 10:00:51 +0200 Subject: [PATCH 2/4] Comment out the handle_return code again --- mythril/analysis/modules/integer.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 13d2eaa3..46b5b70a 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -258,23 +258,27 @@ class IntegerOverflowUnderflowModule(DetectionModule): 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]) except TypeError: return + state_annotation = _get_overflowunderflow_state_annotation(state) + for element in state.mstate.memory[offset : offset + length]: + if not isinstance(element, Expression): continue - state_annotation = _get_overflowunderflow_state_annotation(state) - for annotation in element.annotations: if isinstance(annotation, OverUnderflowAnnotation): state_annotation.overflowing_state_annotations.append(annotation) + """ + def _handle_transaction_end(self, state: GlobalState) -> None: state_annotation = _get_overflowunderflow_state_annotation(state) From a15d38c8b2790ef682f3df76a72bda4de892c6ea Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 12 Jun 2019 10:14:04 +0200 Subject: [PATCH 3/4] Fix processing of return, change lists to sets --- mythril/analysis/modules/integer.py | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 46b5b70a..24db48e2 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -48,7 +48,7 @@ class OverUnderflowStateAnnotation(StateAnnotation): def __init__(self) -> None: self.overflowing_state_annotations = [] # type: List[OverUnderflowAnnotation] - self.ostates_seen = [] # type: List[GlobalState] + self.ostates_seen = set() # type: List[GlobalState] def __copy__(self): new_annotation = OverUnderflowStateAnnotation() @@ -88,8 +88,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): Cache satisfiability of overflow constraints """ - self._ostates_satisfiable = [] # type: List[GlobalState] - self._ostates_unsatisfiable = [] # type: List[GlobalState] + self._ostates_satisfiable = set() + self._ostates_unsatisfiable = set() def reset_module(self): """ @@ -98,8 +98,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): """ super().reset_module() self._overflow_cache = {} - self._ostates_satisfiable = [] - self._ostates_unsatisfiable = [] + self._ostates_satisfiable = set() + self._ostates_unsatisfiable = set() def _execute(self, state: GlobalState) -> None: """Executes analysis module for integer underflow and integer overflow. @@ -232,7 +232,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): continue state_annotation.overflowing_state_annotations.append(annotation) - state_annotation.ostates_seen.append(annotation.overflowing_state) + state_annotation.ostates_seen.add(annotation.overflowing_state) @staticmethod def _handle_jumpi(state): @@ -250,7 +250,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): continue state_annotation.overflowing_state_annotations.append(annotation) - state_annotation.ostates_seen.append(annotation.overflowing_state) + state_annotation.ostates_seen.add(annotation.overflowing_state) @staticmethod def _handle_return(state: GlobalState) -> None: @@ -258,7 +258,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): 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: @@ -274,11 +274,12 @@ class IntegerOverflowUnderflowModule(DetectionModule): continue for annotation in element.annotations: - if isinstance(annotation, OverUnderflowAnnotation): + if ( + isinstance(annotation, OverUnderflowAnnotation) + and annotation not in state_annotation.overflowing_state_annotations + ): state_annotation.overflowing_state_annotations.append(annotation) - """ - def _handle_transaction_end(self, state: GlobalState) -> None: state_annotation = _get_overflowunderflow_state_annotation(state) @@ -294,9 +295,9 @@ class IntegerOverflowUnderflowModule(DetectionModule): try: constraints = ostate.mstate.constraints + [annotation.constraint] solver.get_model(constraints) - self._ostates_satisfiable.append(ostate) + self._ostates_satisfiable.add(ostate) except: - self._ostates_unsatisfiable.append(ostate) + self._ostates_unsatisfiable.add(ostate) continue log.debug( From 1faaf2a21dc7c02e2b4205cbfdd992b591998413 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 12 Jun 2019 10:15:36 +0200 Subject: [PATCH 4/4] Update comment --- 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 24db48e2..2c849a79 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -79,7 +79,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): ) """ - Cache addresses for which overflows already have been detected. + Cache addresses for which overflows or underflows already have been detected. """ self._overflow_cache = {} # type: Dict[int, bool]