search

trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.69k stars 472 forks source link

TooManySolutions crash #488

Open sjcappella opened 7 years ago

sjcappella commented 7 years ago

OS / Environment

Ubuntu Description: Ubuntu 16.10 Release: 16.10 Codename: yakkety

Manticore version

Version: 0.1.4

Python version

Python 2.7.12+

Dependencies

capstone==4.0.0rc1 manticore==0.1.4 pyelftools==0.24 unicorn==1.0.1

Summary of the problem

Manticore exists analysis of a DECREE binary earlier than expected.

Step to reproduce the behavior

$ manticore YAN01_00012

Expected behavior

Manticore should spin in an analysis loop forking a lot of states due to the 'read until' nature of the binary.

Actual behavior

Manticore exists after about 17 seconds and doesn't generate any test cases our output besides a command.sh and visited.txt

YAN01_00012.zip

offlinemark commented 6 years ago

Bounty

catenacyber commented 6 years ago

Not sure if the problem is still present :

> manticore YAN01_00012 --env LD_LIBRARY_PATH=/usr/local/lib/linux/
2018-06-01 10:00:05,520: [35154] m.manticore:INFO: Loading program YAN01_00012
2018-06-01 10:00:06,845: [35154] m.c.executor:ERROR: Exception: Max number of different solutions hit
Traceback (most recent call last):
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/executor.py", line 475, in run
    current_state = self.fork(current_state, e.expression, e.policy, e.setstate)
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/executor.py", line 382, in fork
    solutions = state.concretize(expression, policy)
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/state.py", line 292, in concretize
    silent=False)
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/smtlib/solver.py", line 372, in get_all_values
    raise TooManySolutions(result)
TooManySolutions: Max number of different solutions hit

2018-06-01 10:00:07,963: [35154] m.c.executor:ERROR: Exception: Max number of different solutions hit
Traceback (most recent call last):
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/executor.py", line 475, in run
    current_state = self.fork(current_state, e.expression, e.policy, e.setstate)
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/executor.py", line 382, in fork
    solutions = state.concretize(expression, policy)
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/state.py", line 292, in concretize
    silent=False)
  File "/usr/local/lib/python2.7/site-packages/manticore-0.1.9-py2.7.egg/manticore/core/smtlib/solver.py", line 372, in get_all_values
    raise TooManySolutions(result)
TooManySolutions: Max number of different solutions hit

2018-06-01 10:00:08,157: [35154] m.manticore:INFO: Results in mcore_EiTdLy
2018-06-01 10:00:08,157: [35154] m.manticore:INFO: Total time: 2.5704729557

That TooManySolutionsexception seems to be the expected behavior, doesn't it ?

offlinemark commented 6 years ago

Hm, so ideally we wouldn't just choke and error with TooManySolutions; we should find some way to keep going.

offlinemark commented 6 years ago

re #1097