From b57dd5c730c1ac6263ac1076f4ce9d67bfb35a00 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 16 Apr 2019 21:00:17 +0530 Subject: [PATCH] Fix the account transfer and add initial state --- mythril/analysis/solver.py | 18 +++++++++--------- mythril/analysis/symbolic.py | 18 ++++++++++++++++-- mythril/laser/ethereum/instructions.py | 9 ++++++++- mythril/laser/ethereum/state/world_state.py | 2 ++ mythril/laser/ethereum/svm.py | 18 ++++++++++++++++-- 5 files changed, 51 insertions(+), 14 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 0080081a..cb3f93c5 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -1,5 +1,5 @@ """This module contains analysis module helpers to solve path constraints.""" -from typing import Dict, List +from typing import Collection, Dict, List from z3 import sat, unknown, FuncInterp import z3 @@ -77,7 +77,9 @@ def pretty_print_model(model): return ret -def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str, List[Dict[str, str]]]: +def get_transaction_sequence( + global_state: GlobalState, constraints +) -> Dict[str, Collection]: """Generate concrete transaction sequence. :param global_state: GlobalState to generate transaction sequence for @@ -97,7 +99,7 @@ def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str "blockDifficulty": "", "blockGasLimit": "", "blockNumber": "", - "blockTime": "" + "blockTime": "", } # type: Dict[str, str] concrete_transactions = [] @@ -105,7 +107,7 @@ def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str tx_constraints = constraints.copy() minimize = [] - transactions = [] # type: List[BaseTransaction] + transactions = [] # type: List[BaseTransaction] for transaction in transaction_sequence: tx_id = str(transaction.id) if not isinstance(transaction, ContractCreationTransaction): @@ -141,13 +143,11 @@ def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str concrete_transaction["origin"] = "0x" + ( "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() ).zfill(40) - concrete_transaction["address"] = ( - "%s" % transaction.callee_account.address - ) + concrete_transaction["address"] = "%s" % transaction.callee_account.address concrete_transactions.append(concrete_transaction) - steps = { - "steps": concrete_transactions + "initialState": global_state.world_state.initial_state_account, + "steps": concrete_transactions, } return steps diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index c195a498..a7f54a77 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -12,7 +12,10 @@ from mythril.laser.ethereum.strategy.basic import ( ReturnRandomNaivelyStrategy, ReturnWeightedRandomStrategy, ) -from mythril.laser.ethereum.transaction.symbolic import CREATOR_ADDRESS +from mythril.laser.ethereum.transaction.symbolic import ( + ATTACKER_ADDRESS, + CREATOR_ADDRESS, +) from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory @@ -72,10 +75,21 @@ class SymExecWrapper: dynamic_loader=dynloader, contract_name=contract.name, ) + creator_account = Account( + hex(CREATOR_ADDRESS), "", dynamic_loader=dynloader, contract_name=None + ) + attacker_account = Account( + hex(ATTACKER_ADDRESS), "", dynamic_loader=dynloader, contract_name=None + ) + requires_statespace = ( compulsory_statespace or len(get_detection_modules("post", modules)) > 0 ) - self.accounts = {address: account} + self.accounts = { + address: account, + hex(CREATOR_ADDRESS): creator_account, + hex(ATTACKER_ADDRESS): attacker_account, + } self.laser = svm.LaserEVM( self.accounts, diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b6bb61cd..ea93eae2 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1842,6 +1842,14 @@ class Instruction: callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = 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") + 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( @@ -1859,7 +1867,6 @@ class Instruction: ) if native_result: return native_result - transaction = MessageCallTransaction( world_state=global_state.world_state, gas_price=environment.gasprice, diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 862b7c8d..d7164824 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -26,6 +26,7 @@ class WorldState: self.node = None # type: Optional['Node'] self.transaction_sequence = transaction_sequence or [] self._annotations = annotations or [] + self.initial_state_account = {} # type: Dict def __getitem__(self, item: str) -> Account: """Gets an account from the worldstate using item as key. @@ -47,6 +48,7 @@ class WorldState: ) new_world_state.accounts = copy(self.accounts) new_world_state.node = self.node + new_world_state.initial_state_account = self.initial_state_account return new_world_state def create_account( diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 0fcb8d77..e52169e3 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -1,9 +1,9 @@ """This module implements the main symbolic execution engine.""" import logging from collections import defaultdict -from copy import copy +from copy import copy, deepcopy from datetime import datetime, timedelta -from typing import Callable, Dict, DefaultDict, List, Tuple, Union +from typing import Any, Callable, Dict, DefaultDict, List, Tuple, Union from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException @@ -68,6 +68,8 @@ class LaserEVM: """ world_state = WorldState() world_state.accounts = accounts + world_state.initial_state_account = self.get_standard_initial_state(accounts) + # this sets the initial world state self.world_state = world_state self.open_states = [world_state] @@ -114,6 +116,18 @@ class LaserEVM: """ return self.world_state.accounts + @staticmethod + def get_standard_initial_state(accounts: Dict[str, Account]) -> Dict: + template = {"accounts": {}} # type: Dict[str, Dict[str, Any]] + for address, account in accounts.items(): + template["accounts"][address] = { + "nounce": account.nonce, + "balance": "", + "code": account.code.bytecode, + "storage": {}, + } + return template + def sym_exec( self, main_address=None, creation_code=None, contract_name=None ) -> None: