diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index db5eb6b8..94b3588b 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -2,12 +2,15 @@ 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 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 @@ -19,6 +22,8 @@ from mythril.laser.smt import ( symbol_factory, Not, Expression, + Bool, + And, ) import logging @@ -31,7 +36,7 @@ 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, constraint: Bool ) -> None: self.overflowing_state = overflowing_state self.operator = operator @@ -42,7 +47,7 @@ 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, constraint: Bool ) -> None: self.overflowing_state = overflowing_state self.operator = operator @@ -63,7 +68,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 +93,30 @@ 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"] + funcs = { + "ADD": [self._handle_add], + "SUB": [self._handle_sub], + "MUL": [self._handle_mul], + "SSTORE": [self._handle_sstore], + "JUMPI": [self._handle_jumpi], + "RETURN": [self._handle_return, self._handle_transaction_end], + "STOP": [self._handle_transaction_end], + "EXP": [self._handle_exp], + } + for func in funcs[opcode]: + func(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 @@ -118,12 +128,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): 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 @@ -135,11 +140,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): 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 @@ -150,6 +151,33 @@ class IntegerOverflowUnderflowModule(DetectionModule): 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: + constraint = And( + op1 > symbol_factory.BitVecVal(256, 256), + 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 + ) + else: + constraint = op0.value ** op1.value >= 2 ** 256 + model = self._try_constraints(state.node.constraints, [constraint]) + if model is None: + return + annotation = OverUnderflowAnnotation(state, "exponentiation", constraint) + op0.annotate(annotation) + @staticmethod def _make_bitvec_if_not(stack, index): value = stack[index] @@ -185,7 +213,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: @@ -215,6 +242,31 @@ 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]) + except TypeError: + return + for element in state.mstate.memory[offset : offset + length]: + if not isinstance(element, Expression): + continue + 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], diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 79ab0749..161e742a 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] @@ -1296,7 +1302,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/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: """ 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