Merge branch 'develop' into enhance/tests

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:

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()

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]

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:
         """

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
 

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,

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()