From a288da7bb5c42a3e443eccb82a73ea48a03b6dda Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 24 Jul 2019 16:28:03 -0700 Subject: [PATCH] Clean up leftover code --- mythril/analysis/modules/ether_thief.py | 17 +---- mythril/laser/ethereum/call.py | 1 - mythril/laser/ethereum/instructions.py | 73 ++++++++------------- mythril/laser/ethereum/state/world_state.py | 1 - 4 files changed, 30 insertions(+), 62 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index cf668b25..948e9c89 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -1,29 +1,16 @@ """This module contains the detection code for unauthorized ether withdrawal.""" import logging -import json from copy import copy from mythril.analysis import solver from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue -from mythril.laser.ethereum.transaction.symbolic import ( - ATTACKER_ADDRESS, - CREATOR_ADDRESS, -) +from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS 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, - simplify, - UGE, -) +from mythril.laser.smt import UGT, symbol_factory, UGE log = logging.getLogger(__name__) diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index f29c34bf..e31f0474 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -92,7 +92,6 @@ 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 index = int(match.group(1)) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index eda8a037..80dcd840 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -25,7 +25,6 @@ from mythril.laser.smt import ( Bool, Not, LShR, - BVSubNoUnderflow, UGE, ) from mythril.laser.smt import symbol_factory @@ -56,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. @@ -1697,17 +1720,7 @@ class Instruction: log.debug("The call is related to ether transfer between accounts") sender = environment.active_account.address receiver = callee_account.address - 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 + transfer_ether(sender, receiver, value) global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) @@ -1829,17 +1842,7 @@ class Instruction: log.debug("The call is related to ether transfer between accounts") sender = global_state.environment.active_account.address receiver = callee_account.address - 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 + transfer_ether(sender, receiver, value) global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) @@ -1954,17 +1957,7 @@ class Instruction: log.debug("The call is related to ether transfer between accounts") sender = environment.active_account.address receiver = callee_account.address - 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 + transfer_ether(sender, receiver, value) global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) @@ -2077,17 +2070,7 @@ class Instruction: log.debug("The call is related to ether transfer between accounts") sender = global_state.environment.active_account.address receiver = callee_account.address - 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 + transfer_ether(sender, receiver, value) global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 5227099e..20628877 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -182,6 +182,5 @@ class WorldState: :param account: """ - assert not account.address.symbolic # ??? self._accounts[account.address.value] = account account._balances = self.balances