Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Manticore (via Docker pull/ run) had exceptions on VulnerableToken Youtube example #2579

Open
ronenbitman opened this issue Aug 15, 2022 · 1 comment
Open

Manticore (via Docker pull/ run) had exceptions on VulnerableToken Youtube example #2579

ronenbitman opened this issue Aug 15, 2022 · 1 comment
Labels
bug

Comments

@ronenbitman
Copy link

Summary of the problem

this is my power shell output from the following command

i have a few questions

  • in the video [https://www.youtube.com/watch?v=o6pmBJZpKAc] there was no exceptions, can you please clarify if this is as defined, and if not how can i resolve it
  • in the video the system found a vulnerability in the math overflow, however in my output it didn't, it seems the registered plugins that comes with the docker image are different than the ones in the example, can you advise why and how is it possible to 'enhance' them to all available plugins
  • the video the run time stands at 45sec (for this simple contract) while my runtime is 260sec can you advise on what are the differences and how am i able to make it faster (hardware? software? parameters?)
  • can you please refer me to a library of examples / outputs (ran on latest version)
  • can you provide a link to an API documentation

Manticore version

Name: manticore
Version: 0.3.7
Summary: Manticore is a symbolic execution tool for analysis of binaries and smart contracts.
Home-page: https://github.com/trailofbits/manticore
Author: Trail of Bits
Author-email:
License:
Location: /usr/local/lib/python3.7/dist-packages
Requires: crytic-compile, intervaltree, ply, prettytable, protobuf, pyevmasm, pysha3, pyyaml, rlp, wasm, z3-solver
Required-by:

Python version

n/a

OS / Environment

n/a

Dependencies

asn1crypto==0.24.0
capstone==5.0.0rc2
cryptography==2.1.4
crytic-compile==0.2.3
cytoolz==0.12.0
eth-hash==0.3.3
eth-typing==3.1.0
eth-utils==2.0.0
future==0.18.2
idna==2.6
importlib-metadata==4.12.0
intervaltree==3.1.0
keyring==10.6.0
keyrings.alt==3.0
manticore @ file:///manticore
ply==3.11
prettytable==3.3.0
protobuf==3.20.1
pycrypto==2.6.1
pyelftools==0.28
pyevmasm==0.2.3
PyGObject==3.26.1
pysha3==1.0.2
pyxdg==0.25
PyYAML==6.0
rlp==3.0.0
SecretStorage==2.3.1
six==1.11.0
sortedcontainers==2.4.0
toolz==0.12.0
typing_extensions==4.3.0
unicorn==2.0.0
wasm==1.2
wcwidth==0.2.5
z3-solver==4.10.2.0
zipp==3.8.1

Step to reproduce the behavior

docker pull trailofbits/manticore

docker run -it -v ${pwd}:/mysrc --ulimit stack=10000000:10000000 trailofbits/manticore bash -c "rm /usr/bin/solc && pip3 install solc-select && solc-select install 0.5.12 && solc-select use 0.5.12 && manticore mysrc/VulnerableToken.sol --txaccount attacker --txlimit 3"

`
VulnerableToken.sol

pragma solidity 0.5.12;
contract VulnerableToken{
mapping(address=>uint) private balances;
address public owner;

constructor() public {
    owner = msg.sender;
    balances[owner] = 1000000;    
}

function fund() payable public {
    uint n = msg.value;
    balances[msg.sender] += n;
    if (n<balances[owner]){
        balances[owner] += n;
    }
}

function burn(uint val) public {
    require(balances[msg.sender]> 0);
    balances[msg.sender] -= val;
}

function takeOwnership() public {
    require(balances[owner]<balances[msg.sender]);
    owner = msg.sender;
}

}'

Expected behavior

https://www.youtube.com/watch?v=o6pmBJZpKAc

Actual behavior

Collecting solc-select
Downloading solc_select-0.2.1-py3-none-any.whl (16 kB)
Installing collected packages: solc-select
Successfully installed solc-select-0.2.1
WARNING: Running pip as the 'root' user can result in broken permissions and conflicting behaviour with the system package manager. It is recommended to use a virtual environment instead: https://pip.pypa.io/warnings/venv
Installing '0.5.12'...
Version '0.5.12' installed.
Switched global version to 0.5.12
2022-08-15 04:51:32,914: [1] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-08-15 04:51:32,914: [1] m.main:INFO: Beginning analysis
2022-08-15 04:51:32,916: [1] m.e.manticore:INFO: Starting symbolic create contract
2022-08-15 04:51:34,097: [1] m.e.manticore:INFO: Found a concrete globalsha3 b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' -> 32434096268151414502930714319429211172703610272722345406708838912687411675598
2022-08-15 04:51:34,618: [1] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-08-15 04:51:41,657: [1] m.e.manticore:INFO: Found a concrete globalsha3 b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' -> 73138091548938366139099779971772605061518111956507126412222883840269740007539
2022-08-15 04:51:59,572: [1] m.e.manticore:INFO: 2 alive states, 3 terminated states
2022-08-15 04:52:00,388: [1] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-08-15 04:53:02,967: [1] m.c.worker:ERROR: Exception in state 0: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 137, in run
current_state.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/ethereum/state.py", line 8, in execute
return self._platform.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 3106, in execute
self.current_vm.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 1322, in execute
raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 158, in run
m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
File "/usr/local/lib/python3.7/dist-packages/manticore/core/manticore.py", line 518, in _fork
raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

2022-08-15 04:53:17,036: [1] m.e.manticore:INFO: 7 alive states, 3 terminated states
2022-08-15 04:53:17,666: [1] m.e.manticore:INFO: Starting symbolic transaction: 2
2022-08-15 04:55:16,473: [1] m.c.worker:ERROR: Exception in state 6: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 137, in run
current_state.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/ethereum/state.py", line 8, in execute
return self._platform.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 3106, in execute
self.current_vm.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 1322, in execute
raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 158, in run
m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
File "/usr/local/lib/python3.7/dist-packages/manticore/core/manticore.py", line 518, in _fork
raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

2022-08-15 04:55:45,517: [1] m.c.worker:ERROR: Exception in state 3: ManticoreError('Forking on unfeasible constraint set')
Traceback (most recent call last):
File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 137, in run
current_state.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/ethereum/state.py", line 8, in execute
return self._platform.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 3106, in execute
self.current_vm.execute()
File "/usr/local/lib/python3.7/dist-packages/manticore/platforms/evm.py", line 1322, in execute
raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "/usr/local/lib/python3.7/dist-packages/manticore/core/worker.py", line 158, in run
m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
File "/usr/local/lib/python3.7/dist-packages/manticore/core/manticore.py", line 518, in _fork
raise ManticoreError("Forking on unfeasible constraint set")
manticore.exceptions.ManticoreError: Forking on unfeasible constraint set

2022-08-15 04:56:58,907: [135] m.c.manticore:INFO: Generated testcase No. 0 - STOP(4 txs)
2022-08-15 04:56:58,908: [135] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:58,918: [129] m.c.manticore:INFO: Generated testcase No. 1 - STOP(4 txs)
2022-08-15 04:56:58,919: [129] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:58,997: [118] m.c.manticore:INFO: Generated testcase No. 2 - STOP(4 txs)
2022-08-15 04:56:58,998: [118] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,154: [127] m.c.manticore:INFO: Generated testcase No. 3 - STOP(4 txs)
2022-08-15 04:56:59,155: [127] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,220: [134] m.c.manticore:INFO: Generated testcase No. 4 - STOP(4 txs)
2022-08-15 04:56:59,221: [134] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,269: [120] m.c.manticore:INFO: Generated testcase No. 5 - STOP(4 txs)
2022-08-15 04:56:59,271: [120] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,483: [116] m.c.manticore:INFO: Generated testcase No. 6 - STOP(4 txs)
2022-08-15 04:56:59,484: [116] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,527: [122] m.c.manticore:INFO: Generated testcase No. 8 - STOP(4 txs)
2022-08-15 04:56:59,528: [117] m.c.manticore:INFO: Generated testcase No. 7 - STOP(4 txs)
2022-08-15 04:56:59,528: [122] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,529: [117] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:56:59,709: [119] m.c.manticore:INFO: Generated testcase No. 9 - STOP(4 txs)
2022-08-15 04:56:59,710: [119] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:57:00,075: [132] m.c.manticore:INFO: Generated testcase No. 10 - STOP(4 txs)
2022-08-15 04:57:00,077: [132] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its
initialization
2022-08-15 04:57:05,838: [135] m.c.manticore:INFO: Generated testcase No. 11 - STOP(4 txs)
2022-08-15 04:57:08,641: [129] m.c.manticore:INFO: Generated testcase No. 12 - STOP(4 txs)
2022-08-15 04:57:09,758: [118] m.c.manticore:INFO: Generated testcase No. 13 - STOP(4 txs)
2022-08-15 04:57:10,201: [127] m.c.manticore:INFO: Generated testcase No. 14 - STOP(4 txs)
2022-08-15 04:57:10,455: [120] m.c.manticore:INFO: Generated testcase No. 15 - STOP(4 txs)
2022-08-15 04:57:11,914: [122] m.c.manticore:INFO: Generated testcase No. 16 - STOP(4 txs)
2022-08-15 04:57:12,044: [117] m.c.manticore:INFO: Generated testcase No. 17 - STOP(4 txs)
2022-08-15 04:57:13,458: [132] m.c.manticore:INFO: Generated testcase No. 18 - STOP(4 txs)
2022-08-15 04:57:13,829: [116] m.c.manticore:INFO: Generated testcase No. 19 - STOP(4 txs)
2022-08-15 04:57:14,656: [135] m.c.manticore:INFO: Generated testcase No. 20 - STOP(4 txs)
2022-08-15 04:57:16,732: [120] m.c.manticore:INFO: Generated testcase No. 21 - STOP(4 txs)
2022-08-15 04:57:16,759: [129] m.c.manticore:INFO: Generated testcase No. 22 - STOP(4 txs)
2022-08-15 04:57:17,088: [127] m.c.manticore:INFO: Generated testcase No. 23 - STOP(4 txs)
2022-08-15 04:57:18,619: [122] m.c.manticore:INFO: Generated testcase No. 24 - STOP(4 txs)
2022-08-15 04:57:38,289: [1] m.c.manticore:INFO: Results in /mcore_ek8k5z_d
2022-08-15 04:57:38,290: [1] m.c.manticore:INFO: Total time: 260.28980922698975

Any relevant logs
@mertcmutlu
Copy link

mertcmutlu commented Aug 24, 2022 •
edited

Same problem here. Any help would be appreciated.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mertcmutlu @ronenbitman