From b08a9d9d84d8159dd3a3665498bb4ec098a12db4 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 7 Aug 2019 12:00:18 -0700 Subject: [PATCH 1/2] Constrain all transaction callers to have <= 1000 ETH --- mythril/analysis/solver.py | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 82e3f2ee..8755c6c5 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -8,7 +8,7 @@ from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.transaction import BaseTransaction -from mythril.laser.smt import UGE, Optimize, symbol_factory +from mythril.laser.smt import UGE, Optimize, symbol_factory, simplify from mythril.laser.ethereum.time_handler import time_handler from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( @@ -197,15 +197,21 @@ def _set_minimisation_constraints( # Minimize minimize.append(transaction.call_data.calldatasize) + constraints.append( + UGE( + symbol_factory.BitVecVal(1000000000000000000000, 256), + world_state.starting_balances[transaction.caller], + ) + ) + for account in world_state.accounts.values(): # Lazy way to prevent overflows and to ensure "reasonable" balances # Each account starts with less than 100 ETH - if account.address.symbolic: - constraints.append( - UGE( - symbol_factory.BitVecVal(100000000000000000000, 256), - world_state.starting_balances[account.address], - ) + constraints.append( + UGE( + symbol_factory.BitVecVal(100000000000000000000, 256), + world_state.starting_balances[account.address], ) + ) return constraints, tuple(minimize) From 4bfaadea98bed96a7b4b9385614c99eb74f66261 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 7 Aug 2019 12:03:17 -0700 Subject: [PATCH 2/2] Remove unneeded import --- mythril/analysis/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 8755c6c5..3358d537 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -8,7 +8,7 @@ from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.transaction import BaseTransaction -from mythril.laser.smt import UGE, Optimize, symbol_factory, simplify +from mythril.laser.smt import UGE, Optimize, symbol_factory from mythril.laser.ethereum.time_handler import time_handler from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import (