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.7k stars 472 forks source link

Mutexes for global context are not reliable #1528

Open tpetersonkth opened 5 years ago

tpetersonkth commented 5 years ago

OS / Environment

No LSB modules are available. Distributor ID: Ubuntu Description: Ubuntu 18.04.3 LTS Release: 18.04 Codename: bionic

Manticore version

Version: 0.3.0

Python version

Python 3.6.8

Dependencies

alabaster==0.7.12 apsw==3.16.2.post1 asn1crypto==0.24.0 attrs==18.2.0 Automat==0.7.0 awscli==1.16.107 Babel==2.6.0 backports.functools-lru-cache==1.4 backports.ssl-match-hostname==3.5.0.1 beautifulsoup4==4.6.0 boto==2.44.0 botocore==1.12.97 cached-property==1.3.1 capstone==4.0.1 Cerealizer==0.8.2 certifi==2018.11.29 chardet==3.0.4 CherryPy==8.9.1 cliapp==1.20170827 click==6.7 cmdtest==0.32 colorama==0.3.9 constantly==15.1.0 coverage==4.5.2 crcmod==1.7 cryptography==2.1.4 cssselect==1.0.3 cssutils==1.0.2 cycler==0.10.0 Cython==0.27.3 deluge==1.3.15 dnspython==1.15.0 docker==2.5.1 docker-compose==1.17.1 docker-pycreds==0.2.1 dockerpty==0.4.1 docopt==0.6.2 docutils==0.14 enum34==1.1.6 feedparser==5.2.1 filelock==3.0.10 fretwork==0.3.0 funcsigs==1.0.2 functools32==3.2.3.post2 futures==3.2.0 google-compute-engine==2.8.16 html5-parser==0.4.4 html5lib==0.999999999 hyperlink==18.0.0 idna==2.8 imagesize==1.1.0 incremental==17.5.0 ipaddress==1.0.17 Jinja2==2.10 jmespath==0.9.3 jsonschema==2.6.0 keyring==10.6.0 keyrings.alt==3.0 Lab==3.0 lizard==1.16.3 lxml==4.2.1 Markdown==2.6.9 MarkupSafe==1.1.0 matplotlib==2.1.1 mechanize==0.2.5 mercurial==4.5.3 mock==2.0.0 msgpack==0.5.6 netifaces==0.10.4 numpy==1.15.3 olefile==0.44 packaging==19.0 PAM==0.4.2 pbr==3.1.1 pdfminer==20140328 Pillow==4.3.0 pluggy==0.8.1 py==1.7.0 pyasn1==0.4.5 pyasn1-modules==0.2.4 PyAudio==0.2.11 pycairo==1.16.2 pycrypto==2.6.1 pycurl==7.43.0.1 pyenet==1.3.13.post7 pygame==1.9.5.dev0 Pygments==2.3.1 pygobject==3.26.1 PyHamcrest==1.9.0 pyliblzma==0.5.3 PyOgg==0.6.6a1 PyOpenGL==3.1.0 PyOpenGL-accelerate==3.1.0 pyOpenSSL==17.5.0 pyparsing==2.3.1 pyserial==3.4 pysqlite==1.0.1 python-apt==1.6.4 python-dateutil==2.8.0 python-libtorrent==1.1.5 python-magic==0.4.16 pytz==2018.9 pyxdg==0.25 PyYAML==3.13 regex==2017.12.12 repoze.lru==0.7 requests==2.21.0 Routes==2.4.1 rpm==4.14.1 rsa==3.4.2 s3transfer==0.2.0 scipy==1.1.0 SecretStorage==2.3.1 service-identity==18.1.0 simplejson==3.13.2 six==1.12.0 snowballstemmer==1.2.1 Sphinx==1.8.4 sphinxcontrib-websupport==1.1.0 subprocess32==3.2.7 texttable==0.9.1 toml==0.10.0 tox==3.7.0 tox-venv==0.3.1 ttystatus==0.38 Twisted==18.9.0 typing==3.6.6 urlgrabber==3.10.2 urllib3==1.24.1 uTidylib==0.3 vboxapi==1.0 virtualenv==16.4.0 webencodings==0.5 WebOb==1.7.3 websocket-client==0.44.0 yum-metadata-parser==1.1.4 zope.interface==4.6.0

Summary of the problem

When storing something in the global context of manticore, there appears to be some sort of race condition which results in lost information. Somehow, the mutex ("with m.locked_context() as context:" where m=Manticcore([path to binary])) does not appear to function correctly.

Step to reproduce the behavior

I have minimized and documented a small example that I used to generate the log output below(Under "Any relevant logs"). To reproduce, download reproduce.zip and extract symbolicExecutor.py, customPlugins.py and doubleCallRet(DoubleCallRet is a binary that I analyze for the example). Then, open a terminal and cd into the folder where the files were extracted and execute "for i in {1..500}; do python3 symbolicExecutor.py; done". (Sometimes you have to increase the for loop to iterate more than 500 times before you get one execution with the problem. But I have found that when executing symbolicExecutor.py 500 times it is pretty likely that I get atleast 1 incorrect execution claiming that path 0 is infeasible)

reproduce.zip

Expected behavior

It is expected that the following lines are printed: Path 0[len=10] ending with 0x80480cc has the following successors 0x80480a9 Path 1[len=15] ending with 0x80480cb has the following successors 0x80480b3

Actual behavior

Sometimes the successor address of 0x80480cc is lost. Instead the program outputs: Path 0[len=10] is infeasible Path 1[len=15] ending with 0x80480cb has the following successors 0x80480b3

Any relevant logs

output.txt

feliam commented 5 years ago

I can confirm that something is not getting updated right with shared_contexts vs multiprocessing. Use this as a wrokaround?

cfg = config.get_group("core")
cfg.mprocessing = cfg.mprocessing.threading
cfg.procs = 30