Merge branch 'remove_branch_pruning' of github.com:ConsenSys/mythril into remove_branch_pruning

mythril/analysis/module/modules/ether_thief.py

@@ -11,24 +11,16 @@ 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.analysis import solver
-
+from mythril.exceptions import UnsatError
-from mythril.laser.smt import UGT, UGE
+from mythril.laser.smt import UGT
-from mythril.laser.smt.bool import And
 
 log = logging.getLogger(__name__)
 
 DESCRIPTION = """
-
 Search for cases where Ether can be withdrawn to a user-specified address.
-
+An issue is reported if there is a valid end state where the attacker has successfully
-An issue is reported if:
+increased their Ether balance.
-
-- 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 +32,7 @@ class EtherThief(DetectionModule):
     swc_id = UNPROTECTED_ETHER_WITHDRAWAL
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK
-    pre_hooks = ["STOP"]
+    post_hooks = ["CALL", "STATICCALL"]
 
     def reset_module(self):
         """
@@ -51,7 +43,6 @@ class EtherThief(DetectionModule):
 
     def _execute(self, state: GlobalState) -> None:
         """
-
         :param state:
         :return:
         """
@@ -64,7 +55,6 @@ class EtherThief(DetectionModule):
 
     def _analyze_state(self, state):
         """
-
         :param state:
         :return:
         """
@@ -73,15 +63,18 @@ class EtherThief(DetectionModule):
 
         constraints = copy(state.world_state.constraints)
 
-        attacker_address_bitvec = ACTORS.attacker
-
         constraints += [
             UGT(
-                state.world_state.balances[attacker_address_bitvec],
+                state.world_state.balances[ACTORS.attacker],
-                state.world_state.starting_balances[attacker_address_bitvec],
+                state.world_state.starting_balances[ACTORS.attacker],
             )
         ]
 
+        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,
@@ -92,13 +85,14 @@ 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"
+                + " account. This is likely to be a vulnerability.",
-            + " a vulnerability.",
                 detector=self,
                 constraints=constraints,
             )
 
             return [potential_issue]
+        except UnsatError:
+            return []
 
 
 detector = EtherThief()

mythril/laser/ethereum/plugins/implementations/mutation_pruner.py

@@ -5,10 +5,12 @@ 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,
 )
-from mythril.laser.smt import And, symbol_factory
+from mythril.analysis import solver
+from mythril.exceptions import UnsatError
 
 
 class MutationPruner(LaserPlugin):
@@ -38,6 +40,10 @@ 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())
@@ -48,17 +54,30 @@ class MutationPruner(LaserPlugin):
 
         @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
+
+            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 + [
+                    UGT(callvalue, symbol_factory.BitVecVal(0, 256))
+                ]
+
+                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:
                 raise PluginSkipWorldState

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