Revert Ether thief change & introduce symbolic starting balance

revert_ether_thief
Bernhard Mueller 5 years ago
parent 8b5e484f87
commit a250f40baa
  1. 12
      mythril/analysis/module/modules/ether_thief.py
  2. 9
      mythril/laser/ethereum/state/world_state.py
  3. 2
      mythril/laser/ethereum/transaction/transaction_models.py

@ -40,7 +40,7 @@ class EtherThief(DetectionModule):
swc_id = UNPROTECTED_ETHER_WITHDRAWAL
description = DESCRIPTION
entry_point = EntryPoint.CALLBACK
pre_hooks = ["STOP"]
pre_hooks = ["CALL", "STATICCALL"]
def reset_module(self):
"""
@ -70,16 +70,16 @@ class EtherThief(DetectionModule):
"""
state = copy(state)
instruction = state.get_current_instruction()
to = state.mstate.stack[-2]
constraints = copy(state.world_state.constraints)
attacker_address_bitvec = ACTORS.attacker
constraints += [
to == ACTORS.attacker,
UGT(
state.world_state.balances[attacker_address_bitvec],
state.world_state.starting_balances[attacker_address_bitvec],
)
state.world_state.balances[ACTORS.attacker],
state.world_state.starting_balances[ACTORS.attacker],
),
]
potential_issue = PotentialIssue(

@ -125,7 +125,7 @@ class WorldState:
def create_account(
self,
balance=0,
balance=None,
address=None,
concrete_storage=False,
dynamic_loader=None,
@ -157,7 +157,12 @@ class WorldState:
if code:
new_account.code = code
new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
if balance is not None:
new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
else:
new_account.set_balance(
symbol_factory.BitVecSym("initial)_balance_{}".format(address), 256)
)
self.put_account(new_account)
return new_account

@ -202,7 +202,7 @@ class ContractCreationTransaction(BaseTransaction):
contract_address if isinstance(contract_address, int) else None
)
callee_account = world_state.create_account(
0, concrete_storage=True, creator=caller.value, address=contract_address
concrete_storage=True, creator=caller.value, address=contract_address
)
callee_account.contract_name = contract_name or callee_account.contract_name
# init_call_data "should" be false, but it is easier to model the calldata symbolically

Loading…
Cancel
Save