From be289e7a0313985039d1d0d61f9980a3d8a1fff8 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 6 Mar 2020 15:30:39 +0100 Subject: [PATCH 01/11] Simplify EtherThief --- .../analysis/module/modules/ether_thief.py | 22 ++++++------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index be3939df..c4b0c8d0 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -11,24 +11,18 @@ from mythril.analysis.potential_issues import ( from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.ethereum.transaction import ContractCreationTransaction -from mythril.laser.smt import UGT, UGE -from mythril.laser.smt.bool import And +from mythril.laser.smt import UGT log = logging.getLogger(__name__) DESCRIPTION = """ - Search for cases where Ether can be withdrawn to a user-specified address. - An issue is reported if: - - The transaction sender does not match contract creator; - The sender address can be chosen arbitrarily; - The receiver address is identical to the sender address; - The sender can withdraw *more* than the total amount they sent over all transactions. - """ @@ -40,7 +34,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): """ @@ -51,7 +45,6 @@ class EtherThief(DetectionModule): def _execute(self, state: GlobalState) -> None: """ - :param state: :return: """ @@ -64,22 +57,21 @@ class EtherThief(DetectionModule): def _analyze_state(self, state): """ - :param state: :return: """ 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( From 7359a459900766dfc591ac40aec6b6bbcdcd13d9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 6 Mar 2020 16:28:24 +0100 Subject: [PATCH 02/11] Make module a posthook and remote 'to' constraint --- mythril/analysis/module/modules/ether_thief.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index c4b0c8d0..70231a7c 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -35,6 +35,7 @@ class EtherThief(DetectionModule): description = DESCRIPTION entry_point = EntryPoint.CALLBACK pre_hooks = ["CALL", "STATICCALL"] + post_hooks = ["CALL", "STATICCALL"] def reset_module(self): """ @@ -62,16 +63,19 @@ class EtherThief(DetectionModule): """ state = copy(state) instruction = state.get_current_instruction() - to = state.mstate.stack[-2] constraints = copy(state.world_state.constraints) + """ + Fixme: Potential issue should only be created it call target is the attacker. + This requires a prehook in addition to the posthook + """ + constraints += [ - to == ACTORS.attacker, UGT( state.world_state.balances[ACTORS.attacker], state.world_state.starting_balances[ACTORS.attacker], - ), + ) ] potential_issue = PotentialIssue( From e0c8e812f1ce710cfc74e247e9cd8c417d28213b Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 09:12:29 +0100 Subject: [PATCH 03/11] Remove prehook --- mythril/analysis/module/modules/ether_thief.py | 3 +-- mythril/laser/ethereum/transaction/symbolic.py | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index 70231a7c..c79accf8 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -34,7 +34,6 @@ class EtherThief(DetectionModule): swc_id = UNPROTECTED_ETHER_WITHDRAWAL description = DESCRIPTION entry_point = EntryPoint.CALLBACK - pre_hooks = ["CALL", "STATICCALL"] post_hooks = ["CALL", "STATICCALL"] def reset_module(self): @@ -67,7 +66,7 @@ class EtherThief(DetectionModule): constraints = copy(state.world_state.constraints) """ - Fixme: Potential issue should only be created it call target is the attacker. + FIXME: Potential issue should only be created it call target is the attacker. This requires a prehook in addition to the posthook """ diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index a5ee883d..505b6f9e 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -145,6 +145,7 @@ def execute_contract_creation( ) _setup_global_state_for_execution(laser_evm, transaction) new_account = new_account or transaction.callee_account + laser_evm.exec(True) return new_account From d6fc31ddda7b24c431a4cacf7b6dbfd6b789a308 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 09:14:46 +0100 Subject: [PATCH 04/11] Update description --- mythril/analysis/module/modules/ether_thief.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index c79accf8..39e9aa84 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -18,11 +18,8 @@ log = logging.getLogger(__name__) DESCRIPTION = """ Search for cases where Ether can be withdrawn to a user-specified address. -An issue is reported if: -- The transaction sender does not match contract creator; -- The sender address can be chosen arbitrarily; -- The receiver address is identical to the sender address; -- The sender can withdraw *more* than the total amount they sent over all transactions. +An issue is reported if there is a valid end state where the attacker has successfully +increased their Ether balance. """ From 417a42909e3b8ef6e037ac9c6af7154438ada4f9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 09:17:04 +0100 Subject: [PATCH 05/11] Update description text --- mythril/analysis/module/modules/ether_thief.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index 39e9aa84..9e579cd9 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -84,8 +84,7 @@ class EtherThief(DetectionModule): bytecode=state.environment.code.bytecode, description_head="Anyone can withdraw ETH from the contract account.", description_tail="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.", + + " account. This is likely to be a vulnerability.", detector=self, constraints=constraints, ) From 9cc8a5ca459d2ddeb654e9a2d4bf640c0958ec13 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 09:29:26 +0100 Subject: [PATCH 06/11] Clean up --- .../analysis/module/modules/ether_thief.py | 47 ++++++++++--------- 1 file changed, 25 insertions(+), 22 deletions(-) diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index 9e579cd9..54cb34d0 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -11,7 +11,8 @@ from mythril.analysis.potential_issues import ( from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.laser.ethereum.state.global_state import GlobalState - +from mythril.analysis import solver +from mythril.exceptions import UnsatError from mythril.laser.smt import UGT log = logging.getLogger(__name__) @@ -62,11 +63,6 @@ class EtherThief(DetectionModule): constraints = copy(state.world_state.constraints) - """ - FIXME: Potential issue should only be created it call target is the attacker. - This requires a prehook in addition to the posthook - """ - constraints += [ UGT( state.world_state.balances[ACTORS.attacker], @@ -74,22 +70,29 @@ class EtherThief(DetectionModule): ) ] - potential_issue = PotentialIssue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=instruction["address"], - swc_id=UNPROTECTED_ETHER_WITHDRAWAL, - title="Unprotected Ether Withdrawal", - severity="High", - bytecode=state.environment.code.bytecode, - description_head="Anyone can withdraw ETH from the contract account.", - description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" - + " account. This is likely to be a vulnerability.", - detector=self, - constraints=constraints, - ) - - return [potential_issue] + try: + # Pre-solve so we only add potential issues if the attacker's balance is increased. + + solver.get_model(constraints) + + potential_issue = PotentialIssue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=instruction["address"], + swc_id=UNPROTECTED_ETHER_WITHDRAWAL, + title="Unprotected Ether Withdrawal", + severity="High", + bytecode=state.environment.code.bytecode, + description_head="Anyone can withdraw ETH from the contract account.", + description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" + + " account. This is likely to be a vulnerability.", + detector=self, + constraints=constraints, + ) + + return [potential_issue] + except UnsatError: + return [] detector = EtherThief() From edae71dfc07c82afb0133daf8a7f2a51cf733ebf Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 12:32:47 +0100 Subject: [PATCH 07/11] Don't prune states that are reachable if callvalue > 0 --- .../implementations/mutation_pruner.py | 32 +++++++++---------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 02e55c7b..d1b49005 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -3,12 +3,14 @@ from mythril.laser.ethereum.plugins.plugin import LaserPlugin from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( MutationAnnotation, ) +from mythril.laser.smt.bitvec_helper import UGT from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) -from mythril.laser.smt import And, symbol_factory +from mythril.analysis import solver +from mythril.exceptions import UnsatError, CriticalError class MutationPruner(LaserPlugin): @@ -38,27 +40,23 @@ class MutationPruner(LaserPlugin): def sstore_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) - @symbolic_vm.pre_hook("CALL") - def call_mutator_hook(global_state: GlobalState): - global_state.annotate(MutationAnnotation()) - - @symbolic_vm.pre_hook("STATICCALL") - def staticcall_mutator_hook(global_state: GlobalState): - global_state.annotate(MutationAnnotation()) - @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): - if And( - *global_state.world_state.constraints[:] - + [ - global_state.environment.callvalue - > symbol_factory.BitVecVal(0, 256) - ] - ).is_false: - return + if isinstance( global_state.current_transaction, ContractCreationTransaction ): return + + try: + constraints = global_state.world_state.constraints + [ + global_state.environment.callvalue > 0 + ] + + solver.get_model(constraints) + return + except UnsatError: + pass + if len(list(global_state.get_annotations(MutationAnnotation))) == 0: raise PluginSkipWorldState From cdc4e6ef1615c7992a26d1b53a41010538909217 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 12:44:45 +0100 Subject: [PATCH 08/11] Reintroduce call mutator hooks to catch outgoing balance changes (+FIXME) --- .../plugins/implementations/mutation_pruner.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index d1b49005..aa36945c 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -40,6 +40,18 @@ class MutationPruner(LaserPlugin): def sstore_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + """FIXME: Check for changes in world_state.balances instead of adding MutationAnnotation for all calls. + Requires world_state.starting_balances to be initalized at every tx start *after* call value has been added. + """ + + @symbolic_vm.pre_hook("CALL") + def call_mutator_hook(global_state: GlobalState): + global_state.annotate(MutationAnnotation()) + + @symbolic_vm.pre_hook("STATICCALL") + def staticcall_mutator_hook(global_state: GlobalState): + global_state.annotate(MutationAnnotation()) + @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): From 534677ceff60ddf0c08b411357bc01cb9eb6c8b0 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 8 Mar 2020 12:53:39 +0100 Subject: [PATCH 09/11] Remove unused imports --- .../laser/ethereum/plugins/implementations/mutation_pruner.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index aa36945c..22d76c1b 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -3,14 +3,13 @@ from mythril.laser.ethereum.plugins.plugin import LaserPlugin from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( MutationAnnotation, ) -from mythril.laser.smt.bitvec_helper import UGT from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) from mythril.analysis import solver -from mythril.exceptions import UnsatError, CriticalError +from mythril.exceptions import UnsatError class MutationPruner(LaserPlugin): From 7638f2c688632fe2b68a70b3d5a8630fc66109b7 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 10 Mar 2020 16:06:14 +0100 Subject: [PATCH 10/11] Update mythril/laser/ethereum/plugins/implementations/mutation_pruner.py Co-Authored-By: JoranHonig --- .../laser/ethereum/plugins/implementations/mutation_pruner.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 22d76c1b..3213dd76 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -67,6 +67,7 @@ class MutationPruner(LaserPlugin): solver.get_model(constraints) return except UnsatError: + # callvalue is constrained to 0, therefore there is no balance based world state mutation pass if len(list(global_state.get_annotations(MutationAnnotation))) == 0: From 1f84fb1fc08c1e614d659967d107fd1645d40f79 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 10 Mar 2020 16:24:09 +0100 Subject: [PATCH 11/11] Use UGT comparison --- .../plugins/implementations/mutation_pruner.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 3213dd76..73963d3a 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -5,6 +5,7 @@ from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( ) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.svm import LaserEVM +from mythril.laser.smt import UGT, symbol_factory from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) @@ -59,9 +60,17 @@ class MutationPruner(LaserPlugin): ): return + if isinstance(global_state.environment.callvalue, int): + callvalue = symbol_factory.BitVecVal( + global_state.environment.callvalue, 256 + ) + else: + callvalue = global_state.environment.callvalue + try: + constraints = global_state.world_state.constraints + [ - global_state.environment.callvalue > 0 + UGT(callvalue, symbol_factory.BitVecVal(0, 256)) ] solver.get_model(constraints)