Merge branch 'analyze-with-mythx' of github.com:ConsenSys/mythril-classic into analyze-with-mythx

README.md

@@ -32,7 +32,7 @@ Install from Pypi:
 $ pip3 install mythril
 ```
 
-See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup) for more detailed instructions. 
+See the [docs](https://mythril-classic.readthedocs.io/en/master/installation.html) for more detailed instructions. 
 
 ## Usage
 
@@ -75,7 +75,7 @@ Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0
 ```
 
 
-Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 
+Instructions for using Mythril are found on the [docs](https://mythril-classic.readthedocs.io/en/master/). 
 
 For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 

mythril/__version__.py

@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-__version__ = "v0.21.13"
+__version__ = "v0.21.15"

mythril/analysis/call_helpers.py

@@ -4,6 +4,7 @@ from typing import Union
 
 from mythril.analysis.ops import VarType, Call, get_variable
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 
 
 def get_call_from_state(state: GlobalState) -> Union[Call, None]:
@@ -28,7 +29,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
             get_variable(stack[-7]),
         )
 
-        if to.type == VarType.CONCRETE and 0 < to.val < 5:
+        if to.type == VarType.CONCRETE and 0 < to.val <= PRECOMPILE_COUNT:
             return None
 
         if meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE:

mythril/analysis/modules/ether_thief.py

@@ -1,7 +1,6 @@
 """This module contains the detection code for unauthorized ether
 withdrawal."""
 import logging
-import json
 from copy import copy
 
 from mythril.analysis import solver
@@ -13,9 +12,10 @@ from mythril.laser.ethereum.transaction.symbolic import (
 )
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
-from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import UGT, Sum, symbol_factory, BVAddNoOverflow, If
+from mythril.laser.ethereum.transaction import ContractCreationTransaction
+
+from mythril.laser.smt import UGT, symbol_factory, UGE
 
 log = logging.getLogger(__name__)
 
@@ -74,54 +74,48 @@ class EtherThief(DetectionModule):
         :param state:
         :return:
         """
+        state = copy(state)
         instruction = state.get_current_instruction()
 
-        if instruction["opcode"] != "CALL":
-            return []
-
         value = state.mstate.stack[-3]
         target = state.mstate.stack[-2]
 
-        eth_sent_by_attacker = symbol_factory.BitVecVal(0, 256)
-
         constraints = copy(state.mstate.constraints)
 
+        """
+        Require that the current transaction is sent by the attacker and
+        that the Ether sent to the attacker's address is greater than the
+        amount of Ether the attacker sent.
+        """
         for tx in state.world_state.transaction_sequence:
-            """
-            Constraint: The call value must be greater than the sum of Ether sent by the attacker over all
-            transactions. This prevents false positives caused by legitimate refund functions.
-            Also constrain the addition from overflowing (otherwise the solver produces solutions with
-            ridiculously high call values).
-            """
-            constraints += [
-                BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False)
-            ]
-            eth_sent_by_attacker = Sum(
-                eth_sent_by_attacker,
-                tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0),
-            )
-
             """
             Constraint: All transactions must originate from regular users (not the creator/owner).
             This prevents false positives where the owner willingly transfers ownership to another address.
             """
-
             if not isinstance(tx, ContractCreationTransaction):
                 constraints += [tx.caller != CREATOR_ADDRESS]
 
-        """
+        attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
-        Require that the current transaction is sent by the attacker and
-        that the Ether is sent to the attacker's address.
-        """
 
         constraints += [
-            UGT(value, eth_sent_by_attacker),
+            UGE(
+                state.world_state.balances[state.environment.active_account.address],
+                value,
+            )
+        ]
+        state.world_state.balances[attacker_address_bitvec] += value
+        state.world_state.balances[state.environment.active_account.address] -= value
+
+        constraints += [
+            UGT(
+                state.world_state.balances[attacker_address_bitvec],
+                state.world_state.starting_balances[attacker_address_bitvec],
+            ),
             target == ATTACKER_ADDRESS,
             state.current_transaction.caller == ATTACKER_ADDRESS,
         ]
 
         try:
-
             transaction_sequence = solver.get_transaction_sequence(state, constraints)
 
             issue = Issue(

mythril/analysis/modules/external_calls.py

@@ -10,6 +10,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
 from mythril.laser.smt import UGT, symbol_factory, Or, BitVec
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
 from copy import copy
@@ -33,7 +34,7 @@ def _is_precompile_call(global_state: GlobalState):
     constraints += [
         Or(
             to < symbol_factory.BitVecVal(1, 256),
-            to > symbol_factory.BitVecVal(16, 256),
+            to > symbol_factory.BitVecVal(PRECOMPILE_COUNT, 256),
         )
     ]
 

mythril/analysis/modules/suicide.py

@@ -60,9 +60,7 @@ class SuicideModule(DetectionModule):
 
         to = state.mstate.stack[-1]
 
-        log.debug(
+        log.debug("SUICIDE in function %s", state.environment.active_function_name)
-            "[SUICIDE] SUICIDE in function " + state.environment.active_function_name
-        )
 
         description_head = "The contract can be killed by anyone."
 
@@ -103,7 +101,7 @@ class SuicideModule(DetectionModule):
             )
             return [issue]
         except UnsatError:
-            log.info("[UNCHECKED_SUICIDE] no model found")
+            log.debug("No model found")
 
         return []
 

mythril/analysis/report.py

@@ -238,7 +238,7 @@ class Report:
             return {}
         logs = []  # type: List[Dict]
         for exception in self.exceptions:
-            logs += [{"level": "error", "hidden": "true", "msg": exception}]
+            logs += [{"level": "error", "hidden": True, "msg": exception}]
         return {"logs": logs}
 
     def as_swc_standard_format(self):

mythril/analysis/solver.py

@@ -95,7 +95,7 @@ def get_transaction_sequence(
     concrete_transactions = []
 
     tx_constraints, minimize = _set_minimisation_constraints(
-        transaction_sequence, constraints.copy(), [], 5000
+        transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
     )
 
     try:
@@ -103,19 +103,23 @@ def get_transaction_sequence(
     except UnsatError:
         raise UnsatError
 
-    min_price_dict = {}  # type: Dict[str, int]
+    # Include creation account in initial state
+    # Note: This contains the code, which should not exist until after the first tx
+    initial_world_state = transaction_sequence[0].world_state
+    initial_accounts = initial_world_state.accounts
+
     for transaction in transaction_sequence:
         concrete_transaction = _get_concrete_transaction(model, transaction)
         concrete_transactions.append(concrete_transaction)
 
-        caller = concrete_transaction["origin"]
+    min_price_dict = {}  # type: Dict[str, int]
-        value = int(concrete_transaction["value"], 16)
+    for address in initial_accounts.keys():
-        min_price_dict[caller] = min_price_dict.get(caller, 0) + value
+        min_price_dict[address] = model.eval(
-
+            initial_world_state.starting_balances[
-    if isinstance(transaction_sequence[0], ContractCreationTransaction):
+                symbol_factory.BitVecVal(address, 256)
-        initial_accounts = transaction_sequence[0].prev_world_state.accounts
+            ].raw,
-    else:
+            model_completion=True,
-        initial_accounts = transaction_sequence[0].world_state.accounts
+        ).as_long()
 
     concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
 
@@ -133,7 +137,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
         data = dict()  # type: Dict[str, Union[int, str]]
         data["nonce"] = account.nonce
         data["code"] = account.code.bytecode
-        data["storage"] = account.storage.printable_storage
+        data["storage"] = str(account.storage)
         data["balance"] = hex(min_price_dict.get(address, 0))
         accounts[hex(address)] = data
     return {"accounts": accounts}
@@ -171,7 +175,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
 
 
 def _set_minimisation_constraints(
-    transaction_sequence, constraints, minimize, max_size
+    transaction_sequence, constraints, minimize, max_size, world_state
 ) -> Tuple[Constraints, tuple]:
     """ Set constraints that minimise key transaction values
 
@@ -193,5 +197,21 @@ def _set_minimisation_constraints(
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
         minimize.append(transaction.call_value)
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(1000000000000000000000, 256),
+                world_state.starting_balances[transaction.caller],
+            )
+        )
+
+    for account in world_state.accounts.values():
+        # Lazy way to prevent overflows and to ensure "reasonable" balances
+        # Each account starts with less than 100 ETH
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(100000000000000000000, 256),
+                world_state.starting_balances[account.address],
+            )
+        )
 
     return constraints, tuple(minimize)

mythril/analysis/symbolic.py

@@ -14,6 +14,7 @@ from mythril.laser.ethereum.strategy.basic import (
     BasicSearchStrategy,
 )
 
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.transaction.symbolic import (
     ATTACKER_ADDRESS,
     CREATOR_ADDRESS,
@@ -212,7 +213,10 @@ class SymExecWrapper:
                             get_variable(stack[-7]),
                         )
 
-                        if to.type == VarType.CONCRETE and to.val < 5:
+                        if (
+                            to.type == VarType.CONCRETE
+                            and 0 < to.val <= PRECOMPILE_COUNT
+                        ):
                             # ignore prebuilts
                             continue
 

mythril/interfaces/cli.py

@@ -15,8 +15,7 @@ import coloredlogs
 import traceback
 
 import mythril.support.signatures as sigs
-from argparse import ArgumentParser, Namespace
+from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
-
 from mythril import mythx
 from mythril.exceptions import AddressNotFoundError, CriticalError
 from mythril.mythril import (
@@ -68,9 +67,7 @@ def exit_with_error(format_, message):
                 "sourceType": "",
                 "sourceFormat": "",
                 "sourceList": [],
-                "meta": {
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
             }
         ]
         print(json.dumps(result))
@@ -200,6 +197,7 @@ def main() -> None:
             output_parser,
         ],
         aliases=ANALYZE_LIST[1:],
+        formatter_class=RawTextHelpFormatter,
     )
     create_analyzer_parser(analyzer_parser)
 
@@ -213,6 +211,7 @@ def main() -> None:
             creation_input_parser,
             runtime_input_parser,
         ],
+        formatter_class=RawTextHelpFormatter,
     )
     create_disassemble_parser(disassemble_parser)
 
@@ -262,7 +261,13 @@ def create_disassemble_parser(parser: ArgumentParser):
     :param parser:
     :return:
     """
-    parser.add_argument("solidity_file", nargs="*")
+    # Using nargs=* would the implementation below for getting code for both disassemble and analyze
+    parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. Currently supports a single contract\n"
+        "usage: file1.sol:OptionalContractName",
+    )
 
 
 def create_pro_parser(parser: ArgumentParser):
@@ -343,7 +348,12 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
     :param analyzer_parser:
     :return:
     """
-    analyzer_parser.add_argument("solidity_file", nargs="*")
+    analyzer_parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. \n"
+        "usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName",
+    )
     commands = analyzer_parser.add_argument_group("commands")
     commands.add_argument("-g", "--graph", help="generate a control flow graph")
     commands.add_argument(
@@ -478,6 +488,8 @@ def validate_args(args: Namespace):
             exit_with_error(
                 args.outform, "Invalid -v value, you can find valid values in usage"
             )
+    if args.command in DISASSEMBLE_LIST and len(args.solidity_files) > 1:
+        exit_with_error("text", "Only a single arg is supported for using disassemble")
 
     if args.command in ANALYZE_LIST:
         if args.query_signature and sigs.ethereum_input_decoder is None:
@@ -562,15 +574,15 @@ def load_code(disassembler: MythrilDisassembler, args: Namespace):
     elif args.__dict__.get("address", False):
         # Get bytecode from a contract address
         address, _ = disassembler.load_from_address(args.address)
-    elif args.__dict__.get("solidity_file", False):
+    elif args.__dict__.get("solidity_files", False):
         # Compile Solidity source file(s)
-        if args.command in ANALYZE_LIST and args.graph and len(args.solidity_file) > 1:
+        if args.command in ANALYZE_LIST and args.graph and len(args.solidity_files) > 1:
             exit_with_error(
                 args.outform,
                 "Cannot generate call graphs from multiple input files. Please do it one at a time.",
             )
         address, _ = disassembler.load_from_solidity(
-            args.solidity_file
+            args.solidity_files
         )  # list of files
     else:
         exit_with_error(

mythril/interfaces/old_cli.py

@@ -44,9 +44,7 @@ def exit_with_error(format_, message):
                 "sourceType": "",
                 "sourceFormat": "",
                 "sourceList": [],
-                "meta": {
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
             }
         ]
         print(json.dumps(result))

mythril/laser/ethereum/call.py

@@ -10,13 +10,14 @@ import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum import natives
 from mythril.laser.ethereum.gas import OPCODE_GAS
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.state.calldata import (
     BaseCalldata,
     SymbolicCalldata,
     ConcreteCalldata,
 )
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import BitVec
+from mythril.laser.smt import BitVec, is_true
 from mythril.laser.smt import simplify, Expression, symbol_factory
 from mythril.support.loader import DynLoader
 
@@ -49,7 +50,11 @@ def get_call_parameters(
 
     callee_account = None
     call_data = get_call_data(global_state, memory_input_offset, memory_input_size)
-    if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0:
+    if (
+        isinstance(callee_address, BitVec)
+        or int(callee_address, 16) > PRECOMPILE_COUNT
+        or int(callee_address, 16) == 0
+    ):
         callee_account = get_callee_account(
             global_state, callee_address, dynamic_loader
         )
@@ -84,12 +89,11 @@ def get_callee_address(
     except TypeError:
         log.debug("Symbolic call encountered")
 
-        # TODO: This is broken. Now it should be Storage[(\d+)].
+        match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address)))
-        match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address)))
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
-            raise ValueError()
+            return symbolic_to_address
 
         index = int(match.group(1))
         log.debug("Dynamic contract address at storage index {}".format(index))
@@ -100,9 +104,8 @@ def get_callee_address(
                 "0x{:040X}".format(environment.active_account.address.value), index
             )
         # TODO: verify whether this happens or not
-        except Exception:
+        except:
-            log.debug("Error accessing contract storage.")
+            return symbolic_to_address
-            raise ValueError
 
         # testrpc simply returns the address, geth response is more elaborate.
         if not re.match(r"^0x[0-9a-f]{40}$", callee_address):
@@ -112,7 +115,9 @@ def get_callee_address(
 
 
 def get_callee_account(
-    global_state: GlobalState, callee_address: str, dynamic_loader: DynLoader
+    global_state: GlobalState,
+    callee_address: Union[str, BitVec],
+    dynamic_loader: DynLoader,
 ):
     """Gets the callees account from the global_state.
 
@@ -121,7 +126,11 @@ def get_callee_account(
     :param dynamic_loader: dynamic loader to use
     :return: Account belonging to callee
     """
-    accounts = global_state.accounts
+    if isinstance(callee_address, BitVec):
+        if callee_address.symbolic:
+            return Account(callee_address, balances=global_state.world_state.balances)
+        else:
+            callee_address = hex(callee_address.value)[2:]
 
     try:
         return global_state.accounts[int(callee_address, 16)]
@@ -151,7 +160,7 @@ def get_callee_account(
         dynamic_loader=dynamic_loader,
         balances=global_state.world_state.balances,
     )
-    accounts[callee_address] = callee_account
+    global_state.accounts[int(callee_address, 16)] = callee_account
 
     return callee_account
 
@@ -189,10 +198,10 @@ def get_call_data(
     )
 
     uses_entire_calldata = simplify(
-        memory_size - global_state.environment.calldata.calldatasize == 0
+        memory_size == global_state.environment.calldata.calldatasize
     )
 
-    if uses_entire_calldata is True:
+    if is_true(uses_entire_calldata):
         return global_state.environment.calldata
 
     try:
@@ -203,18 +212,24 @@ def get_call_data(
         ]
         return ConcreteCalldata(transaction_id, calldata_from_mem)
     except TypeError:
-        log.debug("Unsupported symbolic calldata offset")
+        log.debug(
+            "Unsupported symbolic calldata offset %s size %s", memory_start, memory_size
+        )
         return SymbolicCalldata(transaction_id)
 
 
 def native_call(
     global_state: GlobalState,
-    callee_address: str,
+    callee_address: Union[str, BitVec],
     call_data: BaseCalldata,
     memory_out_offset: Union[int, Expression],
     memory_out_size: Union[int, Expression],
 ) -> Optional[List[GlobalState]]:
-    if not 0 < int(callee_address, 16) < 5:
+
+    if (
+        isinstance(callee_address, BitVec)
+        or not 0 < int(callee_address, 16) <= PRECOMPILE_COUNT
+    ):
         return None
 
     log.debug("Native contract called: " + callee_address)

mythril/laser/ethereum/instructions.py

@@ -25,6 +25,7 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
+    UGE,
 )
 from mythril.laser.smt import symbol_factory
 
@@ -54,6 +55,30 @@ TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 
 
+def transfer_ether(
+    global_state: GlobalState,
+    sender: BitVec,
+    receiver: BitVec,
+    value: Union[int, BitVec],
+):
+    """
+    Perform an Ether transfer between two accounts
+
+    :param global_state: The global state in which the Ether transfer occurs
+    :param sender: The sender of the Ether
+    :param receiver: The recipient of the Ether
+    :param value: The amount of Ether to send
+    :return:
+    """
+    value = value if isinstance(value, BitVec) else symbol_factory.BitVecVal(value, 256)
+
+    global_state.mstate.constraints.append(
+        UGE(global_state.world_state.balances[sender], value)
+    )
+    global_state.world_state.balances[receiver] += value
+    global_state.world_state.balances[sender] -= value
+
+
 class StateTransition(object):
     """Decorator that handles global state copy and original return.
 
@@ -173,6 +198,7 @@ class Instruction:
         """
         # Generalize some ops
         log.debug("Evaluating %s at %i", self.op_code, global_state.mstate.pc)
+
         op = self.op_code.lower()
         if self.op_code.startswith("PUSH"):
             op = "push"
@@ -758,15 +784,10 @@ class Instruction:
             log.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
             dstart = simplify(op1)
 
-        size_sym = False
         try:
             size = util.get_concrete_int(op2)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic size in CALLDATACOPY")
-            size = simplify(op2)
-            size_sym = True
-
-        if size_sym:
             size = 320  # The excess size will get overwritten
 
         size = cast(int, size)
@@ -840,7 +861,11 @@ class Instruction:
         """
         state = global_state.mstate
         address = state.stack.pop()
-        state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
+
+        balance = global_state.world_state.balances[
+            global_state.environment.active_account.address
+        ]
+        state.stack.append(balance)
         return [global_state]
 
     @StateTransition()
@@ -1368,7 +1393,6 @@ class Instruction:
 
         state = global_state.mstate
         index = state.stack.pop()
-
         state.stack.append(global_state.environment.active_account.storage[index])
         return [global_state]
 
@@ -1381,7 +1405,6 @@ class Instruction:
         """
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
-
         global_state.environment.active_account.storage[index] = value
         return [global_state]
 
@@ -1615,7 +1638,7 @@ class Instruction:
         transfer_amount = global_state.environment.active_account.balance()
         # Often the target of the suicide instruction will be symbolic
         # If it isn't then we'll transfer the balance to the indicated contract
-        global_state.world_state[target].add_balance(transfer_amount)
+        global_state.world_state.balances[target] += transfer_amount
 
         global_state.environment.active_account = deepcopy(
             global_state.environment.active_account
@@ -1689,6 +1712,10 @@ class Instruction:
 
             if callee_account is not None and callee_account.code.bytecode == "":
                 log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
                 )
@@ -1804,6 +1831,18 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -1907,6 +1946,18 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -2008,6 +2059,18 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(

mythril/laser/ethereum/natives.py

@@ -6,12 +6,20 @@ from typing import List, Union
 
 from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
+import py_ecc.optimized_bn128 as bn128
 from rlp.utils import ALL_BYTES
 
 from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata
-from mythril.laser.ethereum.util import bytearray_to_int
+from mythril.laser.ethereum.util import extract_copy, extract32
-from ethereum.utils import sha3
+from ethereum.utils import (
-from mythril.laser.smt import Concat, simplify
+    sha3,
+    big_endian_to_int,
+    safe_ord,
+    zpad,
+    int_to_big_endian,
+    encode_int32,
+)
+from ethereum.specials import validate_point
 
 log = logging.getLogger(__name__)
 
@@ -22,35 +30,6 @@ class NativeContractException(Exception):
     pass
 
 
-def int_to_32bytes(
-    i: int
-) -> bytes:  # used because int can't fit as bytes function's input
-    """
-
-    :param i:
-    :return:
-    """
-    o = [0] * 32
-    for x in range(32):
-        o[31 - x] = i & 0xFF
-        i >>= 8
-    return bytes(o)
-
-
-def extract32(data: bytearray, i: int) -> int:
-    """
-
-    :param data:
-    :param i:
-    :return:
-    """
-    if i >= len(data):
-        return 0
-    o = data[i : min(i + 32, len(data))]
-    o.extend(bytearray(32 - len(o)))
-    return bytearray_to_int(o)
-
-
 def ecrecover(data: List[int]) -> List[int]:
     """
 
@@ -59,14 +38,14 @@ def ecrecover(data: List[int]) -> List[int]:
     """
     # TODO: Add type hints
     try:
-        byte_data = bytearray(data)
+        bytes_data = bytearray(data)
-        v = extract32(byte_data, 32)
+        v = extract32(bytes_data, 32)
-        r = extract32(byte_data, 64)
+        r = extract32(bytes_data, 64)
-        s = extract32(byte_data, 96)
+        s = extract32(bytes_data, 96)
     except TypeError:
         raise NativeContractException
 
-    message = b"".join([ALL_BYTES[x] for x in byte_data[0:32]])
+    message = b"".join([ALL_BYTES[x] for x in bytes_data[0:32]])
     if r >= secp256k1n or s >= secp256k1n or v < 27 or v > 28:
         return []
     try:
@@ -85,10 +64,10 @@ def sha256(data: List[int]) -> List[int]:
     :return:
     """
     try:
-        byte_data = bytes(data)
+        bytes_data = bytes(data)
     except TypeError:
         raise NativeContractException
-    return list(bytearray(hashlib.sha256(byte_data).digest()))
+    return list(bytearray(hashlib.sha256(bytes_data).digest()))
 
 
 def ripemd160(data: List[int]) -> List[int]:
@@ -120,6 +99,114 @@ def identity(data: List[int]) -> List[int]:
     return data
 
 
+def mod_exp(data: List[int]) -> List[int]:
+    """
+    TODO: Some symbolic parts can be handled here
+    Modular Exponentiation
+    :param data: Data with <length_of_BASE> <length_of_EXPONENT> <length_of_MODULUS> <BASE> <EXPONENT> <MODULUS>
+    :return: modular exponentiation
+    """
+    bytes_data = bytearray(data)
+    baselen = extract32(bytes_data, 0)
+    explen = extract32(bytes_data, 32)
+    modlen = extract32(bytes_data, 64)
+    if baselen == 0:
+        return [0] * modlen
+    if modlen == 0:
+        return []
+
+    first_exp_bytes = extract32(bytes_data, 96 + baselen) >> (8 * max(32 - explen, 0))
+    bitlength = -1
+    while first_exp_bytes:
+        bitlength += 1
+        first_exp_bytes >>= 1
+
+    base = bytearray(baselen)
+    extract_copy(bytes_data, base, 0, 96, baselen)
+    exp = bytearray(explen)
+    extract_copy(bytes_data, exp, 0, 96 + baselen, explen)
+    mod = bytearray(modlen)
+    extract_copy(bytes_data, mod, 0, 96 + baselen + explen, modlen)
+    if big_endian_to_int(mod) == 0:
+        return [0] * modlen
+    o = pow(big_endian_to_int(base), big_endian_to_int(exp), big_endian_to_int(mod))
+    return [safe_ord(x) for x in zpad(int_to_big_endian(o), modlen)]
+
+
+def ec_add(data: List[int]) -> List[int]:
+    bytes_data = bytearray(data)
+    x1 = extract32(bytes_data, 0)
+    y1 = extract32(bytes_data, 32)
+    x2 = extract32(bytes_data, 64)
+    y2 = extract32(bytes_data, 96)
+    p1 = validate_point(x1, y1)
+    p2 = validate_point(x2, y2)
+    if p1 is False or p2 is False:
+        return []
+    o = bn128.normalize(bn128.add(p1, p2))
+    return [safe_ord(x) for x in (encode_int32(o[0].n) + encode_int32(o[1].n))]
+
+
+def ec_mul(data: List[int]) -> List[int]:
+    bytes_data = bytearray(data)
+    x = extract32(bytes_data, 0)
+    y = extract32(bytes_data, 32)
+    m = extract32(bytes_data, 64)
+    p = validate_point(x, y)
+    if p is False:
+        return []
+    o = bn128.normalize(bn128.multiply(p, m))
+    return [safe_ord(c) for c in (encode_int32(o[0].n) + encode_int32(o[1].n))]
+
+
+def ec_pair(data: List[int]) -> List[int]:
+    if len(data) % 192:
+        return []
+
+    zero = (bn128.FQ2.one(), bn128.FQ2.one(), bn128.FQ2.zero())
+    exponent = bn128.FQ12.one()
+    bytes_data = bytearray(data)
+    for i in range(0, len(bytes_data), 192):
+        x1 = extract32(bytes_data, i)
+        y1 = extract32(bytes_data, i + 32)
+        x2_i = extract32(bytes_data, i + 64)
+        x2_r = extract32(bytes_data, i + 96)
+        y2_i = extract32(bytes_data, i + 128)
+        y2_r = extract32(bytes_data, i + 160)
+        p1 = validate_point(x1, y1)
+        if p1 is False:
+            return []
+        for v in (x2_i, x2_r, y2_i, y2_r):
+            if v >= bn128.field_modulus:
+                return []
+        fq2_x = bn128.FQ2([x2_r, x2_i])
+        fq2_y = bn128.FQ2([y2_r, y2_i])
+        if (fq2_x, fq2_y) != (bn128.FQ2.zero(), bn128.FQ2.zero()):
+            p2 = (fq2_x, fq2_y, bn128.FQ2.one())
+            if not bn128.is_on_curve(p2, bn128.b2):
+                return []
+        else:
+            p2 = zero
+        if bn128.multiply(p2, bn128.curve_order)[-1] != bn128.FQ2.zero():
+            return []
+        exponent *= bn128.pairing(p2, p1, final_exponentiate=False)
+    result = bn128.final_exponentiate(exponent) == bn128.FQ12.one()
+    return [0] * 31 + [1 if result else 0]
+
+
+PRECOMPILE_FUNCTIONS = (
+    ecrecover,
+    sha256,
+    ripemd160,
+    identity,
+    mod_exp,
+    ec_add,
+    ec_mul,
+    ec_pair,
+)
+PRECOMPILE_COUNT = len(PRECOMPILE_FUNCTIONS)
+
+
 def native_contracts(address: int, data: BaseCalldata) -> List[int]:
     """Takes integer address 1, 2, 3, 4.
 
@@ -127,11 +214,10 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]:
     :param data:
     :return:
     """
-    functions = (ecrecover, sha256, ripemd160, identity)
 
     if isinstance(data, ConcreteCalldata):
         concrete_data = data.concrete(None)
     else:
         raise NativeContractException()
 
-    return functions[address - 1](concrete_data)
+    return PRECOMPILE_FUNCTIONS[address - 1](concrete_data)

mythril/laser/ethereum/plugins/implementations/dependency_pruner.py

@@ -25,6 +25,7 @@ class DependencyAnnotation(StateAnnotation):
     def __init__(self):
         self.storage_loaded = []  # type: List
         self.storage_written = {}  # type: Dict[int, List]
+        self.has_call = False  # type: bool
         self.path = [0]  # type: List
         self.blocks_seen = set()  # type: Set[int]
 
@@ -32,6 +33,7 @@ class DependencyAnnotation(StateAnnotation):
         result = DependencyAnnotation()
         result.storage_loaded = copy(self.storage_loaded)
         result.storage_written = copy(self.storage_written)
+        result.has_call = self.has_call
         result.path = copy(self.path)
         result.blocks_seen = copy(self.blocks_seen)
         return result
@@ -134,6 +136,7 @@ class DependencyPruner(LaserPlugin):
 
     def _reset(self):
         self.iteration = 0
+        self.calls_on_path = {}  # type: Dict[int, bool]
         self.sloads_on_path = {}  # type: Dict[int, List[object]]
         self.sstores_on_path = {}  # type: Dict[int, List[object]]
         self.storage_accessed_global = set()  # type: Set
@@ -166,6 +169,17 @@ class DependencyPruner(LaserPlugin):
             else:
                 self.sstores_on_path[address] = [target_location]
 
+    def update_calls(self, path: List[int]) -> None:
+        """Update the dependency map for the block offsets on the given path.
+
+        :param path
+        :param target_location
+        """
+
+        for address in path:
+            if address in self.sstores_on_path:
+                self.calls_on_path[address] = True
+
     def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool:
         """Decide whether the basic block starting at 'address' should be executed.
 
@@ -175,6 +189,9 @@ class DependencyPruner(LaserPlugin):
 
         storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1)
 
+        if address in self.calls_on_path:
+            return True
+
         # Skip "pure" paths that don't have any dependencies.
 
         if address not in self.sloads_on_path:
@@ -270,6 +287,13 @@ class DependencyPruner(LaserPlugin):
             self.update_sloads(annotation.path, location)
             self.storage_accessed_global.add(location)
 
+        @symbolic_vm.pre_hook("CALL")
+        def call_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+
+            self.update_calls(annotation.path)
+            annotation.has_call = True
+
         @symbolic_vm.pre_hook("STOP")
         def stop_hook(state: GlobalState):
             _transaction_end(state)
@@ -293,11 +317,14 @@ class DependencyPruner(LaserPlugin):
             for index in annotation.storage_written:
                 self.update_sstores(annotation.path, index)
 
+            if annotation.has_call:
+                self.update_calls(annotation.path)
+
         def _check_basic_block(address: int, annotation: DependencyAnnotation):
             """This method is where the actual pruning happens.
 
              :param address: Start address (bytecode offset) of the block
-             :param annotation
+             :param annotation:
              """
 
             # Don't skip any blocks in the contract creation transaction
@@ -338,13 +365,3 @@ class DependencyPruner(LaserPlugin):
             annotation.storage_loaded = []
 
             world_state_annotation.annotations_stack.append(annotation)
-
-            log.debug(
-                "Iteration {}: Adding world state at address {}, end of function {}.\nDependency map: {}\nStorage written: {}".format(
-                    self.iteration,
-                    state.get_current_instruction()["address"],
-                    state.node.function_name,
-                    self.sloads_on_path,
-                    annotation.storage_written[self.iteration],
-                )
-            )

mythril/laser/ethereum/plugins/implementations/mutation_pruner.py

@@ -42,7 +42,11 @@ class MutationPruner(LaserPlugin):
         """
 
         @symbolic_vm.pre_hook("SSTORE")
-        def mutator_hook(global_state: GlobalState):
+        def sstore_mutator_hook(global_state: GlobalState):
+            global_state.annotate(MutationAnnotation())
+
+        @symbolic_vm.pre_hook("CALL")
+        def call_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
         @symbolic_vm.laser_hook("add_world_state")

mythril/laser/ethereum/state/account.py

@@ -4,7 +4,7 @@ This includes classes representing accounts and their storage.
 """
 import logging
 from copy import copy, deepcopy
-from typing import Any, Dict, Union, Tuple, cast
+from typing import Any, Dict, Union, Tuple, Set, cast
 
 
 from mythril.laser.smt import (
@@ -60,6 +60,7 @@ class Storage:
         self.printable_storage = {}  # type: Dict[BitVec, BitVec]
 
         self.dynld = dynamic_loader
+        self.storage_keys_loaded = set()  # type: Set[int]
         self.address = address
 
     @staticmethod
@@ -74,17 +75,18 @@ class Storage:
     def __getitem__(self, item: BitVec) -> BitVec:
         storage, is_keccak_storage = self._get_corresponding_storage(item)
         if is_keccak_storage:
-            item = self._sanitize(cast(BitVecFunc, item).input_)
+            sanitized_item = self._sanitize(cast(BitVecFunc, item).input_)
-        value = storage[item]
+        else:
+            sanitized_item = item
         if (
-            (value.value == 0 or value.value is None)  # 0 for Array, None for K
+            self.address
-            and self.address
-            and item.symbolic is False
             and self.address.value != 0
+            and item.symbolic is False
+            and int(item.value) not in self.storage_keys_loaded
             and (self.dynld and self.dynld.storage_loading)
         ):
             try:
-                storage[item] = symbol_factory.BitVecVal(
+                storage[sanitized_item] = symbol_factory.BitVecVal(
                     int(
                         self.dynld.read_storage(
                             contract_address="0x{:040X}".format(self.address.value),
@@ -94,12 +96,12 @@ class Storage:
                     ),
                     256,
                 )
-                self.printable_storage[item] = storage[item]
+                self.storage_keys_loaded.add(int(item.value))
-                return storage[item]
+                self.printable_storage[item] = storage[sanitized_item]
             except ValueError as e:
                 log.debug("Couldn't read storage at %s: %s", item, e)
 
-        return simplify(storage[item])
+        return simplify(storage[sanitized_item])
 
     @staticmethod
     def get_map_index(key: BitVec) -> BitVec:
@@ -136,6 +138,8 @@ class Storage:
         if is_keccak_storage:
             key = self._sanitize(key.input_)
         storage[key] = value
+        if key.symbolic is False:
+            self.storage_keys_loaded.add(int(key.value))
 
     def __deepcopy__(self, memodict=dict()):
         concrete = isinstance(self._standard_storage, K)
@@ -144,7 +148,8 @@ class Storage:
         )
         storage._standard_storage = deepcopy(self._standard_storage)
         storage._map_storage = deepcopy(self._map_storage)
-        storage.print_storage = copy(self.printable_storage)
+        storage.printable_storage = copy(self.printable_storage)
+        storage.storage_keys_loaded = copy(self.storage_keys_loaded)
         return storage
 
     def __str__(self) -> str:

mythril/laser/ethereum/state/world_state.py

@@ -27,6 +27,7 @@ class WorldState:
         """
         self._accounts = {}  # type: Dict[int, Account]
         self.balances = Array("balance", 256, 256)
+        self.starting_balances = copy(self.balances)
 
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
@@ -60,6 +61,7 @@ class WorldState:
             annotations=new_annotations,
         )
         new_world_state.balances = copy(self.balances)
+        new_world_state.starting_balances = copy(self.starting_balances)
         for account in self._accounts.values():
             new_world_state.put_account(copy(account))
         new_world_state.node = self.node
@@ -115,7 +117,7 @@ class WorldState:
             concrete_storage=concrete_storage,
         )
         if balance:
-            new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
+            new_account.add_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
         return new_account

mythril/laser/ethereum/svm.py

@@ -257,6 +257,7 @@ class LaserEVM:
 
     def _add_world_state(self, global_state: GlobalState):
         """ Stores the world_state of the passed global state in the open states"""
+
         for hook in self._add_world_state_hooks:
             try:
                 hook(global_state)
@@ -325,6 +326,8 @@ class LaserEVM:
             new_global_state.node = global_state.node
             new_global_state.mstate.constraints = global_state.mstate.constraints
 
+            log.debug("Starting new transaction %s", start_signal.transaction)
+
             return [new_global_state], op_code
 
         except TransactionEndSignal as end_signal:
@@ -332,6 +335,8 @@ class LaserEVM:
                 -1
             ]
 
+            log.debug("Ending transaction %s.", transaction)
+
             if return_global_state is None:
                 if (
                     not isinstance(transaction, ContractCreationTransaction)

mythril/laser/ethereum/transaction/symbolic.py

@@ -23,7 +23,7 @@ ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 ACTOR_ADDRESSES = [
     symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
     symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256),
-    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256),
+    symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256),
 ]
 
 

mythril/laser/ethereum/transaction/transaction_models.py

@@ -4,7 +4,7 @@ execution."""
 import array
 from copy import deepcopy
 from z3 import ExprRef
-from typing import Union, Optional, cast
+from typing import Union, Optional
 
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.laser.ethereum.state.account import Account
@@ -12,8 +12,10 @@ from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
 from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
-from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.smt import symbol_factory, UGE, BitVec
-from mythril.laser.smt import symbol_factory
+import logging
+
+log = logging.getLogger(__name__)
 
 _next_transaction_id = 0
 
@@ -115,16 +117,31 @@ class BaseTransaction:
 
         sender = environment.sender
         receiver = environment.active_account.address
-        value = environment.callvalue
+        value = (
+            environment.callvalue
+            if isinstance(environment.callvalue, BitVec)
+            else symbol_factory.BitVecVal(environment.callvalue, 256)
+        )
 
-        global_state.world_state.balances[sender] -= value
+        global_state.mstate.constraints.append(
+            UGE(global_state.world_state.balances[sender], value)
+        )
         global_state.world_state.balances[receiver] += value
+        global_state.world_state.balances[sender] -= value
 
         return global_state
 
     def initial_global_state(self) -> GlobalState:
         raise NotImplementedError
 
+    def __str__(self) -> str:
+        return "{} {} from {} to {:#42x}".format(
+            self.__class__.__name__,
+            self.id,
+            self.caller,
+            int(str(self.callee_account.address)) if self.callee_account else -1,
+        )
+
 
 class MessageCallTransaction(BaseTransaction):
     """Transaction object models an transaction."""
@@ -180,7 +197,6 @@ class ContractCreationTransaction(BaseTransaction):
             0, concrete_storage=True, creator=caller.value
         )
         callee_account.contract_name = contract_name
-        # TODO: set correct balance for new account
         super().__init__(
             world_state=world_state,
             callee_account=callee_account,

mythril/laser/ethereum/util.py

@@ -150,3 +150,27 @@ def bytearray_to_int(arr):
     for a in arr:
         o = (o << 8) + a
     return o
+
+
+def extract_copy(
+    data: bytearray, mem: bytearray, memstart: int, datastart: int, size: int
+):
+    for i in range(size):
+        if datastart + i < len(data):
+            mem[memstart + i] = data[datastart + i]
+        else:
+            mem[memstart + i] = 0
+
+
+def extract32(data: bytearray, i: int) -> int:
+    """
+
+    :param data:
+    :param i:
+    :return:
+    """
+    if i >= len(data):
+        return 0
+    o = data[i : min(i + 32, len(data))]
+    o.extend(bytearray(32 - len(o)))
+    return bytearray_to_int(o)

requirements.txt

@@ -1,7 +1,7 @@
 coloredlogs>=10.0
 configparser>=3.5.0
 coverage
-py_ecc==1.4.2
+py_ecc==1.6.0
 eth_abi==1.3.0
 eth-account>=0.1.0a2,<=0.3.0
 ethereum>=2.3.2

setup.py

@@ -25,7 +25,7 @@ REQUIRES_PYTHON = ">=3.5.0"
 # What packages are required for this module to be executed?
 REQUIRED = [
     "coloredlogs>=10.0",
-    "py_ecc==1.4.2",
+    "py_ecc==1.6.0",
     "ethereum>=2.3.2",
     "z3-solver>=4.8.5.0",
     "requests>=2.22.0",

tests/laser/Precompiles/test_ec_add.py

@@ -0,0 +1,27 @@
+from mock import patch
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import ec_add
+from py_ecc.optimized_bn128 import FQ
+
+VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+
+def test_ec_add_sanity():
+    assert ec_add(VECTOR_A) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.add", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_add(f1, f2, f3):
+    FQ.fielf_modulus = 128
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    assert ec_add(VECTOR_A) == ([0] * 31 + [1]) * 2

tests/laser/Precompiles/test_elliptic_curves.py

@@ -0,0 +1,35 @@
+from mock import patch
+from mythril.laser.ethereum.natives import ec_pair
+from py_ecc.optimized_bn128 import FQ
+
+
+def test_ec_pair_192_check():
+    vec_c = [0] * 100
+    assert ec_pair(vec_c) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.is_on_curve", return_value=True)
+@patch("mythril.laser.ethereum.natives.bn128.pairing", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_pair(f1, f2, f3, f4):
+    FQ.fielf_modulus = 100
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    vec_c = [0] * 192
+    assert ec_pair(vec_c) == [0] * 31 + [1]
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=False)
+def test_ec_pair_point_validation_failure(f1):
+    vec_c = [0] * 192
+    assert ec_pair(vec_c) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+def test_ec_pair_field_exceed_mod(f1):
+    FQ.fielf_modulus = 100
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    vec_c = [10] * 192
+    assert ec_pair(vec_c) == []

tests/laser/Precompiles/test_elliptic_mul.py

@@ -0,0 +1,27 @@
+from mock import patch
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import ec_mul
+from py_ecc.optimized_bn128 import FQ
+
+VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.multiply", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_mul(f1, f2, f3):
+    FQ.fielf_modulus = 128
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    assert ec_mul(VECTOR_A) == ([0] * 31 + [1]) * 2
+
+
+def test_ec_mul_validation_failure():
+    assert ec_mul(VECTOR_A) == []

tests/laser/Precompiles/test_mod_exp.py

@@ -0,0 +1,61 @@
+import pytest
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import mod_exp
+from ethereum.utils import big_endian_to_int
+
+
+EIP198_VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+EIP198_VECTOR_B = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000000"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+EIP198_VECTOR_C = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000002"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "ffff"
+    "8000000000000000000000000000000000000000000000000000000000000000"
+    "07"
+)
+
+EIP198_VECTOR_D = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000002"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "ffff"
+    "80"
+)
+
+
+@pytest.mark.parametrize(
+    "data,expected",
+    (
+        (EIP198_VECTOR_A, 1),
+        (EIP198_VECTOR_B, 0),
+        (
+            EIP198_VECTOR_C,
+            26689440342447178617115869845918039756797228267049433585260346420242739014315,
+        ),
+        (
+            EIP198_VECTOR_D,
+            26689440342447178617115869845918039756797228267049433585260346420242739014315,
+        ),
+    ),
+)
+def test_modexp_result(data, expected):
+    actual = mod_exp(data)
+    assert big_endian_to_int(actual) == expected

tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json

@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {

tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json

@@ -54,7 +54,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {

tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json

@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {

tests/laser/transaction/create_transaction_test.py

@@ -44,7 +44,7 @@ def test_sym_exec():
         contract,
         address=(util.get_indexed_address(0)),
         strategy="dfs",
-        execution_timeout=10,
+        execution_timeout=25,
     )
     issues = fire_lasers(sym)