diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 76952a54..b5dc8c02 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -114,15 +114,21 @@ class EtherThief(DetectionModule): Require that the current transaction is sent by the attacker and that the Ether is sent to the attacker's address. """ - + attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256) + eth_recieved_by_attacker = ( + value + + state.world_state.balances[attacker_address_bitvec] + - state.world_state.starting_balances[attacker_address_bitvec] + ) + eth_recieved_by_attacker.simplify() + print(eth_recieved_by_attacker) constraints += [ - UGT(value, eth_sent_by_attacker), + UGT(eth_recieved_by_attacker, eth_sent_by_attacker), target == ATTACKER_ADDRESS, state.current_transaction.caller == ATTACKER_ADDRESS, ] try: - transaction_sequence = solver.get_transaction_sequence(state, constraints) issue = Issue( diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2 index dd70bb45..776b661d 100644 --- a/mythril/analysis/templates/report_as_text.jinja2 +++ b/mythril/analysis/templates/report_as_text.jinja2 @@ -21,6 +21,8 @@ In file: {{ issue.filename }}:{{ issue.lineno }} {% if issue.tx_sequence %} Transaction Sequence: +{{ issue.tx_sequence.initialState }} + {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }} diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 918c1d3f..7cb084b0 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -49,7 +49,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) >= 5 + or int(callee_address, 16) == 0 + ): callee_account = get_callee_account( global_state, callee_address, dynamic_loader ) @@ -88,6 +92,8 @@ def get_callee_address( log.debug("CALL to: " + str(simplify(symbolic_to_address))) if match is None or dynamic_loader is None: + # TODO: Fix types + return symbolic_to_address raise ValueError() index = int(match.group(1)) @@ -111,7 +117,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. @@ -123,6 +131,12 @@ def get_callee_account( environment = global_state.environment 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 = callee_address.value + try: return global_state.accounts[int(callee_address, 16)] except KeyError: diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b3e3eaa6..79c00945 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -25,7 +25,7 @@ from mythril.laser.smt import ( Bool, Not, LShR, -) + BVSubNoUnderflow, UGE) from mythril.laser.smt import symbol_factory import mythril.laser.ethereum.util as helper @@ -840,7 +840,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() @@ -1688,7 +1692,14 @@ class Instruction: ) if callee_account is not None and callee_account.code.bytecode == "": - log.debug("The call is related to ether transfer between accounts") + log.warning( + "The call is related to ether transfer between accounts" + ) # TODO: was debug + + global_state.mstate.constraints.append(UGE(global_state.world_state.balances[environment.active_account.address], value)) + #global_state.world_state.balances[environment.active_account.address] -= value + global_state.world_state.balances[callee_account.address] += value + global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) ) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index f5196287..9e83f63a 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -169,6 +169,8 @@ class Account: self._balances = balances self.balance = lambda: self._balances[self.address] + # TODO: Add initial balance + def __str__(self) -> str: return str(self.as_dict) diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 236da526..d5851533 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/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 @@ -180,5 +182,6 @@ class WorldState: :param account: """ + assert not account.address.symbolic # ??? self._accounts[account.address.value] = account account._balances = self.balances diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 93cc7e3b..2f5c34cf 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -13,7 +13,7 @@ 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 +from mythril.laser.smt import symbol_factory, BVSubNoUnderflow, UGE _next_transaction_id = 0 @@ -117,7 +117,8 @@ class BaseTransaction: receiver = environment.active_account.address value = environment.callvalue - 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[sender] -= value global_state.world_state.balances[receiver] += value return global_state