py3 yolo_master (feature / bugfixes) (#994)

* 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

* missing files

* 985

* formatting fixes; codeclimate

* review changes

.codeclimate.yml

@@ -23,7 +23,7 @@ checks:
   method-lines:
     enabled: true
     config:
-      threshold: 52
+      threshold: 53
   nested-control-flow:
     enabled: true
     config:

.travis.yml

@@ -9,6 +9,10 @@ python:
 env:
   global:
     - CC_TEST_REPORTER_ID=db72f1ed59628c16eb0c00cbcd629c4c71f68aa1892ef42d18c7c2b8326f460a
+  matrix:
+    - TEST_TYPE=examples
+    - TEST_TYPE=tests
+    - TEST_TYPE=eth
 
 branches:
   only:
@@ -22,15 +26,15 @@ cache:
   - $HOME/virtualenv/python3.6.5/bin/
 
 install:
-  - scripts/travis_install.sh
+  - scripts/travis_install.sh $TEST_TYPE
 
 before_script:
   - curl -L https://codeclimate.com/downloads/test-reporter/test-reporter-latest-linux-amd64 > ./cc-test-reporter
   - chmod +x ./cc-test-reporter
   - ./cc-test-reporter before-build
 
 script:
-  - scripts/travis_test.sh
+  - scripts/travis_test.sh $TEST_TYPE
 
 after_script:
   - ./cc-test-reporter after-build --exit-code $TRAVIS_TEST_RESULT

README.md

@@ -141,8 +141,8 @@ m = Manticore('./path/to/binary')
 @m.hook(hook_pc)
 def hook(state):
   cpu = state.cpu
-  print 'eax', cpu.EAX
-  print cpu.read_int(cpu.ESP)
+  print('eax', cpu.EAX)
+  print(cpu.read_int(cpu.ESP))
 
   m.terminate()  # tell Manticore to stop
 

examples/evm/minimal.py

@@ -36,9 +36,8 @@
 symbolic_data = m.make_symbolic_buffer(320) 
 symbolic_value = m.make_symbolic_value(name="VALUE")
 symbolic_address = m.make_symbolic_value(name="ADDRESS")
-m.constrain(Operators.OR(symbolic_address == contract_account, symbolic_address == user_account))
-#TODO: broken; fixed in yolo-master
-m.transaction(caller=user_account,
+symbolic_caller = m.make_symbolic_value(name="CALLER")
+m.transaction(caller=symbolic_caller,
                 address=symbolic_address,
                 data=symbolic_data,
                 value=symbolic_value )

examples/evm/minimal_bytecode_only.py

@@ -21,7 +21,7 @@
 
 print("[+] Now the symbolic values")
 symbolic_data = m.make_symbolic_buffer(320) 
-symbolic_value = None 
+symbolic_value = m.make_symbolic_value()
 m.transaction(caller=user_account,
                 address=contract_account,
                 data=symbolic_data,

examples/script/concolic.py

@@ -73,7 +73,7 @@ def flip(constraint):
     cond, iifpc, eelsepc = ite.operands
     assert isinstance(iifpc, BitVecConstant) and isinstance(eelsepc, BitVecConstant)
 
-    equal.operands[1] = eelsepc if forcepc.value == iifpc.value else iifpc
+    equal._operands= (equal.operands[0], eelsepc if forcepc.value == iifpc.value else iifpc)
 
     return equal
 

manticore/__main__.py

@@ -92,6 +92,9 @@ def positive(value):
     parser.add_argument('--detect-uninitialized-storage', action='store_true',
                         help='Enable detection of uninitialized storage usage (Ethereum only)')
 
+    parser.add_argument('--detect-reentrancy', action='store_true',
+                        help='Enable detection of reentrancy bug (Ethereum only)')
+
     parser.add_argument('--detect-all', action='store_true',
                         help='Enable all detector heuristics (Ethereum only)')
 
@@ -111,7 +114,7 @@ def positive(value):
 
 
 def ethereum_cli(args):
-    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions
+    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectReentrancy
     log.init_logging()
 
     m = ManticoreEVM(procs=args.procs)
@@ -124,11 +127,13 @@ def ethereum_cli(args):
         m.register_detector(DetectUninitializedStorage())
     if args.detect_all or args.detect_uninitialized_memory:
         m.register_detector(DetectUninitializedMemory())
+    if args.detect_all or args.detect_reentrancy:
+        m.register_detector(DetectReentrancy())
 
     if args.avoid_constant:
         # avoid all human level tx that has no effect on the storage
         filter_nohuman_constants = FilterFunctions(regexp=r".*", depth='human', mutability='constant', include=False)
-        self.register_plugin(filter_nohuman_constants)
+        m.register_plugin(filter_nohuman_constants)
 
     logger.info("Beginning analysis")
 
@@ -139,6 +144,8 @@ def ethereum_cli(args):
 
 
 def main():
+    from .manticore import InstructionCounter, Visited, Tracer, RecordSymbolicBranches
+
     log.init_logging()
     args = parse_arguments()
 
@@ -153,6 +160,12 @@ def main():
 
     m = Manticore(args.argv[0], argv=args.argv[1:], env=env, entry_symbol=args.entrysymbol, workspace_url=args.workspace, policy=args.policy, disasm=args.disasm, concrete_start=args.data)
 
+    # Default plugins for now.. FIXME REMOVE!
+    m.register_plugin(InstructionCounter())
+    m.register_plugin(Visited())
+    m.register_plugin(Tracer())
+    m.register_plugin(RecordSymbolicBranches())
+
     # Fixme(felipe) remove this, move to plugin
     m.coverage_file = args.coverage
 

manticore/core/executor.py

@@ -384,6 +384,9 @@ def fork(self, state, expression, policy='ALL', setstate=None):
         # Find a set of solutions for expression
         solutions = state.concretize(expression, policy)
 
+        if not solutions:
+            logger.info("Forking on unfeasible constraint set")
+
         if len(solutions) == 1:
             setstate(state, solutions[0])
             return state
@@ -473,7 +476,6 @@ def run(self):
                         # expression
                         # policy
                         # setstate()
-
                         logger.debug("Generic state fork on condition")
                         current_state = self.fork(current_state, e.expression, e.policy, e.setstate)
 

manticore/core/smtlib/constraints.py

@@ -1,6 +1,6 @@
 
 from .expression import BitVecVariable, BoolVariable, ArrayVariable, Array, Bool, BitVec, BoolConstant, ArrayProxy, BoolEq, Variable, Constant
-from .visitors import GetDeclarations, TranslatorSmtlib, get_variables, simplify, replace
+from .visitors import GetDeclarations, TranslatorSmtlib, get_variables, simplify, replace, translate_to_smtlib
 import logging
 
 logger = logging.getLogger(__name__)
@@ -105,11 +105,9 @@ def __get_related(self, related_to=None):
             for constraint in self.constraints:
                 related_variables |= get_variables(constraint)
             related_constraints = set(self.constraints)
-
         return related_variables, related_constraints
 
-    def to_string(self, related_to=None, replace_constants=False):
-        replace_constants = True
+    def to_string(self, related_to=None, replace_constants=True):
         related_variables, related_constraints = self.__get_related(related_to)
 
         if replace_constants:
@@ -134,9 +132,15 @@ def to_string(self, related_to=None, replace_constants=False):
         translator = TranslatorSmtlib(use_bindings=True)
         for constraint in related_constraints:
             if replace_constants:
-                constraint = simplify(replace(constraint, constant_bindings))
-            translator.visit(constraint)
+                if isinstance(constraint, BoolEq) and \
+                   isinstance(constraint.operands[0], Variable) and \
+                   isinstance(constraint.operands[1], Constant):
+                    var = constraint.operands[0]
+                    expression = constraint.operands[1]
+                    expression = simplify(replace(expression, constant_bindings))
+                    constraint = var == expression
 
+            translator.visit(constraint)
         for name, exp, smtlib in translator.bindings:
             if isinstance(exp, BitVec):
                 result += '(declare-fun %s () (_ BitVec %d))' % (name, exp.size)
@@ -198,21 +202,27 @@ def migrate(self, expression, name=None, bindings=None):
         # Simply check there are no name overlappings
         if bindings is None:
             bindings = {}
-        if name is None:
-            name = self._get_new_name('migrated')
         variables = get_variables(expression)
         for var in variables:
+            if name is None:
+                name = self._get_new_name(var.name + '_migrated')
+
             if var in bindings:
                 continue
+
             if isinstance(var, Bool):
-                new_var = self.new_bool()
-            elif isinstance(expression, BitVec):
-                new_var = self.new_bitvec(var.size)
-            elif isinstance(expression, Array):
-                new_var = self.new_array(index_max=var.index_max, index_bits=var.index_bits, value_bits=var.value_bits)
+                new_var = self.new_bool(name=name)
+            elif isinstance(var, BitVec):
+                new_var = self.new_bitvec(var.size, name=name)
+            elif isinstance(var, Array):
+                new_var = self.new_array(index_max=var.index_max, index_bits=var.index_bits, value_bits=var.value_bits, name=name)
+            else:
+                raise NotImplemented("Unknown type {}".format(type(var)))
+
             bindings[var] = new_var
 
-        return replace(expression, bindings)
+        migrated_expression = replace(expression, bindings)
+        return migrated_expression
 
     def new_bool(self, name='B', taint=frozenset()):
         ''' Declares a free symbolic boolean in the constraint store

manticore/core/smtlib/expression.py

@@ -14,7 +14,7 @@ def __init__(self, taint=()):
         self._taint = frozenset(taint)
 
     def __repr__(self):
-        return "<%s at %x>" % (type(self).__name__, id(self))
+        return "<%s at %x%s>" % (type(self).__name__, id(self), self.taint and '-T' or '')
 
     @property
     def is_tainted(self):
@@ -46,6 +46,9 @@ def __deepcopy__(self, memo):
         memo[id(self)] = self
         return self
 
+    def __repr__(self):
+        return "<%s(%s) at %x>" % (type(self).__name__, self.name, id(self))
+
 
 class Constant(Expression):
     def __init__(self, value, *args, **kwargs):
@@ -654,7 +657,10 @@ def __getitem__(self, index):
             start, stop = self._fix_index(index)
             size = self._get_size(index)
             return ArraySlice(self, start, size)
-
+        else:
+            if self.index_max is not None:
+                if not isinstance(index, Expression) and index >= self.index_max:
+                    raise IndexError
         return self.select(self.cast_index(index))
 
     def __eq__(self, other):
@@ -700,15 +706,15 @@ def write_BE(self, address, value, size):
         value = BitVec(size * self.value_bits).cast(value)
         array = self
         for offset in range(size):
-            array = self.store(address + offset, BitVecExtract(value, (size - 1 - offset) * self.value_bits, self.value_bits))
+            array = array.store(address + offset, BitVecExtract(value, (size - 1 - offset) * self.value_bits, self.value_bits))
         return array
 
     def write_LE(self, address, value, size):
         address = self.cast_index(address)
         value = BitVec(size * self.value_bits).cast(value)
         array = self
         for offset in reversed(range(size)):
-            array = self.store(address + offset, BitVecExtract(value, (size - 1 - offset) * self.value_bits, self.value_bits))
+            array = array.store(address + offset, BitVecExtract(value, (size - 1 - offset) * self.value_bits, self.value_bits))
         return array
 
     def __add__(self, other):
@@ -784,9 +790,13 @@ def value(self):
 
 
 class ArraySlice(Array):
-    def __init__(self, array, offset, size):
+    def __init__(self, array, offset, size, *args, **kwargs):
         if not isinstance(array, Array):
             raise ValueError("Array expected")
+        if isinstance(array, ArrayProxy):
+            array = array._array
+        super(ArraySlice, self).__init__(array.index_bits, array.index_max, array.value_bits, *args, **kwargs)
+
         self._array = array
         self._slice_offset = offset
         self._slice_size = size
@@ -900,7 +910,7 @@ def store(self, index, value):
         self.written.add(index)
         auxiliar = self._array.store(index, value)
         self._array = auxiliar
-        return auxiliar
+        return self
 
     def __getitem__(self, index):
         if isinstance(index, slice):
@@ -1021,7 +1031,7 @@ class BitVecConcat(BitVecOperation):
     def __init__(self, size_dest, *operands, **kwargs):
         assert isinstance(size_dest, int)
         assert all(isinstance(x, BitVec) for x in operands)
-        assert size_dest == sum([x.size for x in operands])
+        assert size_dest == sum(x.size for x in operands)
         super(BitVecConcat, self).__init__(size_dest, *operands, **kwargs)
 
 

manticore/core/smtlib/solver.py

@@ -365,11 +365,10 @@ def get_all_values(self, constraints, expression, maxcnt=30000, silent=False):
             elif isinstance(expression, BitVec):
                 var = temp_cs.new_bitvec(expression.size)
             else:
-                raise NotImplementedError("get_all_values only implemted for Bool and BitVec")
+                raise NotImplementedError("get_all_values only implemented for Bool and BitVec")
 
             temp_cs.add(var == expression)
             self._reset(temp_cs.to_string(related_to=var))
-
             result = []
             val = None
             while self._check() == 'sat':
@@ -386,6 +385,7 @@ def get_all_values(self, constraints, expression, maxcnt=30000, silent=False):
                         break
                     else:
                         raise TooManySolutions(result)
+
             return result
 
     #@memoized