Merge pull request #715 from ConsenSys/ether_send_improvement

Baby steps to a better Ether Thief

mythril/analysis/modules/ether_thief.py

@@ -5,6 +5,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
 import logging
 
 
@@ -12,14 +13,12 @@ DESCRIPTION = """
 
 Search for cases where Ether can be withdrawn to a user-specified address. 
 
-An issue is reported ONLY IF:
+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 has not previously sent any ETH to the contract account.
-
-This is somewhat coarse and needs to be refined in the future.
+- The sender can withdraw *more* than the total amount they sent over all transactions.
 
 """
 
@@ -61,18 +60,18 @@ class EtherThief(DetectionModule):
         if constrained:
             return []
 
-        try:
+        eth_sent_total = BitVecVal(0, 256)
+
+        for tx in state.world_state.transaction_sequence[1:]:
+            eth_sent_total += tx.call_value
 
-            """
-            FIXME: Instead of solving for call_value > 0, check whether call value can be greater than
-            the total value of all transactions received by the caller
-            """
+        try:
 
             model = solver.get_model(
                 node.constraints
                 + not_creator_constraints
                 + [
-                    call_value > 0,
+                    UGT(call_value, eth_sent_total),
                     state.environment.sender == ARBITRARY_SENDER_ADDRESS,
                     target == state.environment.sender,
                 ]
@@ -83,18 +82,12 @@ class EtherThief(DetectionModule):
                 node.constraints
                 + not_creator_constraints
                 + [
-                    call_value > 0,
+                    call_value > eth_sent_total,
                     state.environment.sender == ARBITRARY_SENDER_ADDRESS,
                     target == state.environment.sender,
                 ],
             )
 
-            # For now we only report an issue if zero ETH has been sent to the contract account.
-
-            for key, value in transaction_sequence.items():
-                if int(value["call_value"], 16) > 0:
-                    return []
-
             debug = "Transaction Sequence: " + str(transaction_sequence)
 
             issue = Issue(
@@ -105,8 +98,9 @@ class EtherThief(DetectionModule):
                 title="Ether thief",
                 _type="Warning",
                 bytecode=state.environment.code.bytecode,
-                description="Users other than the contract creator can withdraw ETH from the contract account"
-                + " without previously having sent any ETH to it. This is likely to be vulnerability.",
+                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),
             )

tests/testdata/outputs_expected/ether_send.sol.o.json

@@ -5,11 +5,11 @@
       "address": 722,
       "contract": "Unknown",
       "debug": "<DEBUG-DATA>",
-      "description": "Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.",
+      "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.",
       "function": "withdrawfunds()",
-      "swc-id": "105",
-      "min_gas_used": 1138,
       "max_gas_used": 1749,
+      "min_gas_used": 1138,
+      "swc-id": "105",
       "title": "Ether thief",
       "type": "Warning"
     },
@@ -19,9 +19,9 @@
       "debug": "<DEBUG-DATA>",
       "description": "This binary add operation can result in integer overflow.\n",
       "function": "invest()",
-      "swc-id": "101",
-      "min_gas_used": 1571,
       "max_gas_used": 1856,
+      "min_gas_used": 1571,
+      "swc-id": "101",
       "title": "Integer Overflow",
       "type": "Warning"
     }

tests/testdata/outputs_expected/ether_send.sol.o.markdown

@@ -10,7 +10,7 @@
 
 ### Description
 
-Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
+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.
 
 ## Integer Overflow
 - SWC ID: 101

tests/testdata/outputs_expected/ether_send.sol.o.text

@@ -5,7 +5,7 @@ Contract: Unknown
 Function name: withdrawfunds()
 PC address: 722
 Estimated Gas Usage: 1138 - 1749
-Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
+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.
 --------------------
 
 ==== Integer Overflow ====

tests/testdata/outputs_expected/multi_contracts.sol.o.json

@@ -5,11 +5,11 @@
       "address": 142,
       "contract": "Unknown",
       "debug": "<DEBUG-DATA>",
-      "description": "Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.",
+      "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.",
       "function": "transfer()",
-      "swc-id": "105",
-      "min_gas_used": 186,
       "max_gas_used": 467,
+      "min_gas_used": 186,
+      "swc-id": "105",
       "title": "Ether thief",
       "type": "Warning"
     }

tests/testdata/outputs_expected/multi_contracts.sol.o.markdown

@@ -10,4 +10,4 @@
 
 ### Description
 
-Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
+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.

tests/testdata/outputs_expected/multi_contracts.sol.o.text

@@ -5,6 +5,6 @@ Contract: Unknown
 Function name: transfer()
 PC address: 142
 Estimated Gas Usage: 186 - 467
-Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
+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.
 --------------------