Merge pull request #1076 from ConsenSys/bugfix/bectoken

Fix Storage and calldata

mythril/laser/ethereum/instructions.py

@@ -768,18 +768,10 @@ class Instruction:
             size_sym = True
 
         if size_sym:
-            state.mem_extend(mstart, 1)
-            state.memory[mstart] = global_state.new_bitvec(
-                "calldata_"
-                + str(environment.active_account.contract_name)
-                + "["
-                + str(dstart)
-                + ": + "
-                + str(size)
-                + "]",
-                8,
-            )
-            return [global_state]
+            size = (
+                320
+            )  # This excess stuff will get overwritten as memory is dynamically sized
+
         size = cast(int, size)
         if size > 0:
             try:
@@ -1389,7 +1381,15 @@ class Instruction:
                 return self._sload_helper(global_state, str(index))
 
             storage_keys = global_state.environment.active_account.storage.keys()
-            keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
+            keys = filter(keccak_function_manager.is_keccak, storage_keys)
+            addr = global_state.get_current_instruction()["address"]
+            keccak_keys = [
+                key
+                for key in keys
+                if global_state.environment.active_account.storage.potential_func(
+                    key, addr
+                )
+            ]
 
             results = []  # type: List[GlobalState]
             constraints = []
@@ -1427,11 +1427,16 @@ class Instruction:
         :param constraints:
         :return:
         """
+        address = global_state.get_current_instruction()["address"]
         try:
-            data = global_state.environment.active_account.storage[index]
+            data = global_state.environment.active_account.storage.get(
+                index, addr=address
+            )
         except KeyError:
             data = global_state.new_bitvec("storage_" + str(index), 256)
-            global_state.environment.active_account.storage[index] = data
+            global_state.environment.active_account.storage.put(
+                key=index, value=data, addr=address
+            )
 
         if constraints is not None:
             global_state.mstate.constraints += constraints
@@ -1475,7 +1480,15 @@ class Instruction:
                 return self._sstore_helper(global_state, str(index), value)
 
             storage_keys = global_state.environment.active_account.storage.keys()
-            keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
+            keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
+            addr = global_state.get_current_instruction()["address"]
+            keccak_keys = [
+                key
+                for key in keccak_keys
+                if global_state.environment.active_account.storage.potential_func(
+                    key, addr
+                )
+            ]
 
             results = []  # type: List[GlobalState]
             new = symbol_factory.Bool(False)
@@ -1528,19 +1541,18 @@ class Instruction:
         :param constraint:
         :return:
         """
-        try:
         global_state.environment.active_account = deepcopy(
             global_state.environment.active_account
         )
         global_state.accounts[
             global_state.environment.active_account.address.value
         ] = global_state.environment.active_account
-
-            global_state.environment.active_account.storage[index] = (
-                value if not isinstance(value, Expression) else simplify(value)
+        address = global_state.get_current_instruction()["address"]
+        global_state.environment.active_account.storage.put(
+            key=index,
+            value=value if not isinstance(value, Expression) else simplify(value),
+            addr=address,
         )
-        except KeyError:
-            log.debug("Error writing to storage: Invalid index")
 
         if constraint is not None:
             global_state.mstate.constraints.append(constraint)

mythril/laser/ethereum/state/account.py

@@ -24,8 +24,12 @@ class Storage:
         self.concrete = concrete
         self.dynld = dynamic_loader
         self.address = address
+        self._storage_opcodes = {}  # type: Dict
 
-    def __getitem__(self, item: Union[str, int]) -> Any:
+    def get(self, item: Union[str, int], addr: int) -> Any:
+        if item not in self._storage_opcodes:
+            self._storage_opcodes[item] = set()
+        self._storage_opcodes[item].add(addr)
         try:
             return self._storage[item]
         except KeyError:
@@ -56,9 +60,17 @@ class Storage:
         )
         return self._storage[item]
 
-    def __setitem__(self, key: Union[int, str], value: Any) -> None:
+    def put(self, key: Union[int, str], value: Any, addr) -> None:
+        if key not in self._storage_opcodes:
+            self._storage_opcodes[key] = set()
+        self._storage_opcodes[key].add(addr)
         self._storage[key] = value
 
+    def potential_func(self, key, opcode) -> bool:
+        if key not in self._storage_opcodes:
+            return False
+        return opcode in self._storage_opcodes[key]
+
     def keys(self) -> KeysView:
         """
 

tests/laser/evm_testsuite/evm_test.py

@@ -125,7 +125,7 @@ def test_vmtest(
         account.code = Disassembly(details["code"][2:])
         account.nonce = int(details["nonce"], 16)
         for key, value in details["storage"].items():
-            account.storage[int(key, 16)] = int(value, 16)
+            account.storage.put(int(key, 16), int(value, 16), 10)
 
         world_state.put_account(account)
         account.set_balance(int(details["balance"], 16))
@@ -175,7 +175,7 @@ def test_vmtest(
 
             for index, value in details["storage"].items():
                 expected = int(value, 16)
-                actual = account.storage[int(index, 16)]
+                actual = account.storage.get(int(index, 16), 0)
 
                 if isinstance(actual, Expression):
                     actual = actual.value

tests/laser/state/storage_test.py

@@ -12,7 +12,7 @@ def test_concrete_storage_uninitialized_index(initial_storage, key):
     storage._storage = initial_storage
 
     # Act
-    value = storage[key]
+    value = storage.get(key, 0)
 
     # Assert
     assert value == 0
@@ -25,7 +25,7 @@ def test_symbolic_storage_uninitialized_index(initial_storage, key):
     storage._storage = initial_storage
 
     # Act
-    value = storage[key]
+    value = storage.get(key, 0)
 
     # Assert
     assert isinstance(value, Expression)
@@ -36,10 +36,10 @@ def test_storage_set_item():
     storage = Storage()
 
     # Act
-    storage[1] = 13
+    storage.put(key=1, value=13, addr=10)
 
     # Assert
-    assert storage[1] == 13
+    assert storage.get(item=1, addr=10) == 13
 
 
 def test_storage_change_item():
@@ -47,7 +47,7 @@ def test_storage_change_item():
     storage = Storage()
     storage._storage = {1: 12}
     # Act
-    storage[1] = 14
+    storage.put(key=1, value=14, addr=10)
 
     # Assert
-    assert storage[1] == 14
+    assert storage.get(item=1, addr=10) == 14

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

@@ -1,5 +1,19 @@
 {
     "error": null,
-    "issues": [],
+    "issues": [
+        {
+            "address": 498,
+            "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": "sendToken(address,uint256)",
+            "max_gas_used": 52806,
+            "min_gas_used": 11860,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow"
+        }
+    ],
     "success": true
 }

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

@@ -1,6 +1,24 @@
 [
     {
-        "issues": [],
+        "issues": [
+            {
+                "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": "498:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
+            }
+        ],
         "meta": {},
         "sourceFormat": "evm-byzantium-bytecode",
         "sourceList": [

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

@@ -1,3 +1,14 @@
-# Analysis results for None
+# Analysis results for test-filename.sol
 
-The analysis was completed successfully. No issues were detected.
+## Integer Overflow
+- SWC ID: 101
+- Severity: High
+- Contract: Unknown
+- Function name: `sendToken(address,uint256)`
+- PC address: 498
+- Estimated Gas Usage: 11860 - 52806
+
+### 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/metacoin.sol.o.text

@@ -1 +1,11 @@
-The analysis was completed successfully. No issues were detected.
+==== Integer Overflow ====
+SWC ID: 101
+Severity: High
+Contract: Unknown
+Function name: sendToken(address,uint256)
+PC address: 498
+Estimated Gas Usage: 11860 - 52806
+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.
+--------------------
+