From f6dc874226910cdc2841bfe95a0f764a4841576a Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 26 Nov 2018 18:26:19 +0700 Subject: [PATCH] Return 0x00 for unitialized storage, Ether Thief fixes --- mythril/analysis/modules/ether_thief.py | 22 ++++++++++++++-------- mythril/laser/ethereum/state/account.py | 4 ++-- 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index f70973a1..90a6d402 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -4,7 +4,7 @@ from mythril.analysis.report import Issue from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.analysis.modules.base import DetectionModule from mythril.exceptions import UnsatError -from z3 import BitVecVal, UGT +from z3 import BitVecVal, UGT, Sum import logging @@ -55,16 +55,22 @@ class EtherThief(DetectionModule): eth_sent_total = BitVecVal(0, 256) - for tx in state.world_state.transaction_sequence[1:]: - eth_sent_total += tx.call_value + constraints = node.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 += [UGT(call_value, eth_sent_total), target == state.environment.sender] try: - transaction_sequence = solver.get_transaction_sequence( - state, - node.constraints - + [UGT(call_value, eth_sent_total), target == state.environment.sender], - ) + transaction_sequence = solver.get_transaction_sequence(state, constraints) debug = "Transaction Sequence: " + str(transaction_sequence) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 89a54586..0e51b524 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -1,6 +1,6 @@ from typing import Dict, Union, Any, KeysView -from z3 import BitVec, ExprRef +from z3 import BitVec, BitVecVal, ExprRef from mythril.disassembler.disassembly import Disassembly @@ -41,7 +41,7 @@ class Storage: pass if self.concrete: return 0 - self._storage[item] = BitVec("storage_" + str(item), 256) + self._storage[item] = BitVecVal(0, 256) return self._storage[item] def __setitem__(self, key: str, value: ExprRef) -> None: