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

Gas related bug #1295

Open bingen opened 5 years ago

bingen commented 5 years ago

OS / Environment

I was using docker version. Ubuntu 16.04.5 LTS on host Ubuntu 18.04.1 LTS on container

Manticore version

(I was using docker version.) Manticore 0.2.2

Python version

I was using docker version. Python 3.6.6

Dependencies

asn1crypto==0.24.0 capstone==3.0.5.post1 cryptography==2.1.4 future==0.17.1 idna==2.6 keyring==10.6.0 keyrings.alt==3.0 manticore==0.2.2 ply==3.11 pycrypto==2.6.1 pyelftools==0.25 pyevmasm==0.1.0 pygobject==3.26.1 pysha3==1.0.2 python-apt==1.6.3 pyxdg==0.25 PyYAML==3.13 SecretStorage==2.3.1 six==1.11.0 unattended-upgrades==0.1 unicorn==1.0.1 z3-solver==4.8.0.0.post1

Summary of the problem

Exception while running manticore

Step to reproduce the behavior

docker run --rm -ti -v `pwd`:/src trailofbits/manticore bash
ulimit -s unlimited
manticore --detect-all --contract Staking /src/flattened_contracts/Staking.sol

You can find contract here: https://gist.github.com/bingen/abd7c11829a72c5bd71c18b33225d1d9 (just dismiss the last one, the Echidna one)

Actual behavior

This is the exception output:

2018-12-10 01:13:05,979: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
2018-12-10 01:16:52,201: [271] m.c.executor:ERROR: Exception: 
Traceback (most recent call last):
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/executor.py", line 467, in run
    if not current_state.execute():
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/state.py", line 141, in execute
    result = self._platform.execute()
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 2160, in execute
    self.current_vm.execute()
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 901, in execute
    last_pc, last_gas, instruction, arguments = self._checkpoint()
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 824, in _checkpoint
    self._consume(instruction.fee)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 747, in _consume
    enough_gas_solutions = solver.get_all_values(self.constraints, Operators.UGT(self._gas, fee))
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 383, in get_all_values
    while self._check() == 'sat':
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 281, in _check
    raise SolverException(_status)
manticore.exceptions.SolverException

2018-12-10 01:16:52,998: [271] m.ethereum:INFO: Generated testcase No. 0 - Solver failedRETURN
2018-12-10 01:16:53,047: [271] m.c.executor:ERROR: Exception: 
Traceback (most recent call last):
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/executor.py", line 467, in run
    if not current_state.execute():
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/state.py", line 141, in execute
    result = self._platform.execute()
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 2160, in execute
    self.current_vm.execute()
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 901, in execute
    last_pc, last_gas, instruction, arguments = self._checkpoint()
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 824, in _checkpoint
    self._consume(instruction.fee)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 747, in _consume
    enough_gas_solutions = solver.get_all_values(self.constraints, Operators.UGT(self._gas, fee))
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 383, in get_all_values
    while self._check() == 'sat':
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 281, in _check
    raise SolverException(_status)
manticore.exceptions.SolverException

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/executor.py", line 501, in run
    self.generate_testcase(current_state, "Solver failed" + str(e))
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/core/executor.py", line 358, in generate_testcase
    self._publish('will_generate_testcase', state, 'test', message)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 117, in _publish
    self._publish_impl(_name, *args, **kwargs)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 134, in _publish_impl
    sink._publish_impl(_name, *args, **kwargs)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 125, in _publish_impl
    callback(robj(), *args, **kwargs)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/ethereum/__init__.py", line 1385, in _generate_testcase_callback
    is_something_symbolic = state.platform.dump(stream, state, self, message)
  File "/home/manticore/.local/lib/python3.6/site-packages/manticore/platforms/evm.py", line 2370, in dump
    assert at_runtime != at_init
AssertionError

2018-12-10 01:23:00,818: [271] m.e.detectors:WARNING: Warning NUMBER instruction used
2018-12-10 03:42:04,517: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
2018-12-10 03:46:10,301: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
2018-12-10 05:48:28,386: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
2018-12-10 05:52:32,618: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
2018-12-10 07:28:22,865: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
2018-12-10 07:32:28,828: [271] m.c.s.solver:WARNING: Found an unknown core, probably a solver timeout
disconnect3d commented 5 years ago

As of 0.2.4 this still fails:

root@4010b00e1dd0:/src# manticore --contract Staking EchidnaStaking.sol
2019-01-14 16:29:24,071: [176] m.c.manticore:INFO: Verbosity set to 1.
2019-01-14 16:29:24,115: [176] m.main:INFO: Registered plugins: DetectReentrancyAdvanced, DetectSuicidal, DetectInvalid, DetectUnusedRetVal, DetectEnvInstruction, DetectExternalCallAndLeak, DetectUninitializedStorage, DetectUninitializedMemory, DetectDelegatecall, DetectIntegerOverflow, DetectReentrancySimple
2019-01-14 16:29:24,115: [176] m.main:INFO: Beginning analysis
2019-01-14 16:29:24,116: [176] m.e.manticore:INFO: Starting symbolic create contract

2019-01-14 16:30:34,943: [176] m.e.manticore:INFO: Starting symbolic transaction: 0
2019-01-14 17:45:12,243: [176] m.c.executor:ERROR: Exception:
Traceback (most recent call last):
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/executor.py", line 454, in run
    if not current_state.execute():
  File "/usr/local/lib/python3.6/dist-packages/manticore/ethereum/state.py", line 6, in execute
    return self._platform.execute()
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 2365, in execute
    self.current_vm.execute()
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 1028, in execute
    self._consume(fee)
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 811, in _consume
    enough_gas_solutions = get_possible_solutions()
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 796, in get_possible_solutions
    return solver.get_all_values(self.constraints, Operators.UGT(self._gas, fee))
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/smtlib/solver.py", line 408, in get_all_values
    while self._is_sat():
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/smtlib/solver.py", line 306, in _is_sat
    raise SolverError(status)
manticore.exceptions.SolverError

2019-01-14 17:45:12,565: [176] m.c.executor:ERROR: Exception:
Traceback (most recent call last):
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/executor.py", line 454, in run
    if not current_state.execute():
  File "/usr/local/lib/python3.6/dist-packages/manticore/ethereum/state.py", line 6, in execute
    return self._platform.execute()
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 2365, in execute
    self.current_vm.execute()
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 1028, in execute
    self._consume(fee)
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 811, in _consume
    enough_gas_solutions = get_possible_solutions()
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 796, in get_possible_solutions
    return solver.get_all_values(self.constraints, Operators.UGT(self._gas, fee))
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/smtlib/solver.py", line 408, in get_all_values
    while self._is_sat():
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/smtlib/solver.py", line 306, in _is_sat
    raise SolverError(status)
manticore.exceptions.SolverError

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/executor.py", line 488, in run
    self._publish('internal_generate_testcase', current_state, message="Solver failed" + str(e))
  File "/usr/local/lib/python3.6/dist-packages/manticore/utils/event.py", line 122, in _publish
    self._publish_impl(_name, *args, **kwargs)
  File "/usr/local/lib/python3.6/dist-packages/manticore/utils/event.py", line 139, in _publish_impl
    sink._publish_impl(_name, *args, **kwargs)
  File "/usr/local/lib/python3.6/dist-packages/manticore/utils/event.py", line 130, in _publish_impl
    callback(robj(), *args, **kwargs)
  File "/usr/local/lib/python3.6/dist-packages/manticore/core/manticore.py", line 97, in _publish_generate_testcase
    self._publish('will_generate_testcase', state, testcase, message)
  File "/usr/local/lib/python3.6/dist-packages/manticore/utils/event.py", line 122, in _publish
    self._publish_impl(_name, *args, **kwargs)
  File "/usr/local/lib/python3.6/dist-packages/manticore/utils/event.py", line 130, in _publish_impl
    callback(robj(), *args, **kwargs)
  File "/usr/local/lib/python3.6/dist-packages/manticore/ethereum/manticore.py", line 1379, in _generate_testcase_callback
    is_something_symbolic = state.platform.dump(stream, state, self, message)
  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 2591, in dump
    assert at_runtime != at_init
AssertionError