Symbol friendly fake hash replacement for evm sha3 (#1549)

* Okay, boring fakehash added

* Correctness oriented default

* blkn

* sha3type sound default

* Stack is not simplified by default

* better log

* read/write mem black

* .

* Delete test workspace

Author: feliam

manticore/core/state.py

@@ -311,13 +311,19 @@ def must_be_true(self, expr):
             self._constraints, expr == False
         )
 
-    def solve_one(self, *exprs, constrain=False):
+    def solve_one(self, expr, constrain=False):
+        """
+        A version of solver_one_n for a single expression. See solve_one_n.
+        """
+        return self.solve_one_n(expr, constrain=constrain)[0]
+
+    def solve_one_n(self, *exprs, constrain=False):
         """
         Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into
         one solution.
 
-        :param exprs: Symbolic value to concretize. An iterable of manticore.core.smtlib.Expression
-        :param bool constrain: If True, constrain expr to concretized value
+        :param exprs: An iterable of manticore.core.smtlib.Expression
+        :param bool constrain: If True, constrain expr to solved solution value
         :return: Concrete value or a tuple of concrete values
         :rtype: int
         """
@@ -334,8 +340,6 @@ def solve_one(self, *exprs, constrain=False):
                 if isinstance(value, bytearray):
                     value = bytes(value)
                 values.append(value)
-        if len(exprs) == 1:
-            values = values[0]
         return values
 
     def solve_n(self, expr, nsolves):

manticore/ethereum/detectors.py

@@ -661,27 +661,29 @@ class DetectUninitializedMemory(Detector):
     IMPACT = DetectorClassification.MEDIUM
     CONFIDENCE = DetectorClassification.HIGH
 
-    def did_evm_read_memory_callback(self, state, offset, value):
+    def did_evm_read_memory_callback(self, state, offset, value, size):
         initialized_memory = state.context.get("{:s}.initialized_memory".format(self.name), set())
         cbu = True  # Can be unknown
         current_contract = state.platform.current_vm.address
         for known_contract, known_offset in initialized_memory:
             if current_contract == known_contract:
-                cbu = Operators.AND(cbu, offset != known_offset)
+                for offset_i in range(offset, offset + size):
+                    cbu = Operators.AND(cbu, offset_i != known_offset)
         if state.can_be_true(cbu):
             self.add_finding_here(
                 state,
                 "Potentially reading uninitialized memory at instruction (address: %r, offset %r)"
                 % (current_contract, offset),
             )
 
-    def did_evm_write_memory_callback(self, state, offset, value):
+    def did_evm_write_memory_callback(self, state, offset, value, size):
         current_contract = state.platform.current_vm.address
 
         # concrete or symbolic write
-        state.context.setdefault("{:s}.initialized_memory".format(self.name), set()).add(
-            (current_contract, offset)
-        )
+        for offset_i in range(offset, offset + size):
+            state.context.setdefault("{:s}.initialized_memory".format(self.name), set()).add(
+                (current_contract, offset)
+            )
 
 
 class DetectUninitializedStorage(Detector):

manticore/ethereum/manticore.py

@@ -50,6 +50,7 @@ class Sha3Type(Enum):
 
     concretize = "concretize"
     symbolicate = "symbolicate"
+    fake = "fake"
 
     def title(self):
         return self._name_.title()
@@ -64,7 +65,7 @@ def from_string(cls, name):
 consts.add(
     "sha3",
     default=Sha3Type.symbolicate,
-    description="concretize: sound simple concretization\nsymbolicate(*): unsound symbolication with out of cycle false positive killing",
+    description="concretize: sound simple concretization\nsymbolicate(*): unsound symbolication with an out of cycle false positive killing\nfake: using a symbol friendly fake hash (This potentially produces wrong testcases) ",
 )
 consts.add(
     "sha3timeout",
@@ -403,8 +404,6 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
             self.subscribe("on_symbolic_function", self._on_concretize)
         elif consts.sha3 is consts.sha3.symbolicate:
             self.subscribe("on_symbolic_function", self.on_unsound_symbolication)
-        else:
-            raise NotImplemented
 
         self._accounts: Dict[str, EVMContract] = dict()
         self._serializer = PickleSerializer()
@@ -625,7 +624,7 @@ def solidity_create_contract(
         for state in self.ready_states:
             if state.platform.get_code(int(contract_account)):
                 return contract_account
-        logger.info("Failed to compile contract", contract_names)
+        logger.info("Failed to compile contract %r", contract_names)
         return None
 
     def get_nonce(self, address):
@@ -1182,15 +1181,15 @@ def on_unsound_symbolication(self, state, func, data, result):
                 # if we found another pair that matches use that instead
                 # the duplicated pair is not added to symbolic_pairs
                 if state.must_be_true(Operators.OR(x == data, y == value)):
-                    constraint = simplify(Operators.AND(x == data, y == value))
+                    constraint = Operators.AND(x == data, y == value)
                     state.constrain(constraint)
                     data, value = x, y
                     break
             else:
                 # bijectiveness; new pair is added to symbolic_pairs
                 for x, y in symbolic_pairs:
                     if len(x) == len(data):
-                        constraint = simplify((x == data) == (y == value))
+                        constraint = (x == data) == (y == value)
                     else:
                         constraint = y != value
                     state.constrain(constraint)  # bijective
@@ -1261,9 +1260,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
                 for x_concrete, y_concrete in concrete_pairs:
                     if len(x) == len(x_concrete):  # If the size of the buffer wont
                         # match it does not matter
-                        unseen = Operators.AND(
-                            Operators.AND(x != x_concrete, y != y_concrete), unseen
-                        )
+                        unseen = Operators.AND(x != x_concrete, y != y_concrete, unseen)
                 # Search for a new unseen sha3 pair
                 with state as temp_state:
                     temp_state.constrain(unseen)

manticore/platforms/evm.py

@@ -749,6 +749,7 @@ def extend_with_zeroes(b):
         # Used calldata size
         self._used_calldata_size = 0
         self._valid_jmpdests = set()
+        self._sha3 = {}
 
     @property
     def pc(self):
@@ -777,6 +778,7 @@ def gas(self):
 
     def __getstate__(self):
         state = super().__getstate__()
+        state["sha3"] = self._sha3
         state["memory"] = self.memory
         state["world"] = self._world
         state["constraints"] = self.constraints
@@ -800,6 +802,7 @@ def __getstate__(self):
         return state
 
     def __setstate__(self, state):
+        self._sha3 = state["sha3"]
         self._checkpoint_data = state["_checkpoint_data"]
         self._published_pre_instruction_events = state["_published_pre_instruction_events"]
         self._on_transaction = state["_on_transaction"]
@@ -940,6 +943,7 @@ def _push(self, value):
         value = simplify(value)
         if isinstance(value, Constant) and not value.taint:
             value = value.value
+
         self.stack.append(value)
 
     def _top(self, n=0):
@@ -1065,9 +1069,6 @@ def _pop_arguments(self):
         for _ in range(current.pops):
             arguments.append(self._pop())
         # simplify stack arguments
-        for i, arg in enumerate(arguments):
-            if isinstance(arg, Constant) and not arg.taint:
-                arguments[i] = arg.value
         return arguments
 
     def _top_arguments(self):
@@ -1119,7 +1120,7 @@ def _checkpoint(self):
         if self._checkpoint_data is None:
             if not self._published_pre_instruction_events:
                 self._published_pre_instruction_events = True
-                self._publish("will_decode_instruction", self.pc)
+                # self._publish("will_decode_instruction", self.pc)
                 self._publish(
                     "will_evm_execute_instruction", self.instruction, self._top_arguments()
                 )
@@ -1154,7 +1155,7 @@ def _set_check_jmpdest(self, flag=True):
         Note that at this point `flag` can be the conditional from a JUMPI
         instruction hence potentially a symbolic value.
         """
-        self._check_jumpdest = simplify(flag)
+        self._check_jumpdest = flag
 
     def _check_jmpdest(self):
         """
@@ -1164,7 +1165,13 @@ def _check_jmpdest(self):
         Here, if symbolic, the conditional `self._check_jumpdest` would be
         already constrained to a single concrete value.
         """
-        should_check_jumpdest = self._check_jumpdest
+        # If pc is already pointing to a JUMPDEST thre is no need to check.
+        pc = self.pc.value if isinstance(self.pc, Constant) else self.pc
+        if pc in self._valid_jumpdests:
+            self._check_jumpdest = False
+            return
+
+        should_check_jumpdest = simplify(self._check_jumpdest)
         if isinstance(should_check_jumpdest, Constant):
             should_check_jumpdest = should_check_jumpdest.value
         elif issymbolic(should_check_jumpdest):
@@ -1176,11 +1183,10 @@ def _check_jmpdest(self):
             should_check_jumpdest = should_check_jumpdest_solutions[0]
 
         # If it can be solved only to False just set it False. If it can be solved
-        # only to True, process it and also se it to False
+        # only to True, process it and also set it to False
         self._check_jumpdest = False
 
         if should_check_jumpdest:
-            pc = self.pc.value if isinstance(self.pc, Constant) else self.pc
             if pc not in self._valid_jumpdests:
                 raise InvalidOpcode()
 
@@ -1235,7 +1241,6 @@ def setstate(state, value):
             last_pc, last_gas, instruction, arguments, fee, allocated = self._checkpoint()
             result = self._handler(*arguments)
             self._advance(result)
-
         except ConcretizeGas as ex:
 
             def setstate(state, value):
@@ -1324,19 +1329,13 @@ def _load(self, offset, size=1):
         except Exception:
             pass
 
-        for i in range(size):
-            self._publish(
-                "did_evm_read_memory", offset + i, Operators.EXTRACT(value, (size - i - 1) * 8, 8)
-            )
+        self._publish("did_evm_read_memory", offset, value, size)
         return value
 
     def _store(self, offset, value, size=1):
         """Stores value in memory as a big endian"""
         self.memory.write_BE(offset, value, size)
-        for i in range(size):
-            self._publish(
-                "did_evm_write_memory", offset + i, Operators.EXTRACT(value, (size - i - 1) * 8, 8)
-            )
+        self._publish("did_evm_write_memory", offset, value, size)
 
     def safe_add(self, a, b, *args):
         a = Operators.ZEXTEND(a, 512)
@@ -1575,7 +1574,24 @@ def SHA3(self, start, size):
 
         """
         data = self.read_buffer(start, size)
-        return self.world.symbolic_function(globalsha3, data)
+
+        if consts.sha3 == consts.sha3.fake:
+            # Fake hash selected. Replace with symbol friendly hash.
+            h = len(data) + 0x4141414141414141414141414141414141414141414141414141414141414100
+            for i in range(0, len(data), 32):
+                h <<= 16
+                h += data.read_BE(i, 32)
+
+            # Try to avoid some common incorrect cases
+            self.constraints.add(h != 0)
+            # Force fake collision resistance
+            for x, y in self._sha3.items():
+                self.constraints.add((data == x) == (h == y))
+
+            self._sha3[data] = h
+            return h
+        else:
+            return self.world.symbolic_function(globalsha3, data)
 
     ############################################################################
     # Environmental Information
@@ -1646,7 +1662,7 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
         memfee = self._get_memfee(mem_offset, size)
         return self.safe_add(copyfee, memfee)
 
-    # @concretized_args(size="SAMPLED")
+    # @concretized_args(size="ALL")
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
         # calldata_overflow = const.calldata_overflow
@@ -1680,10 +1696,6 @@ def CALLDATACOPY(self, mem_offset, data_offset, size):
                 logger.info(f"Constraining CALLDATACOPY size to {cap}")
                 max_size = cap
                 self.constraints.add(Operators.ULE(size, cap))
-                # cond = Operators.OR(size == 0, size==4)
-                # for conc_size in range(8,max_size, 32):
-                #   cond = Operators.OR(size==conc_size, cond)
-                # self.constraints.add(cond)
 
         for i in range(max_size):
             try:

tests/ethereum/EVM/test_EVMCALLDATALOAD.py

@@ -4,6 +4,7 @@
 from manticore.platforms import evm
 from manticore.core import state
 from manticore.core.smtlib import Operators, ConstraintSet
+from manticore.core.smtlib import simplify, to_constant
 import os
 
 
@@ -76,8 +77,8 @@ def test_CALLDATALOAD_2(self):
         last_exception, last_returned = self._execute(new_vm)
         self.assertEqual(last_exception, None)
         self.assertEqual(new_vm.pc, 1)
-        self.assertEqual(
-            new_vm.stack,
+        self.assertSequenceEqual(
+            list(map(to_constant, new_vm.stack)),
             [29515630589904128245223976570842015727304113738300535931626442982409229107200],
         )
 
@@ -101,8 +102,8 @@ def test_CALLDATALOAD_3(self):
         last_exception, last_returned = self._execute(new_vm)
         self.assertEqual(last_exception, None)
         self.assertEqual(new_vm.pc, 1)
-        self.assertEqual(
-            new_vm.stack,
+        self.assertSequenceEqual(
+            list(map(to_constant, new_vm.stack)),
             [29515630589904128245223976570842015727304113738300535931626442982409224847360],
         )
 
@@ -171,7 +172,7 @@ def test_CALLDATALOAD_6(self):
         self.assertEqual(last_exception, None)
         self.assertEqual(new_vm.pc, 1)
         self.assertEqual(
-            new_vm.stack,
+            list(map(to_constant, new_vm.stack)),
             [29515630589904128245223976570842010042800435681475029265659040150473943285760],
         )