Use symbolic storage for concrete=False (#1039)

mythril/laser/ethereum/state/account.py

@@ -47,9 +47,13 @@ class Storage:
                     return self._storage[item]
                 except ValueError:
                     pass
+
         if self.concrete:
             return symbol_factory.BitVecVal(0, 256)
-        self._storage[item] = symbol_factory.BitVecVal(0, 256)
+
+        self._storage[item] = symbol_factory.BitVecSym(
+            "storage_{}_{}".format(str(item), str(self.address)), 256
+        )
         return self._storage[item]
 
     def __setitem__(self, key: Union[int, str], value: Any) -> None:

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

@@ -5,14 +5,14 @@
             "address": 661,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
-            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "thisisfine()",
             "max_gas_used": 1254,
             "min_gas_used": 643,
-            "severity": "Low",
+            "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To Fixed Address"
+            "title": "External Call To User-Supplied Address"
         },
         {
             "address": 661,
@@ -31,14 +31,14 @@
             "address": 779,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
-            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "callstoredaddress()",
             "max_gas_used": 1298,
             "min_gas_used": 687,
-            "severity": "Low",
+            "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To Fixed Address"
+            "title": "External Call To User-Supplied Address"
         },
         {
             "address": 779,
@@ -57,14 +57,14 @@
             "address": 858,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
-            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "reentrancy()",
             "max_gas_used": 1320,
             "min_gas_used": 709,
-            "severity": "Low",
+            "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To Fixed Address"
+            "title": "External Call To User-Supplied Address"
         },
         {
             "address": 858,
@@ -87,7 +87,7 @@
             "function": "reentrancy()",
             "max_gas_used": null,
             "min_gas_used": null,
-            "severity": "Low",
+            "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
             "title": "State change after external call"

tests/testdata/outputs_expected/calls.sol.o.jsonv2

@@ -3,8 +3,8 @@
         "issues": [
             {
                 "description": {
-                    "head": "The contract executes an external message call.",
+                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
+                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
                     "discoveryTime": "<DISCOVERY-TIME-DATA>"
@@ -14,14 +14,14 @@
                         "sourceMap": "661:1:0"
                     }
                 ],
-                "severity": "Low",
+                "severity": "Medium",
                 "swcID": "SWC-107",
                 "swcTitle": "Reentrancy"
             },
             {
                 "description": {
-                    "head": "The contract executes an external message call.",
+                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
+                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
                     "discoveryTime": "<DISCOVERY-TIME-DATA>"
@@ -31,14 +31,14 @@
                         "sourceMap": "779:1:0"
                     }
                 ],
-                "severity": "Low",
+                "severity": "Medium",
                 "swcID": "SWC-107",
                 "swcTitle": "Reentrancy"
             },
             {
                 "description": {
-                    "head": "The contract executes an external message call.",
+                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
+                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
                     "discoveryTime": "<DISCOVERY-TIME-DATA>"
@@ -48,7 +48,7 @@
                         "sourceMap": "858:1:0"
                     }
                 ],
-                "severity": "Low",
+                "severity": "Medium",
                 "swcID": "SWC-107",
                 "swcTitle": "Reentrancy"
             },
@@ -82,7 +82,7 @@
                         "sourceMap": "869:1:0"
                     }
                 ],
-                "severity": "Low",
+                "severity": "Medium",
                 "swcID": "SWC-107",
                 "swcTitle": "Reentrancy"
             },

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

@@ -1,8 +1,8 @@
 # Analysis results for test-filename.sol
 
-## External Call To Fixed Address
+## External Call To User-Supplied Address
 - SWC ID: 107
-- Severity: Low
+- Severity: Medium
 - Contract: Unknown
 - Function name: `thisisfine()`
 - PC address: 661
@@ -10,8 +10,8 @@
 
 ### Description
 
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
 ## Unchecked Call Return Value
 - SWC ID: 104
@@ -26,9 +26,9 @@ An external function call to a fixed contract address is executed. Make sure tha
 The return value of a message call is not checked.
 External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.
 
-## External Call To Fixed Address
+## External Call To User-Supplied Address
 - SWC ID: 107
-- Severity: Low
+- Severity: Medium
 - Contract: Unknown
 - Function name: `callstoredaddress()`
 - PC address: 779
@@ -36,8 +36,8 @@ External calls return a boolean value. If the callee contract halts with an exce
 
 ### Description
 
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
 ## Unchecked Call Return Value
 - SWC ID: 104
@@ -52,9 +52,9 @@ An external function call to a fixed contract address is executed. Make sure tha
 The return value of a message call is not checked.
 External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.
 
-## External Call To Fixed Address
+## External Call To User-Supplied Address
 - SWC ID: 107
-- Severity: Low
+- Severity: Medium
 - Contract: Unknown
 - Function name: `reentrancy()`
 - PC address: 858
@@ -62,8 +62,8 @@ External calls return a boolean value. If the callee contract halts with an exce
 
 ### Description
 
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
 ## Unchecked Call Return Value
 - SWC ID: 104
@@ -80,7 +80,7 @@ External calls return a boolean value. If the callee contract halts with an exce
 
 ## State change after external call
 - SWC ID: 107
-- Severity: Low
+- Severity: Medium
 - Contract: Unknown
 - Function name: `reentrancy()`
 - PC address: 869

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

@@ -1,12 +1,12 @@
-==== External Call To Fixed Address ====
+==== External Call To User-Supplied Address ====
 SWC ID: 107
-Severity: Low
+Severity: Medium
 Contract: Unknown
 Function name: thisisfine()
 PC address: 661
 Estimated Gas Usage: 643 - 1254
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
 ==== Unchecked Call Return Value ====
@@ -20,15 +20,15 @@ The return value of a message call is not checked.
 External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.
 --------------------
 
-==== External Call To Fixed Address ====
+==== External Call To User-Supplied Address ====
 SWC ID: 107
-Severity: Low
+Severity: Medium
 Contract: Unknown
 Function name: callstoredaddress()
 PC address: 779
 Estimated Gas Usage: 687 - 1298
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
 ==== Unchecked Call Return Value ====
@@ -42,15 +42,15 @@ The return value of a message call is not checked.
 External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.
 --------------------
 
-==== External Call To Fixed Address ====
+==== External Call To User-Supplied Address ====
 SWC ID: 107
-Severity: Low
+Severity: Medium
 Contract: Unknown
 Function name: reentrancy()
 PC address: 858
 Estimated Gas Usage: 709 - 1320
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
 ==== Unchecked Call Return Value ====
@@ -66,7 +66,7 @@ External calls return a boolean value. If the callee contract halts with an exce
 
 ==== State change after external call ====
 SWC ID: 107
-Severity: Low
+Severity: Medium
 Contract: Unknown
 Function name: reentrancy()
 PC address: 869

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

@@ -1,5 +1,32 @@
 {
     "error": null,
-    "issues": [],
+    "issues": [
+        {
+            "address": 722,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "Anyone can withdraw ETH from the contract account.\nArbitrary 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()",
+            "max_gas_used": 1749,
+            "min_gas_used": 1138,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "105",
+            "title": "Unprotected Ether Withdrawal"
+        },
+        {
+            "address": 883,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
+            "function": "invest()",
+            "max_gas_used": 26883,
+            "min_gas_used": 6598,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow"
+        }
+    ],
     "success": true
 }

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

@@ -1,6 +1,41 @@
 [
     {
-        "issues": [],
+        "issues": [
+            {
+                "description": {
+                    "head": "Anyone can withdraw ETH from the contract account.",
+                    "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."
+                },
+                "extra": {
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "722:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-105",
+                "swcTitle": "Unprotected Ether Withdrawal"
+            },
+            {
+                "description": {
+                    "head": "The binary addition can overflow.",
+                    "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
+                },
+                "extra": {
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "883:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
+            }
+        ],
         "meta": {},
         "sourceFormat": "evm-byzantium-bytecode",
         "sourceList": [

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

@@ -1,3 +1,27 @@
-# Analysis results for None
+# Analysis results for test-filename.sol
 
-The analysis was completed successfully. No issues were detected.
+## Unprotected Ether Withdrawal
+- SWC ID: 105
+- Severity: High
+- Contract: Unknown
+- Function name: `withdrawfunds()`
+- PC address: 722
+- Estimated Gas Usage: 1138 - 1749
+
+### Description
+
+Anyone can withdraw ETH from the contract account.
+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
+- Severity: High
+- Contract: Unknown
+- Function name: `invest()`
+- PC address: 883
+- Estimated Gas Usage: 6598 - 26883
+
+### Description
+
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.

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

@@ -1 +1,22 @@
-The analysis was completed successfully. No issues were detected.
+==== Unprotected Ether Withdrawal ====
+SWC ID: 105
+Severity: High
+Contract: Unknown
+Function name: withdrawfunds()
+PC address: 722
+Estimated Gas Usage: 1138 - 1749
+Anyone can withdraw ETH from the contract account.
+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
+Severity: High
+Contract: Unknown
+Function name: invest()
+PC address: 883
+Estimated Gas Usage: 6598 - 26883
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
+--------------------
+

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

@@ -5,27 +5,27 @@
             "address": 196,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
-            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "callchecked()",
             "max_gas_used": 1210,
             "min_gas_used": 599,
-            "severity": "Low",
+            "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To Fixed Address"
+            "title": "External Call To User-Supplied Address"
         },
         {
             "address": 285,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
-            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
             "function": "callnotchecked()",
             "max_gas_used": 1232,
             "min_gas_used": 621,
-            "severity": "Low",
+            "severity": "Medium",
             "sourceMap": null,
             "swc-id": "107",
-            "title": "External Call To Fixed Address"
+            "title": "External Call To User-Supplied Address"
         },
         {
             "address": 285,

tests/testdata/outputs_expected/returnvalue.sol.o.jsonv2

@@ -3,8 +3,8 @@
         "issues": [
             {
                 "description": {
-                    "head": "The contract executes an external message call.",
+                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
+                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
                     "discoveryTime": "<DISCOVERY-TIME-DATA>"
@@ -14,14 +14,14 @@
                         "sourceMap": "196:1:0"
                     }
                 ],
-                "severity": "Low",
+                "severity": "Medium",
                 "swcID": "SWC-107",
                 "swcTitle": "Reentrancy"
             },
             {
                 "description": {
-                    "head": "The contract executes an external message call.",
+                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
+                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."
                 },
                 "extra": {
                     "discoveryTime": "<DISCOVERY-TIME-DATA>"
@@ -31,7 +31,7 @@
                         "sourceMap": "285:1:0"
                     }
                 ],
-                "severity": "Low",
+                "severity": "Medium",
                 "swcID": "SWC-107",
                 "swcTitle": "Reentrancy"
             },

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

@@ -1,8 +1,8 @@
 # Analysis results for test-filename.sol
 
-## External Call To Fixed Address
+## External Call To User-Supplied Address
 - SWC ID: 107
-- Severity: Low
+- Severity: Medium
 - Contract: Unknown
 - Function name: `callchecked()`
 - PC address: 196
@@ -10,12 +10,12 @@
 
 ### Description
 
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
-## External Call To Fixed Address
+## External Call To User-Supplied Address
 - SWC ID: 107
-- Severity: Low
+- Severity: Medium
 - Contract: Unknown
 - Function name: `callnotchecked()`
 - PC address: 285
@@ -23,8 +23,8 @@ An external function call to a fixed contract address is executed. Make sure tha
 
 ### Description
 
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
 ## Unchecked Call Return Value
 - SWC ID: 104

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

@@ -1,23 +1,23 @@
-==== External Call To Fixed Address ====
+==== External Call To User-Supplied Address ====
 SWC ID: 107
-Severity: Low
+Severity: Medium
 Contract: Unknown
 Function name: callchecked()
 PC address: 196
 Estimated Gas Usage: 599 - 1210
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
-==== External Call To Fixed Address ====
+==== External Call To User-Supplied Address ====
 SWC ID: 107
-Severity: Low
+Severity: Medium
 Contract: Unknown
 Function name: callnotchecked()
 PC address: 285
 Estimated Gas Usage: 621 - 1232
-The contract executes an external message call.
+A call to a user-supplied address is executed.
-An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
 ==== Unchecked Call Return Value ====