Merge pull request #1054 from ConsenSys/ether_thief_fix

Add constraints on sender and receiver
pull/1056/head
Bernhard Mueller 6 years ago committed by GitHub
commit 317f647b50
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 11
      mythril/analysis/modules/ether_thief.py

@ -7,6 +7,7 @@ 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
from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.state.global_state import GlobalState
@ -81,15 +82,13 @@ class EtherThief(DetectionModule):
constraints = copy(state.mstate.constraints)
for tx in state.world_state.transaction_sequence:
if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF:
# There's sometimes no overflow check on balances added.
# But we don't care about attacks that require more 2^^256 ETH to be sent.
constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)]
eth_sent_total = Sum(eth_sent_total, tx.call_value)
constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)]
eth_sent_total = Sum(eth_sent_total, tx.call_value)
constraints += [
tx.caller == ATTACKER_ADDRESS,
UGT(call_value, eth_sent_total),
target == state.environment.sender,
target == ATTACKER_ADDRESS,
]
try:

Loading…
Cancel
Save