trailofbits/manticore

manticore sometimes reports "overflow" for "underflow or "overflow/underflow"

Open

#1,101 opened on Aug 31, 2018

View on GitHub
 (0 comments) (0 reactions) (0 assignees)Python (481 forks)batch import
bugethereumhelp wanted

Repository metrics

Stars
 (3,469 stars)
PR merge metrics
 (No merged PRs in 30d)

Description

OS / Environment

Description: Ubuntu 18.04.1 LTS Release: 18.04 Codename: bionic

Manticore version

Version: 0.2.0

Python version

Python 3.6.

Dependencies

asn1crypto==0.24.0 atomicwrites==1.1.5 attrdict==2.0.0 attrs==18.1.0 capstone==3.0.5 certifi==2018.4.16 cffi==1.11.5 chardet==3.0.4 click==6.7 coincurve==8.0.0 configparser==3.5.0 coverage==4.5.1 cytoolz==0.9.0.1 dictionaries==0.0.1 eth-abi==1.1.1 eth-account==0.3.0 eth-hash==0.1.4 eth-keyfile==0.5.1 eth-keys==0.2.0b3 eth-rlp==0.1.2 eth-tester==0.1.0b29 eth-utils==1.0.3 ethereum==2.3.2 -e git+git@bitbucket.org:rockybernstein/evm-bytecode.git@80855f3eb9f8c5f7240f63d63f7c54ff19f59860#egg=evm_bytecode flake8==3.5.0 future==0.16.0 hexbytes==0.1.0 hypothesis==3.0.0 idna==2.7 Jinja2==2.10 manticore==0.2.0 markdown2==2.3.5 MarkupSafe==1.0 mccabe==0.6.1 mock==2.0.0 more-itertools==4.2.0 mythril==0.18.11 nose==1.3.7 parsimonious==0.8.0 pbkdf2==1.3 pbr==4.2.0 persistent==4.2.4.2 pkginfo==1.4.2 pluggy==0.6.0 ply==3.11 plyvel==1.0.5 py==1.5.4 py-ecc==1.4.3 py-flags==1.1.2 py-solc==3.1.0 pycodestyle==2.3.1 pycparser==2.18 pycryptodome==3.6.4 pyelftools==0.24 pyethash==0.1.27 pyevmasm==0.1.0 pyflakes==1.6.0 Pygments==2.2.0 pygments-lexer-solidity==0.3.1 PyQt5==5.11.2 PyQt5-sip==4.19.11 pysha3==1.0.2 pytest==3.6.3 pytest-cov==2.5.1 pytest-mock==1.10.0 pytest-qt==2.4.1 pytest-runner==4.2 PyYAML==3.13 repoze.lru==0.7 requests==2.19.1 requests-toolbelt==0.8.0 rlp==1.0.1 scrypt==0.8.6 semantic-version==2.6.0 six==1.11.0 toolz==0.9.0 tqdm==4.23.4 transaction==2.2.1 twine==1.11.0 unicorn==1.0.1 urllib3==1.23 -e git+git@github.com:rocky/python-xdis.git@c77847dd466c9f9a34310346b6ea6c67c3989ae0#egg=xdis z3-solver==4.5.1.0.post2 zope.interface==4.5.

Summary of the problem

Step to reproduce the behavior

$ cd ethereum-analyzer-suites-runner
$ manticore --detect-all benchmarks/Suhabe/benchmarks/integer_overflow_minimal.sol 

Look in mcore's global.findings

Expected behavior

- Unsigned integer underflow at SUB instruction -

or

- Unsigned integer overflow/underflow at SUB instruction -

Actual behavior

- Unsigned integer overflow at SUB instruction -

Contributor guide