VMTests tests for istanbul (#1676)

* New upstream auto-VMTests tests for istanbul

* Removed redundant tests

* bugfix

* Reset CI

* Debug CI 1

* debug CI

* wakey wakey GitHub Actions

* Poke GH

* Fix detector

* New CI weaky weaky

* Change default smtlib max memory usage weaky weaky

* ci weaky waky

* ci weaky waky

* CI waky weaky

* Fix test_general weaky weaky

* Fix ethtests. weaky waky

* Unittest driven bugfixes. weaky waky

* Avoid check-sat in the middle of a solving. weaky wakey

* Fix config. weaky wakey

* Reduce queries in IO detector

* CC

* CC

* fix nativve tests

* CC and solver defaults

* merge. weaky waky

* Fixing tests

* Remove debug print

* Fix in DetectUninitializedMemory

* Change truffle test state count

* CC

* Better forking on failed transactions

* CC

* Fix truffle tst state count

* Improve z3 speed

* Fix truffle test state count

* Change default gas concretization in CALL

* Better logging at fork

* Insane commit to fix several bugfixes and refator stuff

* black

* Fix selfdestruct test

* Fix some unittests

* Default to bytes fo constant calldata

* Fix tests

* Better doc

* https://github.com/trailofbits/manticore/pull/1676/files#r426927762

* https://github.com/trailofbits/manticore/pull/1676/files#r426946198

* Leave native alone and fix pyevmasm dep

* Update manticore/platforms/evm.py

Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>

* Update manticore/platforms/evm.py

Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>

* isSeven

* OPTI/PESI

* Truffle optimistic

* truffle fix

* Truffle state count

* CC

* Fix tests PESI/OPTI

* Update manticore/core/state.py

Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com>

* Better policy naming

* Update manticore/platforms/evm.py

Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com>

* Update manticore/ethereum/manticore.py

Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com>

* Update manticore/platforms/evm.py

Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com>

* PESi PESSI

* blkn

* weaky

* wakey wakey

* blkn

* unreachable

* Fix state count in checkpoint test (merge)

* remove unused exception var

Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Co-authored-by: Samuel E. Moelius <35515885+smoelius@users.noreply.github.com>

.github/workflows/ci.yml

@@ -118,8 +118,8 @@ jobs:
                 echo "Automaking VMTests" `pwd`
                 cd ./tests/ && mkdir -p  ethereum_vm/VMTests_concrete && mkdir -p ethereum_vm/VMTests_symbolic
                 rm -Rf vmtests; git clone https://github.com/ethereum/tests --depth=1 vmtests
-                for i in ./vmtests/VMTests/*; do python ./auto_generators/make_VMTests.py $i; done
-                for i in ./vmtests/VMTests/*; do python ./auto_generators/make_VMTests.py $i --symbolic; done
+                for i in ./vmtests/BlockchainTests/ValidBlocks/VMTests/*/*json; do python ./auto_generators/make_VMTests.py -f istanbul -i $i -o ethereum_vm/VMTests_concrete; done
+                rm ethereum_vm/VMTests_concrete/test_loop*.py #too slow
                 rm -rf ./vmtests
                 touch ethereum_vm/.done
             fi
@@ -157,11 +157,11 @@ jobs:
             mkdir truffle_tests
             cd truffle_tests
             truffle unbox metacoin
-            coverage run -m manticore . --contract MetaCoin --workspace output
+            coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic
             # Truffle smoke test. We test if manticore is able to generate states
             # from a truffle project. 
-            if [ "$(ls output/*tx -l | wc -l)" != "34" ]; then
-                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 34"
+            if [ "$(ls output/*tx -l | wc -l)" != "26" ]; then
+                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 26"
                 return 1
             fi
             echo "Truffle test succeded"

manticore/__init__.py

@@ -8,6 +8,7 @@
 from .utils.log import set_verbosity
 from .core.smtlib import issymbolic, istainted
 from .ethereum.manticore import ManticoreEVM
+from .core.plugin import Plugin
 from .exceptions import ManticoreError
 
 __all__ = [

manticore/core/smtlib/constraints.py

@@ -148,7 +148,7 @@ def __get_related(self, related_to=None):
                             break
 
                     variables = get_variables(constraint)
-                    if related_variables & variables:
+                    if related_variables & variables or not (variables):
                         remaining_constraints.remove(constraint)
                         related_constraints.add(constraint)
                         related_variables |= variables

manticore/core/smtlib/expression.py

@@ -159,6 +159,12 @@ def __rxor__(self, other):
         return BoolXor(self.cast(other), self)
 
     def __bool__(self):
+        # try to be forgiving. Allow user to use Bool in an IF sometimes
+        from .visitors import simplify
+
+        x = simplify(self)
+        if isinstance(x, Constant):
+            return x.value
         raise NotImplementedError("__bool__ for Bool")
 
 
@@ -479,7 +485,8 @@ class BitVecConstant(BitVec):
     __slots__ = ["_value"]
 
     def __init__(self, size: int, value: int, *args, **kwargs):
-        self._value = value
+        MASK = (1 << size) - 1
+        self._value = value & MASK
         super().__init__(size, *args, **kwargs)
 
     def __bool__(self):
@@ -798,6 +805,7 @@ def underlying_variable(self):
         return array
 
     def read_BE(self, address, size):
+        address = self.cast_index(address)
         bytes = []
         for offset in range(size):
             bytes.append(self.get(address + offset, 0))
@@ -1072,6 +1080,7 @@ def store(self, index, value):
             self._concrete_cache = {}
 
         # potentially generate and update .written set
+        # if index is symbolic it may overwrite other previous indexes
         self.written.add(index)
         self._array = self._array.store(index, value)
         return self
@@ -1150,11 +1159,21 @@ def is_known(self, index):
 
         is_known_index = BoolConstant(False)
         written = self.written
-        for known_index in written:
-            if isinstance(index, Constant) and isinstance(known_index, Constant):
-                if known_index.value == index.value:
+        if isinstance(index, Constant):
+            for i in written:
+                # check if the concrete index is explicitly in written
+                if isinstance(i, Constant) and index.value == i.value:
                     return BoolConstant(True)
+
+                # Build an expression to check if our concrete index could be the
+                # solution for anyof the used symbolic indexes
+                is_known_index = BoolOr(is_known_index.cast(index == i), is_known_index)
+            return is_known_index
+
+        # The index is symbolic we need to compare it agains it all
+        for known_index in written:
             is_known_index = BoolOr(is_known_index.cast(index == known_index), is_known_index)
+
         return is_known_index
 
     def get(self, index, default=None):
@@ -1171,12 +1190,15 @@ def get(self, index, default=None):
         if isinstance(index, Constant) and index.value in self._concrete_cache:
             return self._concrete_cache[index.value]
 
-        value = self._array.select(index)
-        if default is None:
-            return value
+        if default is not None:
+            default = self.cast_value(default)
+            is_known = self.is_known(index)
+            if isinstance(is_known, Constant) and is_known.value == False:
+                return default
+        else:
+            return self._array.select(index)
 
-        is_known = self.is_known(index)
-        default = self.cast_value(default)
+        value = self._array.select(index)
         return BitVecITE(self._array.value_bits, is_known, value, default)
 
 

manticore/core/smtlib/solver.py

@@ -32,8 +32,8 @@
 
 logger = logging.getLogger(__name__)
 consts = config.get_group("smt")
-consts.add("timeout", default=240, description="Timeout, in seconds, for each Z3 invocation")
-consts.add("memory", default=16384, description="Max memory for Z3 to use (in Megabytes)")
+consts.add("timeout", default=120, description="Timeout, in seconds, for each Z3 invocation")
+consts.add("memory", default=1024 * 8, description="Max memory for Z3 to use (in Megabytes)")
 consts.add(
     "maxsolutions",
     default=10000,
@@ -333,7 +333,6 @@ def _recv(self) -> str:
         buf = "".join(bufl).strip()
         if "(error" in bufl[0]:
             raise SolverException(f"Error in smtlib: {bufl[0]}")
-
         return buf
 
     def __readline_and_count(self) -> Tuple[str, int, int]:
@@ -450,6 +449,10 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
         expression = simplify(expression)
         if maxcnt is None:
             maxcnt = consts.maxsolutions
+            if isinstance(expression, Bool) and consts.maxsolutions > 1:
+                # We know there is max 2 solutions when Bool
+                maxcnt = 2
+                silent = True
 
         with constraints as temp_cs:
             if isinstance(expression, Bool):
@@ -470,12 +473,10 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
             temp_cs.add(var == expression)
             self._reset(temp_cs.to_string(related_to=var))
             result = []
-
             start = time.time()
             while self._is_sat():
                 value = self._getvalue(var)
                 result.append(value)
-                self._assert(var != value)
 
                 if len(result) >= maxcnt:
                     if silent:
@@ -487,8 +488,15 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                     else:
                         raise TooManySolutions(result)
                 if time.time() - start > consts.timeout:
+                    if silent:
+                        logger.info("Timeout searching for all solutions")
+                        return result
                     raise SolverError("Timeout")
-            return result
+                # Sometimes adding a new contraint after a check-sat eats all the mem
+                temp_cs.add(var != value)
+                self._reset(temp_cs.to_string(related_to=var))
+                # self._assert(var != value)
+            return list(result)
 
     def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10000):
         """

manticore/core/smtlib/visitors.py

@@ -285,7 +285,7 @@ def __init__(self, **kw):
         BitVecAdd: operator.__add__,
         BitVecSub: operator.__sub__,
         BitVecMul: operator.__mul__,
-        BitVecDiv: operator.__truediv__,
+        BitVecDiv: operator.__floordiv__,
         BitVecShiftLeft: operator.__lshift__,
         BitVecShiftRight: operator.__rshift__,
         BitVecAnd: operator.__and__,
@@ -325,12 +325,12 @@ def visit_BitVecSignExtend(self, expression, *operands):
             return operands[0]
 
     def visit_BitVecExtract(self, expression, *operands):
-        if all(isinstance(o, Constant) for o in expression.operands):
-            value = expression.operands[0].value
+        if all(isinstance(o, Constant) for o in operands):
+            value = operands[0].value
             begining = expression.begining
             end = expression.end
             value = value >> begining
-            mask = 2 ** (end - begining + 1) - 1
+            mask = (1 << (end - begining)) - 1
             value = value & mask
             return BitVecConstant(expression.size, value, taint=expression.taint)
 
@@ -618,6 +618,8 @@ def visit_BitVecExtract(self, expression, *operands):
                             new_operands.append(BitVecExtract(item, begining, item.size - begining))
                             size -= item.size - begining
                             begining = 0
+        elif isinstance(op, BitVecConstant):
+            return BitVecConstant(size, (op.value >> begining) & ~(1 << size))
 
         if isinstance(op, (BitVecAnd, BitVecOr, BitVecXor)):
             bitoperand_a, bitoperand_b = op.operands
@@ -767,7 +769,7 @@ def visit_Expression(self, expression, *operands):
         return expression
 
 
-arithmetic_simplifier_cache = CacheDict(max_size=150000, flush_perc=25)
+arithmetic_simplifier_cache = CacheDict(max_size=250000, flush_perc=25)
 
 
 @lru_cache(maxsize=128, typed=True)
@@ -919,10 +921,6 @@ def _visit_operation(self, expression, *operands):
     visit_BoolOperation = _visit_operation
     visit_BitVecOperation = _visit_operation
 
-    @property
-    def results(self):
-        raise SmtlibError("NOOO")
-
     @property
     def result(self):
         output = super().result

manticore/core/state.py

@@ -40,7 +40,7 @@ class Concretize(StateException):
 
     """
 
-    _ValidPolicies = ["MIN", "MAX", "MINMAX", "ALL", "SAMPLED", "ONE"]
+    _ValidPolicies = ["MIN", "MAX", "MINMAX", "ALL", "SAMPLED", "ONE", "PESSIMISTIC", "OPTIMISTIC"]
 
     def __init__(self, message, expression, setstate=None, policy=None, **kwargs):
         if policy is None:
@@ -296,6 +296,20 @@ def concretize(self, symbolic, policy, maxcount=7):
                 )
         elif policy == "ONE":
             vals = [self._solver.get_value(self._constraints, symbolic)]
+        elif policy == "OPTIMISTIC":
+            logger.info("Optimistic case when forking")
+            if self._solver.can_be_true(self._constraints, symbolic):
+                vals = (True,)
+            else:
+                # We assume the path constraint was feasible to begin with
+                vals = (False,)
+        elif policy == "PESSIMISTIC":
+            logger.info("Pessimistic case when forking")
+            if self._solver.can_be_true(self._constraints, symbolic == False):
+                vals = (False,)
+            else:
+                # We assume the path constraint was feasible to begin with
+                vals = (True,)
         else:
             assert policy == "ALL"
             vals = self._solver.get_all_values(

manticore/ethereum/account.py

@@ -113,12 +113,7 @@ def __getattr__(self, name):
         if name in self.__hashes:
 
             def f(
-                *args,
-                signature: Optional[str] = None,
-                caller=None,
-                value=0,
-                gas=0xFFFFFFFFFFFF,
-                **kwargs,
+                *args, signature: Optional[str] = None, caller=None, value=0, gas=210000, **kwargs
             ):
                 try:
                     if signature:

manticore/ethereum/detectors.py

@@ -171,6 +171,7 @@ class DetectExternalCallAndLeak(Detector):
     CONFIDENCE = DetectorClassification.HIGH
 
     def will_evm_execute_instruction_callback(self, state, instruction, arguments):
+
         if instruction.semantics == "CALL":
             dest_address = arguments[1]
             sent_value = arguments[2]
@@ -203,7 +204,7 @@ def will_evm_execute_instruction_callback(self, state, instruction, arguments):
                         )
             else:
                 if msg_sender == dest_address:
-                    self.add_finding_here(state, f"Reachable {msg} to sender")
+                    self.add_finding_here(state, f"Reachable {msg} to sender", True)
 
 
 class DetectInvalid(Detector):
@@ -329,7 +330,7 @@ def did_close_transaction_callback(self, state, tx):
             # Check is the tx was successful
             if tx.result:
                 # Check if gas was enough for a reentrancy attack
-                if tx.gas > 2300:
+                if state.can_be_true(Operators.UGE(tx.gas, 2300)):
                     # Check if target address is attaker controlled
                     if (
                         self._addresses is None
@@ -525,6 +526,8 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re
             iou = self._unsigned_sub_overflow(state, *arguments)
         elif mnemonic == "SSTORE":
             # If an overflowded value is stored in the storage then it is a finding
+            # Todo: save this in a stack and only do the check if this does not
+            #  revert/rollback
             where, what = arguments
             self._check_finding(state, what)
         elif mnemonic == "RETURN":
@@ -537,18 +540,18 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re
 
         if mnemonic in ("SLT", "SGT", "SDIV", "SMOD"):
             result = taint_with(result, "SIGNED")
-            vm.change_last_result(result)
-        if state.can_be_true(ios):
+        if mnemonic in ("ADD", "SUB", "MUL"):
             id_val = self._save_current_location(
                 state, "Signed integer overflow at %s instruction" % mnemonic, ios
             )
             result = taint_with(result, "IOS_{:s}".format(id_val))
-            vm.change_last_result(result)
-        if state.can_be_true(iou):
+
             id_val = self._save_current_location(
                 state, "Unsigned integer overflow at %s instruction" % mnemonic, iou
             )
             result = taint_with(result, "IOU_{:s}".format(id_val))
+
+        if mnemonic in ("SLT", "SGT", "SDIV", "SMOD", "ADD", "SUB", "MUL"):
             vm.change_last_result(result)
 
 
@@ -627,6 +630,11 @@ class DetectDelegatecall(Detector):
     IMPACT = DetectorClassification.HIGH
     CONFIDENCE = DetectorClassification.HIGH
 
+    def _to_constant(self, expression):
+        if isinstance(expression, Constant):
+            return expression.value
+        return expression
+
     def will_evm_execute_instruction_callback(self, state, instruction, arguments):
         world = state.platform
         mnemonic = instruction.semantics
@@ -643,6 +651,8 @@ def will_evm_execute_instruction_callback(self, state, instruction, arguments):
                 if len(possible_addresses) > 1:
                     self.add_finding_here(state, "Delegatecall to user controlled address")
 
+            in_offset = self._to_constant(in_offset)
+            in_size = self._to_constant(in_size)
             calldata = world.current_vm.read_buffer(in_offset, in_size)
             func_id = calldata[:4]
             if issymbolic(func_id):
@@ -667,8 +677,8 @@ def did_evm_read_memory_callback(self, state, offset, value, size):
         current_contract = state.platform.current_vm.address
         for known_contract, known_offset in initialized_memory:
             if current_contract == known_contract:
-                for offset_i in range(offset, offset + size):
-                    cbu = Operators.AND(cbu, offset_i != known_offset)
+                for offset_i in range(size):
+                    cbu = Operators.AND(cbu, (offset + offset_i) != known_offset)
         if state.can_be_true(cbu):
             self.add_finding_here(
                 state,
@@ -680,9 +690,9 @@ def did_evm_write_memory_callback(self, state, offset, value, size):
         current_contract = state.platform.current_vm.address
 
         # concrete or symbolic write
-        for offset_i in range(offset, offset + size):
+        for offset_i in range(size):
             state.context.setdefault("{:s}.initialized_memory".format(self.name), set()).add(
-                (current_contract, offset)
+                (current_contract, offset + offset_i)
             )
 
 
@@ -809,7 +819,7 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re
         world = state.platform
         curr_tx = world.current_transaction
 
-        if curr_tx.sort != "CREATE":
+        if curr_tx.sort != "CREATE" and curr_tx.address in self.manticore.metadata:
             metadata = self.manticore.metadata[curr_tx.address]
             curr_func = metadata.get_func_signature(state.solve_one(curr_tx.data[:4]))