[WIP] Check that a contract exists before calling it

manticore/__main__.py

@@ -120,6 +120,12 @@ def positive(value):
 
     parser.add_argument('--no-testcases', action='store_true',
                         help='Do not generate testcases for discovered states when analysis finishes (Ethereum only)')
+    parser.add_argument('--detect-callunexistant', action='store_true',
+                        help='Detects attemps to call empty code')
+
+
+    parser.add_argument('--verbose-trace', action='store_true',
+                        help='Dump an extra vervose trace for each state (Ethereum only)')
 
     parsed = parser.parse_args(sys.argv[1:])
     if parsed.procs <= 0:
@@ -134,7 +140,7 @@ def positive(value):
 
 
 def ethereum_cli(args):
-    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectReentrancySimple, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectDelegatecall, DetectExternalCallAndLeak, DetectReentrancySimple, DetectEnvInstruction
+    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectReentrancySimple, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectDelegatecall, DetectExternalCallAndLeak, DetectReentrancySimple, DetectEnvInstruction, DetectContractExistance, VerboseTrace
 
     log.init_logging()
 
@@ -160,6 +166,12 @@ def ethereum_cli(args):
         m.register_detector(DetectExternalCallAndLeak())
     if args.detect_all or args.detect_env_instr:
         m.register_detector(DetectEnvInstruction())
+    if args.detect_all or args.detect_callunexistant:
+        m.register_detector(DetectContractExistance())
+
+
+    if args.verbose_trace:
+        m.register_plugin(VerboseTrace())
 
     if args.limit_loops:
         m.register_plugin(LoopDepthLimiter())

manticore/ethereum.py

@@ -238,6 +238,20 @@ def _get_src(self, address, pc):
         return self.manticore.get_metadata(address).get_source_for(pc)
 
 
+class VerboseTrace(Plugin):
+    def will_evm_execute_instruction_callback(self, state, instruction, arguments):
+        world = state.platform
+        mnemonic = instruction.semantics
+        current_vm = world.current_vm
+        str_trace = state.context.get('str_trace',[])
+        str_trace.append(str(current_vm))
+        state.context['str_trace'] = str_trace
+
+    def on_finalize(self, state, testcase):
+        with testcase.open_stream('str_trace') as str_trace_f:
+            str_trace_f.write( '\n'.join(state.context.get('str_trace',[])))
+
+
 class DetectEnvInstruction(Detector):
     ''' Detect the usage of instructions that query environmental/block information:
         BLOCKHASH, COINBASE, TIMESTAMP, NUMBER, DIFFICULTY, GASLIMIT, ORIGIN, GASPRICE
@@ -641,6 +655,39 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re
                 self._remove_retval_taint(state, used_taint)
 
 
+class DetectContractExistance(Detector):
+    """ Detects unused return value from internal transactions """
+
+    def __init__(self, *args, **kwargs):
+        super().__init__(*args, **kwargs)
+
+    def will_evm_execute_instruction_callback(self, state, instruction, arguments):
+        world = state.platform
+        mnemonic = instruction.semantics
+        current_vm = world.current_vm
+        str_trace = state.context.get('str_trace',[])
+        str_trace.append(str(current_vm))
+        state.context['str_trace'] = str_trace
+
+    def did_close_transaction_callback(self, state, tx):
+        world = state.platform
+        # Check that all retvals were used in control flow
+        if not tx.is_human() and tx.return_value == 1:
+
+            code = world.get_code(tx.address)
+            #destinattion account has no code associated with it
+            if not code:
+                # But user send some calldata for processing. Probably a bug
+                if tx.data:
+                    self.add_finding_here(state, f"{tx.sort} with not empty calldata to and empty contract succeeded")
+                if tx.sort in {'DELEGATECALL', 'CALLCODE'}:  
+                    self.add_finding_here(state, f"{tx.sort} to and empty contract succeeded")
+
+
+    def on_finalize(self, state, testcase):
+        with testcase.open_stream('str_trace') as str_trace_f:
+            str_trace_f.write( '\n'.join(state.context.get('str_trace',[])))
+
 class DetectDelegatecall(Detector):
     '''
         Detects DELEGATECALLs to controlled addresses and or with controlled function id.
@@ -2455,11 +2502,26 @@ def _generate_testcase_callback(self, state, name, message=''):
         def flagged(flag):
             return '(*)' if flag else ''
         testcase = self._output.testcase(name.replace(' ', '_'))
+
+        # call on_finalize for each plugin
+        for plugin in self.plugins:
+            try:
+                plugin.on_finalize(state, testcase)
+            except AttributeError:
+                pass
+
         last_tx = blockchain.last_transaction
         if last_tx:
             message = message + last_tx.result
         logger.info("Generated testcase No. {} - {}".format(testcase.num, message))
 
+        for plugin in self.plugins:
+            try:
+                plugin.on_finalize(state, testcase)
+            except AttributeError:
+                pass
+
+
         local_findings = set()
         for detector in self.detectors.values():
             for address, pc, finding, at_init, constraint in detector.get_findings(state):
@@ -2572,8 +2634,9 @@ def flagged(flag):
         # Transactions
         with testcase.open_stream('tx') as tx_summary:
             is_something_symbolic = False
-            for tx in blockchain.human_transactions:  # external transactions
-                tx_summary.write("Transactions Nr. %d\n" % blockchain.transactions.index(tx))
+            interesting_transactions = blockchain.human_transactions
+            for tx in interesting_transactions:  # external transactions
+                tx_summary.write("Transactions Nr. %d\n" % interesting_transactions.index(tx))
 
                 # The result if any RETURN or REVERT
                 tx_summary.write("Type: %s (%d)\n" % (tx.sort, tx.depth))

manticore/platforms/evm.py

@@ -261,7 +261,6 @@ def wrapper(*args, **kwargs):
                     cond = world._constraint_to_accounts(value, ty='both', include_zero=True)
                     world.constraints.add(cond)
                     policy = 'ALL'
-
                 raise ConcretizeStack(index, policy=policy)
             return func(*args, **kwargs)
         wrapper.__signature__ = inspect.signature(func)
@@ -303,15 +302,24 @@ def __get__(self, obj, objtype=None):
             from types import MethodType
 
             #return different version depending on obj._pending_transaction
-            def _pre_func(my_obj, *args, **kwargs):
+            def _wrapped(my_obj, *args, **kwargs):
                 if my_obj._on_transaction:
                     my_obj._on_transaction = False
                     return self._pos(my_obj, *args, **kwargs)
                 else:
-                    my_obj._on_transaction = True
-                    return self._pre(my_obj, *args, **kwargs)
+                    try:
+                        return self._pre(my_obj, *args, **kwargs)
+                    except StartTx as e:
+                        # this has started a transaction. Save it in the state so 
+                        # on  next call it is resolved to the continuation
+                        my_obj._on_transaction = True
+                        raise
+            if obj._on_transaction:
+                _wrapped.__name__ = "_continuation_"
+            else:
+                _wrapped.__signature__ = inspect.signature(self._pre)
 
-            return MethodType(_pre_func, obj)
+            return MethodType(_wrapped, obj)
 
         def __set__(self, obj, value):
             raise AttributeError("can't set attribute")
@@ -1481,7 +1489,7 @@ def p1(x):
             pc = pc.value
 
         if issymbolic(pc):
-            result.append('<Symbolic PC> {:s} {}'.format((translate_to_smtlib(pc), pc.taint)))
+            result.append('<Symbolic PC> {} {}'.format(translate_to_smtlib(pc), pc.taint))
         else:
             operands_str = self.instruction.has_operand and '0x{:x}'.format(self.instruction.operand) or ''
             result.append('0x{:04x}: {:s} {:s} {:s}\n'.format(pc, self.instruction.name, operands_str, self.instruction.description))
@@ -1605,6 +1613,7 @@ def constraints(self):
         return self._constraints
 
     def _open_transaction(self, sort, address, price, bytecode_or_data, caller, value, gas=2300):
+        assert self._pending_transaction is None
         if self.depth > 0:
             origin = self.tx_origin()
         else:
@@ -2030,6 +2039,7 @@ def _pending_transaction_concretize_address(self):
         sort, address, price, data, caller, value, gas = self._pending_transaction
         if issymbolic(address):
             def set_address(state, solution):
+                assert world._pending_transaction is not None
                 world = state.platform
                 world._pending_transaction = sort, solution, price, data, caller, value, gas
             cond = self._constraint_to_accounts(address, ty='contract', include_zero=False)
@@ -2043,6 +2053,7 @@ def _pending_transaction_concretize_caller(self):
         sort, address, price, data, caller, value, gas = self._pending_transaction
         if issymbolic(caller):
             def set_caller(state, solution):
+                assert world._pending_transaction is not None
                 world = state.platform
                 world._pending_transaction = sort, address, price, data, solution, value, gas
             #Constraint it so it can range over all normal accounts
@@ -2077,7 +2088,7 @@ def _process_pending_transaction(self):
             self.create_account(address=address)
 
         # Check depth
-        failed = self.depth > 1024
+        failed = self.depth >= 1024
 
         # Fork on enough funds
         if not failed: