From d29159e212d7566558820589e11d1d3cba568b17 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 12 Feb 2019 18:10:33 +0530 Subject: [PATCH 01/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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 e1c29a1c8321abb02a596bc6a928cfdb8c08b3da Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 1 Mar 2019 18:50:13 +0530 Subject: [PATCH 12/13] 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 13/13] 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(