|
|
|
@ -3,6 +3,7 @@ from mythril.analysis import solver |
|
|
|
|
from mythril.analysis.report import Issue |
|
|
|
|
from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL |
|
|
|
|
from mythril.analysis.modules.base import DetectionModule |
|
|
|
|
from mythril.laser.ethereum.state.global_state import GlobalState |
|
|
|
|
from mythril.exceptions import UnsatError |
|
|
|
|
from z3 import BitVecVal, UGT, Sum |
|
|
|
|
import logging |
|
|
|
@ -22,80 +23,79 @@ An issue is reported if: |
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class EtherThief(DetectionModule): |
|
|
|
|
def __init__(self): |
|
|
|
|
super().__init__( |
|
|
|
|
name="Ether Thief", |
|
|
|
|
swc_id=UNPROTECTED_ETHER_WITHDRAWAL, |
|
|
|
|
hooks=["CALL"], |
|
|
|
|
description=DESCRIPTION, |
|
|
|
|
) |
|
|
|
|
def _analyze_state(state): |
|
|
|
|
instruction = state.get_current_instruction() |
|
|
|
|
node = state.node |
|
|
|
|
|
|
|
|
|
def execute(self, state_space): |
|
|
|
|
logging.debug("Executing module: %s", self.name) |
|
|
|
|
issues = [] |
|
|
|
|
if instruction["opcode"] != "CALL": |
|
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
for k in state_space.nodes: |
|
|
|
|
node = state_space.nodes[k] |
|
|
|
|
for state in node.states: |
|
|
|
|
issues += self._analyze_state(state, node) |
|
|
|
|
call_value = state.mstate.stack[-3] |
|
|
|
|
target = state.mstate.stack[-2] |
|
|
|
|
|
|
|
|
|
return issues |
|
|
|
|
eth_sent_total = BitVecVal(0, 256) |
|
|
|
|
|
|
|
|
|
@staticmethod |
|
|
|
|
def _analyze_state(state, node): |
|
|
|
|
issues = [] |
|
|
|
|
instruction = state.get_current_instruction() |
|
|
|
|
constraints = node.constraints |
|
|
|
|
|
|
|
|
|
if instruction["opcode"] != "CALL": |
|
|
|
|
return [] |
|
|
|
|
for tx in state.world_state.transaction_sequence: |
|
|
|
|
if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF: |
|
|
|
|
|
|
|
|
|
call_value = state.mstate.stack[-3] |
|
|
|
|
target = state.mstate.stack[-2] |
|
|
|
|
# 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. |
|
|
|
|
|
|
|
|
|
eth_sent_total = BitVecVal(0, 256) |
|
|
|
|
constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)] |
|
|
|
|
eth_sent_total = Sum(eth_sent_total, tx.call_value) |
|
|
|
|
|
|
|
|
|
constraints = node.constraints |
|
|
|
|
constraints += [ |
|
|
|
|
UGT(call_value, eth_sent_total), |
|
|
|
|
target == state.environment.sender, |
|
|
|
|
] |
|
|
|
|
|
|
|
|
|
for tx in state.world_state.transaction_sequence: |
|
|
|
|
if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF: |
|
|
|
|
try: |
|
|
|
|
|
|
|
|
|
# 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. |
|
|
|
|
transaction_sequence = solver.get_transaction_sequence(state, constraints) |
|
|
|
|
|
|
|
|
|
constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)] |
|
|
|
|
eth_sent_total = Sum(eth_sent_total, tx.call_value) |
|
|
|
|
debug = str(transaction_sequence) |
|
|
|
|
|
|
|
|
|
constraints += [ |
|
|
|
|
UGT(call_value, eth_sent_total), |
|
|
|
|
target == state.environment.sender, |
|
|
|
|
] |
|
|
|
|
issue = Issue( |
|
|
|
|
contract=node.contract_name, |
|
|
|
|
function_name=node.function_name, |
|
|
|
|
address=instruction["address"], |
|
|
|
|
swc_id=UNPROTECTED_ETHER_WITHDRAWAL, |
|
|
|
|
title="Ether thief", |
|
|
|
|
_type="Warning", |
|
|
|
|
bytecode=state.environment.code.bytecode, |
|
|
|
|
description="Arbitrary senders other than the contract creator can withdraw ETH from the contract" |
|
|
|
|
+ " account without previously having sent an equivalent amount of ETH to it. This is likely to be" |
|
|
|
|
+ " a vulnerability.", |
|
|
|
|
debug=debug, |
|
|
|
|
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
|
|
|
|
) |
|
|
|
|
except UnsatError: |
|
|
|
|
logging.debug("[ETHER_THIEF] no model found") |
|
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
return [issue] |
|
|
|
|
|
|
|
|
|
transaction_sequence = solver.get_transaction_sequence(state, constraints) |
|
|
|
|
|
|
|
|
|
debug = str(transaction_sequence) |
|
|
|
|
class EtherThief(DetectionModule): |
|
|
|
|
def __init__(self): |
|
|
|
|
super().__init__( |
|
|
|
|
name="Ether Thief", |
|
|
|
|
swc_id=UNPROTECTED_ETHER_WITHDRAWAL, |
|
|
|
|
hooks=["CALL"], |
|
|
|
|
description=DESCRIPTION, |
|
|
|
|
entrypoint="callback", |
|
|
|
|
) |
|
|
|
|
self._issues = [] |
|
|
|
|
|
|
|
|
|
issue = Issue( |
|
|
|
|
contract=node.contract_name, |
|
|
|
|
function_name=node.function_name, |
|
|
|
|
address=instruction["address"], |
|
|
|
|
swc_id=UNPROTECTED_ETHER_WITHDRAWAL, |
|
|
|
|
title="Ether thief", |
|
|
|
|
_type="Warning", |
|
|
|
|
bytecode=state.environment.code.bytecode, |
|
|
|
|
description="Arbitrary senders other than the contract creator can withdraw ETH from the contract" |
|
|
|
|
+ " account without previously having sent an equivalent amount of ETH to it. This is likely to be" |
|
|
|
|
+ " a vulnerability.", |
|
|
|
|
debug=debug, |
|
|
|
|
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
|
|
|
|
) |
|
|
|
|
issues.append(issue) |
|
|
|
|
except UnsatError: |
|
|
|
|
logging.debug("[ETHER_THIEF] no model found") |
|
|
|
|
def execute(self, state: GlobalState): |
|
|
|
|
self._issues.extend(_analyze_state(state)) |
|
|
|
|
return self.issues |
|
|
|
|
|
|
|
|
|
return issues |
|
|
|
|
@property |
|
|
|
|
def issues(self): |
|
|
|
|
return self._issues |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
detector = EtherThief() |
|
|
|
|