Detect the odd delegatecall instruction (#1108)

* DAO detector + bugfixes * The actual benchmark tests * The actual benchmark tests * CC * Experiment reporting the finding at a JUMPI * Fix taint. Detect returned overflowded data * DAO -> Reentrancy * DAO -> reentrancy, C -> Benchmark * DAO -> reentrancy, C -> Benchmark * Allow function names to have numbers * Fix contract names in benchmark * Fix contract names in benchmark * Move default plugin registration * Better regexp * Fix minimal_bytecode example * Fix Array Slice and test * add tests * correct other bug * implement bytesM * BROKEN partial progress * need bytearray here * rm cmt * add basic tests for bytesM and bytes symbolic * correct bytes symbolic test * Refactor, clean bytesM handling * Add initial symbolic 'bytes' handling * refactor tests * Unify symbolic/concrete bytes handling in bytesM/bytes * Rm import * Rm debug assert * cc * Visitor/migrate/simplify fixes to make the seth refactor pass * Fix concolic? * Fix concolic? * CC * bytesM fix * Fix address and caller concretization on symb tx * Fix/refactor symbolic address/caller concretization * Fix caller concretization * Fix expression visiting * Fix account policy refactor * Accept numbers in function names abitypes * Simplify installation instructions to recommend install manticore only for the current user * Run some tests in parallel (#970) This PR splits the current test runner into three environments: 1. Linux examples 2. Ethereum tests 3. Remaining tests to faster complete each testing run. Ethereum tests include a number of integration tests that execute scripts to completion, which takes a while. We run them concurrently with other tests to save on execution time. The split is done by naming Ethereum tests differently (`eth_*.py` vs `test_*.py`) and updating what pattern unittest's `discover` uses. This change also updates the installation script and chooses to forego installing Keystone for EVM tests as it takes a while, and it adds a `setup.cfg` config file so that Nose finds the eth tests as well by default. * Be less verbose when testing * Fix slicing wrongly reference to proxyArray. Fix #912 * Only export human/external tx in the testcase (#972) * Make ManticoreEVM.make_symbolic_value size adjustable (#974) * Make size adjustable * Default to 256 * Dev evm yolo fix gas (#975) * Fix gas stipend on CALL and check dao * Add order dependence 1 * Going linter. Report/Detect that thing when code does not check returned value * cleaner example of fail * Update retval_crazy.sol * new solc for travis * CC * Remove duplicated ReentrancyDetector * POrt to py3 * POrt to py3 * P0rt to py3 * CC * Be mega forgiving on global expression usage - EVM * Tests doc * Refactor new_bitvector api * function id to binary * Fix neW_bool * CC * rename avoid_collisions collision * rename avoid_collisions collision * migrate on state.constraint too.. * Migration bugfixes * CC bugfixes * invalid assert removed * move rep code to method * unittets fixes and CC * CC * Refactor result_ref out in favor of change_last_result() * CC * reviewing the codes * CC * Change variable names * typo * Basic refactors and output enhancements * Some minid docstrings and a unittest * Some mini docstrings and a unittest * Add migration integration testion * Keep fuzz-refactoring it * CC * Bugfixfixfixfix * CC * re refactor mig algorithm * better cleaner stronger. (reviewing) * CC * Small refactor and Fix strange strcmp test. * CC * funtion selector abinary * bugfix.. waiting for migreation PR * convenient tx abi parsing func * convenient tx abi parsing func * convenient tx abi parsing func * convenient tx abi parsing func * re re refactor for readability * CC * rev * CC * forgoten var * CC * CC * Delete duplicated detector * WIP delegatecall. Lot of fixes. Recursion fix. * review * typo * CC * Sha3 random concre example when none. Concretize SIZE/OFFSET more. Initial calldata size management * remove debug print * Add check in constraints.add * review * Adding single example to sha3 trick when there are not know examples * CC * review * CC * about to merge sha3 * cleanups * make gas budget configurable by user * cleanups * cleanups * CC: * CC * Fix typo in tests * Fix import typo * pump some gas * typo in skipping slow/big test * skipping more test to make travis happy * skipping more test to make travis happy * debugging travis like a caveman * dbg * dbg * dbg * undbg * undbg * undbg * undbg * undbg and fixed * undbg and fixed * CC
2026-10-12 02:23:44 +00:00 · 2018-09-01 10:37:38 -03:00
parent 1907968c1f
commit aa1ae09ec5
17 changed files with 465 additions and 127 deletions
@@ -95,7 +95,10 @@ def parse_arguments():
                        help='Enable detection of reentrancy bug (Ethereum only)')

    parser.add_argument('--detect-unused-retval', action='store_true',
-                        help='Enable detection of not used internal transaction return value')
+                        help='Enable detection of not used internal transaction return value (Ethereum only)')
+
+    parser.add_argument('--detect-delegatecall', action='store_true',
+                        help='Enable detection of problematic uses of DELEGATECALL instruction (Ethereum only)')

    parser.add_argument('--detect-selfdestruct', action='store_true',
                        help='Enable detection of reachable selfdestruct instructions')
@@ -131,7 +134,8 @@ def parse_arguments():


 def ethereum_cli(args):
-    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectExternalCallAndLeak, DetectReentrancySimple, DetectEnvInstruction
+    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectReentrancySimple, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectDelegatecall, DetectExternalCallAndLeak, DetectReentrancySimple, DetectEnvInstruction
+
    log.init_logging()

    m = ManticoreEVM(procs=args.procs, workspace_url=args.workspace)
@@ -148,6 +152,8 @@ def ethereum_cli(args):
        m.register_detector(DetectReentrancySimple())
    if args.detect_all or args.detect_unused_retval:
        m.register_detector(DetectUnusedRetVal())
+    if args.detect_all or args.detect_delegatecall:
+        m.register_detector(DetectDelegatecall())
    if args.detect_all or args.detect_selfdestruct:
        m.register_detector(DetectSelfdestruct())
    if args.detect_all or args.detect_externalcall:
@@ -51,7 +51,6 @@ class ConstraintSet(object):
        :param check: Currently unused.
        :return:
        '''
-        # XXX(yan): check is an unused param
        if isinstance(constraint, bool):
            constraint = BoolConstant(constraint)
        assert isinstance(constraint, Bool)
@@ -72,6 +71,11 @@ class ConstraintSet(object):

        self._constraints.append(constraint)

+        if check:
+            from manticore.core.smtlib import solver
+            if not solver.check(self):
+                raise ValueError("Added an impossible constraint")
+
    def _get_sid(self):
        ''' Returns an unique id. '''
        assert self._child is None
@@ -635,7 +635,8 @@ class Array(Expression):
        return self._index_max

    def select(self, index):
-        return ArraySelect(self, self.cast_index(index))
+        index = self.cast_index(index)
+        return ArraySelect(self, index)

    def store(self, index, value):
        return ArrayStore(self, self.cast_index(index), self.cast_value(value))
@@ -308,17 +308,27 @@ class Z3Solver(Solver):
            return expression
        assert isinstance(expression, Variable)

-        self._send('(get-value (%s))' % expression.name)
-        ret = self._recv()
-        assert ret.startswith('((') and ret.endswith('))'), ret
+        if isinstance(expression, Array):
+            result = bytearray()
+            for c in expression:
+                expression_str = translate_to_smtlib(c)
+                self._send('(get-value (%s))' % expression_str)
+                response = self._recv()
+                result.append(int('0x{:s}'.format(response.split(expression_str)[1][3:-2]), 16))
+            return bytes(result)
+        else:
+            self._send('(get-value (%s))' % expression.name)
+            ret = self._recv()
+            assert ret.startswith('((') and ret.endswith('))'), ret
+
+            if isinstance(expression, Bool):
+                return {'true': True, 'false': False}[ret[2:-2].split(' ')[1]]
+            elif isinstance(expression, BitVec):
+                pattern, base = self._get_value_fmt
+                m = pattern.match(ret)
+                expr, value = m.group('expr'), m.group('value')
+                return int(value, base)

-        if isinstance(expression, Bool):
-            return {'true': True, 'false': False}[ret[2:-2].split(' ')[1]]
-        elif isinstance(expression, BitVec):
-            pattern, base = self._get_value_fmt
-            m = pattern.match(ret)
-            expr, value = m.group('expr'), m.group('value')
-            return int(value, base)
        raise NotImplementedError("_getvalue only implemented for Bool and BitVec")

    # push pop
@@ -361,6 +371,8 @@ class Z3Solver(Solver):
                var = temp_cs.new_bool()
            elif isinstance(expression, BitVec):
                var = temp_cs.new_bitvec(expression.size)
+            elif isinstance(expression, Array):
+                var = temp_cs.new_array(index_max=expression.index_max, value_bits=expression.value_bits, taint=expression.taint).array
            else:
                raise NotImplementedError("get_all_values only implemented for Bool and BitVec")

@@ -393,15 +393,18 @@ class ArithmeticSimplifier(Visitor):
            return BitVecITE(expression.size, *operands, taint=expression.taint)

    def visit_BitVecExtract(self, expression, *operands):
-        ''' extract(0,sizeof(a))(a)  ==> a
-            extract(0, 16 )( concat(a,b,c,d) ) => concat(c, d)
+        ''' extract(sizeof(a), 0)(a)  ==> a
+            extract(16, 0)( concat(a,b,c,d) ) => concat(c, d)
            extract(m,M)(and/or/xor a b ) => and/or/xor((extract(m,M) a) (extract(m,M) a)
        '''
        op = expression.operands[0]
        begining = expression.begining
        end = expression.end

-        if isinstance(op, BitVecConcat):
+        # extract(sizeof(a), 0)(a)  ==> a
+        if begining == 0 and end + 1 == op.size:
+            return op
+        elif isinstance(op, BitVecConcat):
            new_operands = []
            bitcount = 0
            for item in reversed(op.operands):
@@ -515,6 +518,7 @@ class ArithmeticSimplifier(Visitor):

        if isinstance(index, BitVecConstant):
            ival = index.value
+
            # props are slow and using them tight loops should be avoided, esp when they offer no additional validation
            # arr._operands[1] = arr.index, arr._operands[0] = arr.array
            while isinstance(arr, ArrayStore) and isinstance(arr._operands[1], BitVecConstant) and arr._operands[1]._value != ival:
@@ -35,7 +35,9 @@ class Concretize(StateException):
    '''
    _ValidPolicies = ['MINMAX', 'ALL', 'SAMPLED', 'ONE']

-    def __init__(self, message, expression, setstate=None, policy='ALL', **kwargs):
+    def __init__(self, message, expression, setstate=None, policy=None, **kwargs):
+        if policy is None:
+            policy = 'ALL'
        if policy not in self._ValidPolicies:
            raise Exception("Policy (%s) must be one of: %s" % (policy, ', '.join(self._ValidPolicies),))
        self.expression = expression
@@ -107,13 +109,14 @@ class State(Eventful):
        self.forward_events_from(self._platform)

    # Fixme(felipe) change for with "state.cow_copy() as st_temp":.
+    # This need to change. this is the center of ALL the problems. re. CoW
    def __enter__(self):
        assert self._child is None
        self._platform.constraints = None
-        new_state = State(self._constraints.__enter__(), copy.deepcopy(self._platform))
+        new_state = State(self._constraints.__enter__(), self._platform)
        self.platform.constraints = new_state.constraints
        new_state._input_symbols = list(self._input_symbols)
-        new_state._context = copy.deepcopy(self._context)
+        new_state._context = copy.copy(self._context)
        self._child = new_state
        assert new_state.platform.constraints is new_state.constraints

@@ -245,7 +248,7 @@ class State(Eventful):
        self._input_symbols.append(expr)
        return expr

-    def concretize(self, symbolic, policy, maxcount=5):
+    def concretize(self, symbolic, policy, maxcount=7):
        ''' This finds a set of solutions for symbolic using policy.
            This raises TooManySolutions if more solutions than maxcount
        '''
@@ -253,6 +256,10 @@ class State(Eventful):
        vals = []
        if policy == 'MINMAX':
            vals = self._solver.minmax(self._constraints, symbolic)
+        elif policy == 'MAX':
+            vals = self._solver.max(self._constraints, symbolic)
+        elif policy == 'MIN':
+            vals = self._solver.min(self._constraints, symbolic)
        elif policy == 'SAMPLED':
            m, M = self._solver.minmax(self._constraints, symbolic)
            vals += [m, M]
@@ -260,14 +267,19 @@ class State(Eventful):
                if self._solver.can_be_true(self._constraints, symbolic == (m + M) // 2):
                    vals.append((m + M) // 2)
            if M - m > 100:
+                for i in (0, 1, 2, 5, 32, 64, 128, 320):
+                    if self._solver.can_be_true(self._constraints, symbolic == m + i):
+                        vals.append(m + i)
+                    if maxcount <= len(vals):
+                        break
+            if M - m > 1000 and maxcount > len(vals):
                vals += self._solver.get_all_values(self._constraints, symbolic,
-                                                    maxcnt=maxcount, silent=True)
+                                                    maxcnt=maxcount - len(vals), silent=True)
        elif policy == 'ONE':
            vals = [self._solver.get_value(self._constraints, symbolic)]
        else:
            assert policy == 'ALL'
-            vals = solver.get_all_values(self._constraints, symbolic, maxcnt=maxcount,
-                                         silent=False)
+            vals = solver.get_all_values(self._constraints, symbolic, maxcnt=maxcount, silent=True)

        return tuple(set(vals))

@@ -125,7 +125,6 @@ class FilterFunctions(Plugin):
                #Avoid all not selected hashes
                for func_hsh in md.hashes:
                    if func_hsh in selected_functions:
-                        # Was constraint = Operators.NOT(tx.data[:4] == func_hsh)
                        constraint = tx.data[:4] != func_hsh
                        state.constrain(constraint)

@@ -642,6 +641,38 @@ class DetectUnusedRetVal(Detector):
                self._remove_retval_taint(state, used_taint)


+class DetectDelegatecall(Detector):
+    '''
+        Detects DELEGATECALLs to controlled addresses and or with controlled function id.
+        This detector finds and reports on any delegatecall instruction any the following propositions are hold:
+            * the destination address can be controlled by the caller
+            * the first 4 bytes of the calldata are controlled by the caller
+    '''
+
+    def will_evm_execute_instruction_callback(self, state, instruction, arguments):
+        world = state.platform
+        mnemonic = instruction.semantics
+        current_vm = world.current_vm
+        # If it executed a DELEGATECALL
+        # TODO: Check the transaction was success
+        # if blockchain.last_transaction.return_value:
+        # TODO: check if any of the potential target addresses has code
+        # if not any( world.get_code, possible_addresses):
+        if mnemonic == 'DELEGATECALL':
+            gas, address, in_offset, in_size, out_offset, out_size = arguments
+            if issymbolic(address):
+                possible_addresses = state.solve_n(address, 2)
+                if len(possible_addresses) > 1:
+                    self.add_finding_here(state, "Delegatecall to user controlled address")
+
+            calldata = world.current_vm.read_buffer(in_offset, in_size)
+            func_id = calldata[:4]
+            if issymbolic(func_id):
+                possible_func_ids = state.solve_n(func_id, 2)
+                if len(possible_func_ids) > 1:
+                    self.add_finding_here(state, "Delegatecall to user controlled function")
+
+
 class DetectUninitializedMemory(Detector):
    """
        Detects uses of uninitialized memory
@@ -1532,6 +1563,7 @@ class ManticoreEVM(Manticore):
                output, warnings = ManticoreEVM._run_solc(temp, solc_bin, solc_remaps)
        elif isinstance(source_code, io.IOBase):
            output, warnings = ManticoreEVM._run_solc(source_code, solc_bin, solc_remaps)
+            source_code.seek(0)
            source_code = source_code.read()
        else:
            raise TypeError
@@ -1597,7 +1629,7 @@ class ManticoreEVM(Manticore):
        # Make the constraint store
        constraints = ConstraintSet()
        # make the ethereum world state
-        world = evm.EVMWorld(constraints)
+        world = evm.EVMWorld(constraints, initial_timestamp=1524785992)
        initial_state = State(constraints, world)
        super().__init__(initial_state, **kwargs)

@@ -1829,7 +1861,7 @@ class ManticoreEVM(Manticore):
            return None
        return contract_account

-    def create_contract(self, owner, balance=0, address=None, init=None, name=None):
+    def create_contract(self, owner, balance=0, address=None, init=None, name=None, gas=21000):
        """ Creates a contract

            :param owner: owner account (will be default caller in any transactions)
@@ -1839,6 +1871,7 @@ class ManticoreEVM(Manticore):
            :param int address: the address for the new contract (optional)
            :param str init: initializing evm bytecode and arguments
            :param str name: a uniq name for reference
+            :param gas: gas budget for the creation/inititialization of the contract
            :rtype: EVMAccount
        """
        if not self.count_running_states():
@@ -1859,7 +1892,7 @@ class ManticoreEVM(Manticore):
            # Account name already used
            raise EthereumError("Name already used")

-        self._transaction('CREATE', owner, balance, address, data=init)
+        self._transaction('CREATE', owner, balance, address, data=init, gaslimit=gas)
        # TODO detect failure in the constructor

        self._accounts[name] = EVMContract(address=address, manticore=self, default_caller=owner, name=name)
@@ -1884,7 +1917,7 @@ class ManticoreEVM(Manticore):
            return self.new_address()
        return new_address

-    def transaction(self, caller, address, value, data):
+    def transaction(self, caller, address, value, data, gas=21000):
        """ Issue a symbolic transaction in all running states

            :param caller: the address of the account sending the transaction
@@ -1894,9 +1927,10 @@ class ManticoreEVM(Manticore):
            :param value: balance to be transfered on creation
            :type value: int or SValue
            :param data: initial data
+            :param gas: gas budget
            :raises NoAliveStates: if there are no alive states to execute
        """
-        self._transaction('CALL', caller, value=value, address=address, data=data)
+        self._transaction('CALL', caller, value=value, address=address, data=data, gaslimit=gas)

    def create_account(self, balance=0, address=None, code=None, name=None):
        """ Low level creates an account. This won't generate a transaction.
@@ -1994,8 +2028,8 @@ class ManticoreEVM(Manticore):

            return caller, address, value, data

-    def _transaction(self, sort, caller, value=0, address=None, data=None, price=1):
-        """ Creates a contract
+    def _transaction(self, sort, caller, value=0, address=None, data=None, gaslimit=0, price=1):
+        """ Initiates a transaction

            :param caller: caller account
            :type caller: int or EVMAccount
@@ -2004,6 +2038,7 @@ class ManticoreEVM(Manticore):
            :param price: the price of gas for this transaction. Mostly unused.
            :type value: int or SValue
            :param str data: initializing evm bytecode and arguments or transaction call data
+            :param gaslimit: gas budget
            :rtype: EVMAccount
        """
        #Type Forgiveness
@@ -2071,7 +2106,7 @@ class ManticoreEVM(Manticore):
                    # Address already used
                    raise EthereumError("This is bad. Same address used for different contracts in different states")

-            state.context['_pending_transaction'] = (sort, caller, address, value, data, price)
+            state.context['_pending_transaction'] = (sort, caller, address, value, data, gaslimit, price)

        # run over potentially several states and
        # generating potentially several others
@@ -2119,7 +2154,8 @@ class ManticoreEVM(Manticore):
                self.transaction(caller=tx_account[min(tx_no, len(tx_account) - 1)],
                                 address=contract_account,
                                 data=symbolic_data,
-                                 value=value)
+                                 value=value,
+                                 gas=2100000)
                logger.info("%d alive states, %d terminated states", self.count_running_states(), self.count_terminated_states())
            except NoAliveStates:
                break
@@ -2245,7 +2281,6 @@ class ManticoreEVM(Manticore):
                results.append((data_concrete, data_hash))
                known_hashes_cond = data_concrete == data
                known_sha3.append((data_concrete, data_hash))
-
            not_known_hashes_cond = Operators.NOT(known_hashes_cond)

            # We need to fork/save the state
@@ -2323,14 +2358,14 @@ class ManticoreEVM(Manticore):
        if '_pending_transaction' not in state.context:
            return
        world = state.platform
-        ty, caller, address, value, data, price = state.context['_pending_transaction']
+        ty, caller, address, value, data, gaslimit, price = state.context['_pending_transaction']
        del state.context['_pending_transaction']

        if ty == 'CALL':
-            world.transaction(address=address, caller=caller, data=data, value=value, price=price)
+            world.transaction(address=address, caller=caller, data=data, value=value, price=price, gas=gaslimit)
        else:
            assert ty == 'CREATE'
-            world.create_contract(caller=caller, address=address, balance=value, init=data, price=price)
+            world.create_contract(caller=caller, address=address, balance=value, init=data, price=price, gas=gaslimit)

    def _did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
        """ INTERNAL USE """
@@ -2466,7 +2501,6 @@ class ManticoreEVM(Manticore):
            # Accounts summary
            is_something_symbolic = False
            summary.write("%d accounts.\n" % len(blockchain.accounts))
-
            for account_address in blockchain.accounts:
                is_account_address_symbolic = issymbolic(account_address)
                account_address = state.solve_one(account_address)
@@ -2569,35 +2603,36 @@ class ManticoreEVM(Manticore):

                if tx.sort == 'CALL':
                    if metadata is not None:
-                        function_id = state.solve_one(tx.data[:4])  # hope there is enough data
+                        calldata = state.solve_one(tx.data)
+                        is_calldata_symbolic = issymbolic(tx.data)
+
+                        function_id = calldata[:4]  # hope there is enough data
                        signature = metadata.get_func_signature(function_id)
                        function_name = metadata.get_func_name(function_id)
                        if signature:
-                            _, arguments = ABI.deserialize(signature, tx.data)
+                            _, arguments = ABI.deserialize(signature, calldata)
                        else:
-                            arguments = (tx.data,)
+                            arguments = (calldata,)

                        return_data = None
                        if tx.result == 'RETURN':
                            ret_types = metadata.get_func_return_types(function_id)
-                            return_data = ABI.deserialize(ret_types, tx.return_data)  # function return
+                            return_data = state.solve_one(tx.return_data)
+                            return_values = ABI.deserialize(ret_types, return_data)  # function return
+                            is_return_symbolic = issymbolic(tx.return_data)

                        tx_summary.write('\n')
                        tx_summary.write("Function call:\n")
                        tx_summary.write("%s(" % function_name)
-                        tx_summary.write(','.join(map(repr, map(state.solve_one, arguments))))
-                        is_argument_symbolic = any(map(issymbolic, arguments))
-                        is_something_symbolic = is_something_symbolic or is_argument_symbolic
-                        tx_summary.write(') -> %s %s\n' % (tx.result, flagged(is_argument_symbolic)))
+                        tx_summary.write(','.join(map(repr, arguments)))
+                        tx_summary.write(') -> %s %s\n' % (tx.result, flagged(is_calldata_symbolic)))

                        if return_data is not None:
-                            is_return_symbolic = any(map(issymbolic, return_data))
-                            return_values = tuple(map(state.solve_one, return_data))
                            if len(return_values) == 1:
                                return_values = return_values[0]

                            tx_summary.write('return: %r %s\n' % (return_values, flagged(is_return_symbolic)))
-                            is_something_symbolic = is_something_symbolic or is_return_symbolic
+                        is_something_symbolic = is_calldata_symbolic or is_return_symbolic

                tx_summary.write('\n\n')

@@ -2682,7 +2717,6 @@ class ManticoreEVM(Manticore):
                q.put(state_id)

        report_workers = []
-
        for _ in range(self._config_procs):
            proc = Process(target=worker_finalize, args=(q,))
            proc.start()
@@ -533,7 +533,7 @@ class Manticore(Eventful):
        # Everything is good add it.
        state.constraints.add(assertion)

-    ##########################################################################
+    ############################################################################
    # Some are placeholders Remove FIXME
    # Any platform specific callback should go to a plugin

@@ -252,16 +252,19 @@ def concretized_args(**policies):
                if not issymbolic(args[index]):
                    continue
                if not policy:
-                    raise ConcretizeStack(index)
+                    policy = 'MINMAX'
+
                if policy == "ACCOUNTS":
-                    #special handler for EVM only policy
-                    address = args[index]
+                    value = args[index]
                    world = args[0].world
-                    cond = world._constraint_to_accounts(address, ty='both', include_zero=True)
+                    #special handler for EVM only policy
+                    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)
        return wrapper
    return concretizer

@@ -371,6 +374,12 @@ class EVM(Eventful):
        self._on_transaction = False  # for @transact
        self._checkpoint_data = None

+        # Used calldata size
+        min_size = 0
+        max_size = len(self.data)
+        self._used_calldata_size = 0
+        self._calldata_size = len(self.data)
+
    @property
    def bytecode(self):
        return self._bytecode
@@ -406,6 +415,8 @@ class EVM(Eventful):
        state['logs'] = self.logs
        state['_on_transaction'] = self._on_transaction
        state['_checkpoint_data'] = self._checkpoint_data
+        state['_used_calldata_size'] = self._used_calldata_size
+        state['_calldata_size'] = self._calldata_size
        return state

    def __setstate__(self, state):
@@ -425,9 +436,13 @@ class EVM(Eventful):
        self.stack = state['stack']
        self._allocated = state['allocated']
        self.suicides = state['suicides']
+        self._used_calldata_size = state['_used_calldata_size']
+        self._calldata_size = state['_calldata_size']
+
        super().__setstate__(state)

-    def _allocate(self, address):
+    def _get_memfee(self, address, size=1):
+        address = self.safe_add(address, size)
        allocated = self.allocated
        GMEMORY = 3
        GQUADRATICMEMDENOM = 512  # 1 gas per 512 quadwords
@@ -438,10 +453,12 @@ class EVM(Eventful):
        new_totalfee = self.safe_mul(new_size, GMEMORY) + Operators.UDIV(self.safe_mul(new_size, new_size), GQUADRATICMEMDENOM)
        memfee = new_totalfee - old_totalfee
        flag = Operators.UGT(new_totalfee, old_totalfee)
-        self._consume(Operators.ITEBV(512, flag, memfee, 0))
+        return Operators.ITEBV(512, flag, memfee, 0)

-        address_c = Operators.UDIV(self.safe_add(address, 31), 32) * 32
-        self._allocated = Operators.ITEBV(512, flag, Operators.ZEXTEND(address_c, 512), Operators.ZEXTEND(allocated, 512))
+    def _allocate(self, address):
+        self._consume(self._get_memfee(address))
+        address_c = Operators.ZEXTEND(Operators.UDIV(self.safe_add(address, 31), 32) * 32, 512)
+        self._allocated = Operators.ITEBV(512, address_c > self._allocated, address_c, self.allocated)

    @property
    def allocated(self):
@@ -546,33 +563,46 @@ class EVM(Eventful):
            if (fee.size != 512):
                raise EthereumError("Fees should be 512 bit long")

-        self.constraints.add(Operators.UGE(fee, 0))
-        self.constraints.add(Operators.ULE(fee, self._gas))
-
        #FIXME add configurable checks here
-        if config.out_of_gas is not None:
-            if config.out_of_gas == 0:
-                #default to OOG exception if possible
-                if solver.can_be_true(self.constraints, self._gas < fee):
-                    self.constraints.add(Operators.UGT(fee, self.gas))
-                    logger.debug("Not enough gas for instruction")
-                    raise NotEnoughGas()
-            elif config.out_of_gas == 1:
-                #default to enough gas if possible
-                if solver.can_be_true(self.constraints, self._gas > fee):
-                    self.constraints.add(Operators.UGT(self.gas, fee))
+        config.out_of_gas = 3
+
+        # Iff both are concrete values...
+        if not issymbolic(self._gas) and not issymbolic(fee):
+            if self._gas < fee:
+                logger.debug("Not enough gas for instruction")
+                raise NotEnoughGas()
+        else:
+                if config.out_of_gas is None:
+                    # do nothing. gas could go negative.
+                    # memory could be accessed in great offsets
+                    pass
+                elif config.out_of_gas == 0:
+                    #explore only when OOG
+                    if solver.can_be_true(self.constraints, Operators.ULT(self.gas, fee)):
+                        self.constraints.add(Operators.UGT(fee, self.gas))
+                        logger.debug("Not enough gas for instruction")
+                        raise NotEnoughGas()
+                elif config.out_of_gas == 1:
+                    #explore only when there is enough gas if possible
+                    if solver.can_be_true(self.constraints, Operators.UGT(self.gas, fee)):
+                        self.constraints.add(Operators.UGT(self.gas, fee))
+                    else:
+                        logger.debug("Not enough gas for instruction")
+                        raise NotEnoughGas()
                else:
-                    logger.debug("Not enough gas for instruction")
-                    raise NotEnoughGas()
-            else:
-                #fork on both options
-                if len(solver.get_all_values(self.constraints, self._gas > fee)) == 2:
-                    raise Concretize("Concretice gas fee",
-                                     expression=self._gas > fee,
-                                     setstate=None,
-                                     policy='ALL')
+                    #explore both options / fork
+                    enough_gas_solutions = solver.get_all_values(self.constraints, Operators.UGT(self._gas, fee))
+                    if len(enough_gas_solutions) == 2:
+                        raise Concretize("Concretice gas fee",
+                                         expression=Operators.UGT(self._gas, fee),
+                                         setstate=None,
+                                         policy='ALL')
+                    elif enough_gas_solutions[0] == False:
+                        logger.debug("Not enough gas for instruction")
+                        raise NotEnoughGas()

        self._gas -= fee
+        assert issymbolic(self._gas) or self._gas >= 0

    def _indemnify(self, fee):
        self._gas += fee
@@ -748,6 +778,31 @@ class EVM(Eventful):
        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))
+
+    def safe_add(self, a, b):
+        a = Operators.ZEXTEND(a, 512)
+        b = Operators.ZEXTEND(b, 512)
+        result = a + b
+        '''
+        if solver.can_be_true(self.constraints, Operators.ULT(result, 1 << 256)):
+            self.constraints.add(Operators.ULT(result, 1 << 256))
+        else:
+            raise ValueError("Integer overflow")
+        '''
+        return result
+
+    def safe_mul(self, a, b):
+        a = Operators.ZEXTEND(a, 512)
+        b = Operators.ZEXTEND(b, 512)
+        result = a * b
+        '''
+        if solver.can_be_true(self.constraints, Operators.ULT(result, 1 << 256)):
+            self.constraints.add(Operators.ULT(result, 1 << 256))
+        else:
+            raise ValueError("Integer overflow")
+        '''
+        return result
+
    ############################################################################
    #INSTRUCTIONS

@@ -839,11 +894,12 @@ class EVM(Eventful):
        EXP_SUPPLEMENTAL_GAS = 50   # cost of EXP exponent per byte

        def nbytes(e):
+            result = 32
            for i in range(32):
-                if e >> (i * 8) == 0:
-                    return i
-            return 32
+                result = Operators.ITEBV(512, Operators.EXTRACT(e, i, 8) == 0, i, result)
+            return result
        self._consume(EXP_SUPPLEMENTAL_GAS * nbytes(exponent))
+
        return pow(base, exponent, TT256)

    def SIGNEXTEND(self, size, value):
@@ -914,7 +970,7 @@ class EVM(Eventful):
                concrete_data.append(simplified.value)
            else:
                #simplify by solving. probably means that we need to improve simplification
-                solutions = solver.get_all_values(self.constraints, c, 2, silent=True)
+                solutions = solver.get_all_values(self.constraints, simplified, 2, silent=True)
                if len(solutions) != 1:
                    break
                concrete_data.append(solutions[0])
@@ -942,7 +998,6 @@ class EVM(Eventful):
            for key, hsh in known_sha3.items():
                assert not issymbolic(key), "Saved sha3 data,hash pairs should be concrete"
                cond = key == data
-
                known_hashes_cond = Operators.OR(cond, known_hashes_cond)
                value = Operators.ITEBV(256, cond, hsh, value)
            return value
@@ -979,6 +1034,14 @@ class EVM(Eventful):

    def CALLDATALOAD(self, offset):
        '''Get input data of current environment'''
+
+        if issymbolic(offset):
+            if solver.can_be_true(self._constraints, offset == self._used_calldata_size):
+                self.constraints.add(offset == self._used_calldata_size)
+            raise ConcretizeStack(1, policy='SAMPLED')
+
+        self._use_calldata(offset + 32)
+
        data_length = len(self.data)

        bytes = []
@@ -992,33 +1055,38 @@ class EVM(Eventful):
            bytes.append(c)
        return Operators.CONCAT(256, *bytes)

+    def _use_calldata(self, n):
+        assert not issymbolic(n)
+        max_size = len(self.data)
+        min_size = self._used_calldata_size
+        self._used_calldata_size = Operators.ITEBV(256, min_size + n > max_size, max_size, min_size + n)
+
    def CALLDATASIZE(self):
        '''Get size of input data in current environment'''
-        return len(self.data)
+        return self._calldata_size

-    def safe_add(self, a, b):
-        a = Operators.ZEXTEND(a, 512)
-        b = Operators.ZEXTEND(b, 512)
-        result = a + b
-        self.constraints.add(Operators.UGE(result, 0))
-        self.constraints.add(Operators.ULT(result, 1 << 256))
-        return result
-
-    def safe_mul(self, a, b):
-        a = Operators.ZEXTEND(a, 512)
-        b = Operators.ZEXTEND(b, 512)
-        result = a * b
-        self.constraints.add(Operators.UGE(result, 0))
-        self.constraints.add(Operators.ULT(result, 1 << 256))
-        return result
-
-    @concretized_args(size='SAMPLED')
    def CALLDATACOPY(self, mem_offset, data_offset, size):
        '''Copy input data in current environment to memory'''
-        GCOPY = 3             # cost to copy one 32 byte word
-        self._consume(self.safe_mul(GCOPY, self.safe_add(size, 31) // 32))
-        self._allocate(self.safe_add(mem_offset, size))

+        if issymbolic(size):
+            if solver.can_be_true(self._constraints, size <= len(self.data) + 32):
+                self.constraints.add(size <= len(self.data) + 32)
+            raise ConcretizeStack(3, policy='SAMPLED')
+
+        if issymbolic(data_offset):
+            if solver.can_be_true(self._constraints, data_offset == self._used_calldata_size):
+                self.constraints.add(data_offset == self._used_calldata_size)
+            raise ConcretizeStack(2, policy='SAMPLED')
+
+        GCOPY = 3             # cost to copy one 32 byte word
+        self._use_calldata(data_offset + size)
+        copyfee = self.safe_mul(GCOPY, self.safe_add(size, 31) // 32)
+        memfee = self._get_memfee(mem_offset, size)
+
+        self._consume(copyfee)
+        self._consume(memfee)
+
+        self._allocate(self.safe_add(mem_offset, size))
        for i in range(size):
            try:
                c = Operators.ITEBV(8, data_offset + i < len(self.data), Operators.ORD(self.data[data_offset + i]), 0)
@@ -1031,6 +1099,7 @@ class EVM(Eventful):
        '''Get size of code running in current environment'''
        return len(self.bytecode)

+    @concretized_args(code_offset='SAMPLED', size='SAMPLED')
    def CODECOPY(self, mem_offset, code_offset, size):
        '''Copy code running in current environment to memory'''

@@ -1043,21 +1112,20 @@ class EVM(Eventful):

        for i in range(max_size):
            if issymbolic(i < size):
-                default = Operators.ITEBV(256, i < size, 0, self._load(mem_offset + i))  # Fixme. unnecessary memory read
+                default = Operators.ITEBV(8, i < size, 0, self._load(mem_offset + i, 1))  # Fixme. unnecessary memory read
            else:
                if i < size:
                    default = 0
                else:
-                    default = self._load(mem_offset + i)
+                    default = self._load(mem_offset + i, 1)

            if issymbolic(code_offset):
-                value = Operators.ITEBV(256, code_offset + i >= len(self.bytecode), default, self.bytecode[code_offset + i])
+                value = Operators.ITEBV(8, code_offset + i >= len(self.bytecode), default, self.bytecode[code_offset + i])
            else:
                if code_offset + i >= len(self.bytecode):
                    value = default
                else:
                    value = self.bytecode[code_offset + i]
-
            self._store(mem_offset + i, value)
        self._publish('did_evm_read_code', code_offset, size)

@@ -1281,7 +1349,7 @@ class EVM(Eventful):
                                     data=self.read_buffer(in_offset, in_size),
                                     caller=self.address,
                                     value=value,
-                                     gas=self.gas)
+                                     gas=gas)
        raise StartTx()

    @CALLCODE.pos
@@ -1308,7 +1376,7 @@ class EVM(Eventful):
                                     data=self.read_buffer(in_offset, in_size),
                                     caller=self.address,
                                     value=0,
-                                     gas=self.gas)
+                                     gas=gas)
        raise StartTx()

    @DELEGATECALL.pos
@@ -1330,7 +1398,7 @@ class EVM(Eventful):
                                     data=self.read_buffer(in_offset, in_size),
                                     caller=self.address,
                                     value=0,
-                                     gas=self.gas)
+                                     gas=gas)
        raise StartTx()

    @STATICCALL.pos
@@ -1416,7 +1484,7 @@ class EVM(Eventful):
            result.append('<Symbolic PC> {:s} {}'.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)))
+            result.append('0x{:04x}: {:s} {:s} {:s}\n'.format(pc, self.instruction.name, operands_str, self.instruction.description))

        args = {}
        implementation = getattr(self, self.instruction.semantics, None)
@@ -1556,7 +1624,7 @@ class EVMWorld(Platform):
            address = tx.caller
            assert value == 0

-        vm = EVM(self._constraints, address, data, caller, value, bytecode, world=self)
+        vm = EVM(self._constraints, address, data, caller, value, bytecode, world=self, gas=gas)

        self._publish('will_open_transaction', tx)
        self._callstack.append((tx, self.logs, self.deleted_accounts, copy.copy(self.get_storage(address)), vm))
@@ -1899,7 +1967,7 @@ class EVMWorld(Platform):

        return address

-    def create_contract(self, price=0, address=None, caller=None, balance=0, init=None):
+    def create_contract(self, price=0, address=None, caller=None, balance=0, init=None, gas=2300):
        '''
        The way that the Solidity compiler expects the constructor arguments to
        be passed is by appending the arguments to the byte code produced by the
@@ -1910,12 +1978,12 @@ class EVMWorld(Platform):
        on the network.
        '''
        address = self.create_account(address)
-        self.start_transaction('CREATE', address, price, init, caller, balance)
+        self.start_transaction('CREATE', address, price, init, caller, balance, gas=gas)
        self._process_pending_transaction()
        return address

-    def transaction(self, address, price=0, data='', caller=None, value=0):
-        self.start_transaction('CALL', address, price=price, data=data, caller=caller, value=value)
+    def transaction(self, address, price=0, data='', caller=None, value=0, gas=2300):
+        self.start_transaction('CALL', address, price=price, data=data, caller=caller, value=value, gas=gas)
        self._process_pending_transaction()

    def start_transaction(self, sort, address, price=None, data=None, caller=None, value=0, gas=2300):
@@ -2019,7 +2087,7 @@ class EVMWorld(Platform):

            if set(enough_balance_solutions) == {True, False}:
                raise Concretize('Forking on available funds',
-                                 expression=Operators.ULT(src_balance, value),
+                                 expression=enough_balance,
                                 setstate=lambda a, b: None,
                                 policy='ALL')
            failed = set(enough_balance_solutions) == {False}
@@ -4,6 +4,7 @@ import logging
 import pickle
 import re
 import sys
+import resource

 from collections import OrderedDict
 from ..core.smtlib import Expression, BitVecConstant
@@ -129,7 +130,7 @@ class StateSerializer(object):


 class PickleSerializer(StateSerializer):
-    DEFAULT_RECURSION: int = 0x100000  # 1M
+    DEFAULT_RECURSION: int = 0x10000  # 1M
    MAX_RECURSION: int = 0x1000000  # 16.7M

    def __init__(self):
@@ -0,0 +1,26 @@
+pragma solidity ^0.4.24;
+/*
+There is a dangerous use of lowlevel instruction delegatecall in the fallback function.
+The address to which the delegatecall tx is sent is controlled by any user of this contract.
+The storage variable `addr` is initialized to `this` and it CAN be modified.
+The function selector of the delegate call is fully controlled by the user
+*/
+
+contract DetectThis {
+  address addr;
+  constructor(){
+     addr = address(this);
+  }
+  function setaddr(address a){
+     addr = a;
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+        require(addr.delegatecall(msg.data));
+  }
+}
@@ -0,0 +1,34 @@
+pragma solidity ^0.4.24;
+/*
+There is a dangerous use of lowlevel instruction delegatecall in the fallback function.
+The target address of the delegatecall hardcoded function selector of the delegate 
+call is fully controlled by the user.
+*/
+
+contract DetectThis {
+  address addr;
+  constructor(){
+     addr = address(this);
+  }
+  function setaddr(address a){
+     addr = a;
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function f() public {
+        require(msg.data.length >=4);
+        uint i;
+        bytes memory new_calldata = new bytes(msg.data.length-4);
+
+        for (i=0; i < msg.data.length-4; i++) {
+            new_calldata[i] = msg.data[i+4];
+        }
+
+        require(address(0x41414141).delegatecall(new_calldata));
+  }
+}
+
@@ -0,0 +1,23 @@
+pragma solidity ^0.4.24;
+/*
+A fair use of delegatecall instruction is inserted by the solidity compiler for
+implementing libraries. This is an ok use of delegatecall.
+*/
+pragma solidity ^0.4.24;
+
+library Lib {
+  
+  struct Data {uint val;}
+
+  function set(Data storage self, uint new_val) public{
+    self.val = new_val;      
+  }
+}
+
+contract DetectThis {
+    Lib.Data public myVal;
+
+    function () public payable{
+        Lib.set(myVal, msg.value);
+    }
+}
@@ -0,0 +1,18 @@
+pragma solidity ^0.4.24;
+/*
+There is a fair use of lowlevel instruction delegatecall in the fallback function.
+It is effectivelly a CALL to `default_call` with the full calldata that was givento the fallback function
+*/
+contract DetectThis {
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+        bool retval = address(this).delegatecall(bytes4(keccak256("default_call(bytes)")), msg.data);
+        require(retval);
+  }
+
+}
@@ -0,0 +1,24 @@
+pragma solidity ^0.4.24;
+/*
+There is a fair use of lowlevel instruction delegatecall in the fallback function.
+It is effectivelly a CALL to `this.default_call` with a concrete data.
+The storage variable `addr` is initialized to `this` and can not be modified.
+*/
+
+contract DetectThis {
+  address addr;
+  constructor(){
+        addr = address(this);
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+        bool retval = addr.delegatecall(bytes4(keccak256("default_call(bytes)")), "Concrete values!");
+        require(retval);
+  }
+
+}
@@ -0,0 +1,38 @@
+pragma solidity ^0.4.24;
+/*
+There is a dangerous use of lowlevel instruction delegatecall in the fallback function.
+The address to which the delegatecall tx is sent is controlled by any user of this contract.
+The storage variable `addr` is initialized to `this` and it CAN be modified.
+The function selector of the delegate call is fully controlled by the user
+*/
+
+contract DetectThis {
+  address addr;
+  constructor() public{
+     addr = address(this);
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+  	require(msg.data.length > 4);
+        uint i;
+        bytes memory new_calldata = new bytes(msg.data.length);
+        bytes4 func_id = bytes4(keccak256("default_call(bytes)"));
+        for (i=0; i < 4; i++) {
+            new_calldata[i] = func_id[i];
+        }
+
+        for (; i < msg.data.length; i++) {
+            new_calldata[i] = msg.data[i];
+        }
+
+      require(address(this).delegatecall(new_calldata));
+
+  }
+}
+
+
@@ -12,8 +12,8 @@ import os
 from manticore.core.smtlib import operators
 from eth_general import make_mock_evm_state
 from manticore.ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, Detector, NoAliveStates, ABI, \
-    EthereumError, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectExternalCallAndLeak, \
-    DetectEnvInstruction
+    EthereumError, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectDelegatecall, \
+    DetectEnvInstruction, DetectExternalCallAndLeak, DetectEnvInstruction

 import shutil

@@ -57,7 +57,7 @@ class EthDetectorTest(unittest.TestCase):
        self.assertEqual(expected_findings, actual_findings)

 class EthRetVal(EthDetectorTest):
-    """ https://consensys.net/diligence/evm-analyzer-benchmark-suite/ """
+    """ Detect when a return value of a low level transaction instruction is ignored """
    DETECTOR_CLASS = DetectUnusedRetVal

    def test_retval_ok(self):
@@ -180,3 +180,36 @@ class DetectEnvInstruction(EthDetectorTest):



+class EthDelegatecall(EthDetectorTest):
+    """ Test the detecion of funny delegatecalls """
+    DETECTOR_CLASS = DetectDelegatecall
+
+    def test_delegatecall_ok(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_delegatecall_ok1(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_delegatecall_ok2(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    @unittest.skip("Too slow for this modern times")
+    def test_delegatecall_ok3(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_delegatecall_not_ok(self):
+        self.mevm.register_plugin(LoopDepthLimiter())
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, {(179, 'Delegatecall to user controlled function', False), (179, 'Delegatecall to user controlled address', False)})
+
+    @unittest.skip("Too slow for this modern times")
+    def test_delegatecall_not_ok1(self):
+        self.mevm.register_plugin(LoopDepthLimiter(loop_count_threshold=500))
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, {(179, 'Delegatecall to user controlled function', False)})
+
+