diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 7df300ec..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], @@ -222,22 +274,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 +286,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..46795b8d 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.support.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/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 26e07979..054969a7 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -521,16 +521,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: """ 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 diff --git a/mythril/mythril.py b/mythril/mythril.py index 2f082ba0..4654b235 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -36,6 +36,8 @@ 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.support.start_time import StartTime + log = logging.getLogger(__name__) @@ -569,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/support/start_time.py b/mythril/support/start_time.py new file mode 100644 index 00000000..52b6714f --- /dev/null +++ b/mythril/support/start_time.py @@ -0,0 +1,9 @@ +from time import time +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()