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 tutorial simple example incorrect #2583

Open
bzhang42 opened this issue Aug 25, 2022 · 7 comments
Open

Manticore tutorial simple example incorrect #2583

bzhang42 opened this issue Aug 25, 2022 · 7 comments
Labels
bug
Milestone
Manticore 0.4.0

Comments

@bzhang42
Copy link

Summary of the problem

Running the simple example on the Tutorial does not result in the correct output. https://github.com/trailofbits/manticore/wiki/Tutorial:-Running-under-Manticore

Manticore version

0.3.7

Python version

3.7

OS / Environment

Ubuntu (WSL)

Dependencies

I am using solc version 0.8.16.

Step to reproduce the behavior

Create a file called simple_example.sol:

pragma solidity >=0.4.24;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Then run manticore simple_example.sol.

Expected behavior

An output like the tutorial mentions, with multiple test cases:

...
... m.c.manticore:INFO: Generated testcase No. 0 - STOP
... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
... m.c.manticore:INFO: Generated testcase No. 4 - STOP
... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

Actual behavior

2022-08-25 15:31:37,907: [30234] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-08-25 15:31:37,907: [30234] m.main:INFO: Beginning analysis
2022-08-25 15:31:37,938: [30234] m.e.manticore:INFO: Starting symbolic create contract
2022-08-25 15:31:39,131: [30234] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-08-25 15:31:39,674: [30234] m.e.manticore:INFO: 1 alive states, 1 terminated states
2022-08-25 15:31:39,731: [30234] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-08-25 15:31:40,559: [30234] m.e.manticore:INFO: 1 alive states, 1 terminated states
2022-08-25 15:31:40,770: [30297] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
2022-08-25 15:31:40,775: [30297] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-25 15:31:42,111: [30234] m.c.manticore:INFO: Results in [redacted]
2022-08-25 15:31:42,112: [30234] m.c.manticore:INFO: Total time: 2.362511396408081

Any relevant logs

The user_00000000.tx file shows:

Transactions No. 0
Type: CREATE (0)
From: owner(0x10000) 
To: contract0(0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462) 
Value: 0 (*)
Gas used: 230000 
Data: 0x6080604052348015600f57600080fd5b50609e8061001e6000396000f300608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063b3de648b146044575b600080fd5b6060600480360381019080803590602001909291905050506062565b005b6041811415606f57600080fd5b505600a165627a7a72305820daaf2e537785ac684496ebcb086d2401e4b1dac4f633868ca73d99560e0a953c0029 
Return_data: 0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063b3de648b146044575b600080fd5b6060600480360381019080803590602001909291905050506062565b005b6041811415606f57600080fd5b505600a165627a7a72305820daaf2e537785ac684496ebcb086d2401e4b1dac4f633868ca73d99560e0a953c0029  (*)
Function call:
Constructor() -> RETURN 


Transactions No. 1
Type: CALL (0)
From: attacker(0x20000) 
To: contract0(0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462) 
Value: 1836912146 (*)
Gas used: 230000 
Data: 0xb3de648b00000000000000000000000000000000000000000000000000000000ff000041 (*)
Return_data: 0x () 

Function call:
f(4278190145) -> STOP (*)


Transactions No. 2
Type: CALL (0)
From: attacker(0x20000) 
To: contract0(0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462) 
Value: 0 (*)
Gas used: 230000 
Data: 0xb3de648b00000000000000000000000000000000ff000000000000000000000000000041 (*)
Return_data: 0x () 

Function call:
f(338953138925153547590470800371487866945) -> STOP (*)




(*) Example solution given. Value is symbolic and may take other values
@bzhang42 bzhang42 added the bug label Aug 25, 2022
@Kaylee-Hsu
Copy link

Kaylee-Hsu commented Aug 31, 2022 •
edited
Loading

I think I am having similar problem.

manticore version : 0.3.7
python version : 3.7
OS : Ubuntu 16.04

Expected behavior
From source : https://asciinema.org/a/154012

[I] mark ubuntu /m/h/c/m/e/evm (master) ❯ manticore umd_example.sol                                                                                                      ❮ 07:26
2017-12-22 19:26:36,308: [108889] m.main:INFO: Beginning analysis                                                                                                               
2017-12-22 19:26:36,372: [108889] m.ethereum:INFO: Starting symbolic transaction: 1                                                                                             
2017-12-22 19:26:37,076: [108889] m.ethereum:INFO: Generated testcase No. 0 - REVERT                                                                                            
2017-12-22 19:26:38,781: [108889] m.ethereum:INFO: Generated testcase No. 1 - REVERT                                                                                            
2017-12-22 19:26:40,927: [108889] m.ethereum:INFO: Generated testcase No. 2 - REVERT                                                                                            
2017-12-22 19:26:43,761: [108889] m.ethereum:INFO: Generated testcase No. 3 - REVERT                                                                                            
2017-12-22 19:26:46,297: [108889] m.ethereum:INFO: Generated testcase No. 4 - THROW                                                                                             
2017-12-22 19:26:48,629: [108889] m.ethereum:INFO: Finished symbolic transaction: 1 | Code Coverage: 100% | Terminated States: 5 | Alive States: 4                              
2017-12-22 19:26:48,640: [108889] m.ethereum:INFO: Generated testcase No. 5 - STOP                                                                                              
2017-12-22 19:26:51,005: [108889] m.ethereum:INFO: Generated testcase No. 6 - STOP                                                                                              
2017-12-22 19:26:53,372: [108889] m.ethereum:INFO: Generated testcase No. 7 - STOP                                                                                              
2017-12-22 19:26:55,730: [108889] m.ethereum:INFO: Generated testcase No. 8 - STOP                                                                                              
2017-12-22 19:26:58,145: [108889] m.ethereum:INFO: Results in /mnt/hgfs/code/manticore/examples/evm/mcore_nOeEvF

Actual behavior

$ manticore umd_example.sol 
2022-08-31 17:05:45,984: [27903] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-08-31 17:05:45,985: [27903] m.main:INFO: Beginning analysis
2022-08-31 17:05:45,986: [27903] m.e.manticore:INFO: Starting symbolic create contract
2022-08-31 17:05:46,828: [27903] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-08-31 17:06:16,999: [27903] m.e.manticore:INFO: 4 alive states, 2 terminated states
2022-08-31 17:06:17,353: [27903] m.e.manticore:INFO: Starting symbolic transaction: 1

2022-08-31 17:08:27,332: [27903] m.e.manticore:INFO: 16 alive states, 6 terminated states
2022-08-31 17:08:27,836: [28631] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
2022-08-31 17:08:27,837: [28631] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,841: [28629] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
2022-08-31 17:08:27,842: [28629] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,845: [28634] m.c.manticore:INFO: Generated testcase No. 2 - STOP(3 txs)
2022-08-31 17:08:27,846: [28634] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,881: [28632] m.c.manticore:INFO: Generated testcase No. 4 - STOP(3 txs)
2022-08-31 17:08:27,882: [28632] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,895: [28635] m.c.manticore:INFO: Generated testcase No. 5 - STOP(3 txs)
2022-08-31 17:08:27,909: [28630] m.c.manticore:INFO: Generated testcase No. 7 - STOP(3 txs)
2022-08-31 17:08:27,909: [28635] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,909: [28630] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,895: [28628] m.c.manticore:INFO: Generated testcase No. 3 - STOP(3 txs)
2022-08-31 17:08:27,910: [28628] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,916: [28633] m.c.manticore:INFO: Generated testcase No. 6 - STOP(3 txs)
2022-08-31 17:08:27,924: [28633] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,933: [28637] m.c.manticore:INFO: Generated testcase No. 8 - STOP(3 txs)
2022-08-31 17:08:27,934: [28637] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,947: [28641] m.c.manticore:INFO: Generated testcase No. 9 - STOP(3 txs)
2022-08-31 17:08:27,948: [28641] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:27,996: [28640] m.c.manticore:INFO: Generated testcase No. 10 - STOP(3 txs)
2022-08-31 17:08:27,996: [28640] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-08-31 17:08:31,044: [28629] m.c.manticore:INFO: Generated testcase No. 11 - STOP(3 txs)
2022-08-31 17:08:31,228: [28634] m.c.manticore:INFO: Generated testcase No. 12 - STOP(3 txs)
2022-08-31 17:08:31,265: [28630] m.c.manticore:INFO: Generated testcase No. 13 - STOP(3 txs)
2022-08-31 17:08:31,311: [28641] m.c.manticore:INFO: Generated testcase No. 14 - STOP(3 txs)
2022-08-31 17:08:31,445: [28631] m.c.manticore:INFO: Generated testcase No. 15 - STOP(3 txs)
2022-08-31 17:08:34,219: [27903] m.c.manticore:INFO: Results in /***/example/umd_example/mcore_cuh9jykm
2022-08-31 17:08:34,219: [27903] m.c.manticore:INFO: Total time: 136.78626823425293

@DaniWppner
Copy link

DaniWppner commented Sep 20, 2022 •
edited
Loading

From manticore version 3.6 onwards the cli defaults to quick-mode instead of thorough-mode.
Try running manticore simple_example.sol --thorough instead.

@0xharold
Copy link

0xharold commented Oct 3, 2022

Hi,
I am having similar issues:

  • manticore version : 0.3.7
  • python version : 3.8.10
  • OS : WSL2 -> Ubuntu

1. Using eth-security-toolbox in Docker

Once I run the following commands:

sudo docker run -it --rm -v $PWD:/src trailofbits/eth-security-toolbox

ethsec@fce73100d55f:~$ cd /src/contracts/manticore/exercise1/
ethsec@fce73100d55f:/src/contracts/manticore/exercise1$ manticore Example1.sol

then I get:

2022-10-03 12:41:04,609: [21] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-10-03 12:41:04,609: [21] m.main:INFO: Beginning analysis
2022-10-03 12:41:04,614: [21] m.e.manticore:INFO: Starting symbolic create contract
Process Process-1:
Traceback (most recent call last):
  File "/usr/lib/python3.6/multiprocessing/process.py", line 258, in _bootstrap
    self.run()
  File "/usr/lib/python3.6/multiprocessing/process.py", line 93, in run
    self._target(*self._args, **self._kwargs)
  File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1756, in worker_finalize
    finalizer(q.get_nowait())
  File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1747, in finalizer
    if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
AttributeError: 'NoneType' object has no attribute 'result'
2022-10-03 12:41:04,848: [21] m.c.manticore:INFO: Results in /src/contracts/manticore/exercise1/mcore_g5qqqyb9
2022-10-03 12:41:04,849: [21] m.c.manticore:WARNING: Manticore failed to run

or:

ethsec@fce73100d55f:/src/contracts/manticore/exercise1$ manticore Example1.sol --thorough

2022-10-03 12:42:30,387: [44] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSuicidal, DetectDelegatecall, DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance
2022-10-03 12:42:30,388: [44] m.main:INFO: Beginning analysis
2022-10-03 12:42:30,392: [44] m.e.manticore:INFO: Starting symbolic create contract
2022-10-03 12:42:30,660: [53] m.c.manticore:INFO: Generated testcase No. 0 - NO STATE RESULT (?)(0 txs)
2022-10-03 12:42:30,661: [53] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:42:30,734: [44] m.c.manticore:INFO: Results in /src/contracts/manticore/exercise1/mcore_z0ba6a_k
2022-10-03 12:42:30,735: [44] m.c.manticore:WARNING: Manticore failed to run

2. Using manticore in Docker

This one produce at least some results, but it still seems not to work as indented:

sudo docker run -it --rm -v $PWD:/src trailofbits/manticore

root@445568859aaa:/# cd /src/contracts/manticore/exercise1/
root@445568859aaa:/src/contracts/manticore/exercise1# manticore Example1.sol --thorough

I get:

2022-10-03 12:46:49,974: [34] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSuicidal, DetectDelegatecall, DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance
2022-10-03 12:46:49,974: [34] m.main:INFO: Beginning analysis
2022-10-03 12:46:49,976: [34] m.e.manticore:INFO: Starting symbolic create contract
2022-10-03 12:46:50,330: [34] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-10-03 12:46:50,719: [34] m.e.manticore:INFO: 1 alive states, 3 terminated states
2022-10-03 12:46:50,794: [34] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-10-03 12:46:51,654: [34] m.e.manticore:INFO: 1 alive states, 5 terminated states
2022-10-03 12:46:51,852: [116] m.c.manticore:INFO: Generated testcase No. 0 - REVERT(1 txs)
2022-10-03 12:46:51,856: [116] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:51,901: [117] m.c.manticore:INFO: Generated testcase No. 1 - REVERT(2 txs)
2022-10-03 12:46:51,903: [117] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:51,909: [119] m.c.manticore:INFO: Generated testcase No. 2 - REVERT(2 txs)
2022-10-03 12:46:51,921: [119] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:52,110: [115] m.c.manticore:INFO: Generated testcase No. 3 - STOP(3 txs)
2022-10-03 12:46:52,112: [115] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:52,171: [121] m.c.manticore:INFO: Generated testcase No. 4 - REVERT(3 txs)
2022-10-03 12:46:52,174: [121] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 12:46:52,430: [116] m.c.manticore:INFO: Generated testcase No. 5 - REVERT(3 txs)
2022-10-03 12:46:54,104: [34] m.c.manticore:INFO: Results in /src/contracts/manticore/exercise1/mcore_xh1ep81t
2022-10-03 12:46:54,105: [34] m.c.manticore:INFO: Total time: 3.3057878017425537

3. Using manticore standalone

This produces the same result as manticore in docker

pip install manticore

cd ./contracts/manticore/exercise1
manticore Example1.sol --thorough

I get the same results:

2022-10-03 14:48:28,750: [20899] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSuicidal, DetectDelegatecall, DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance
2022-10-03 14:48:28,750: [20899] m.main:INFO: Beginning analysis
2022-10-03 14:48:28,752: [20899] m.e.manticore:INFO: Starting symbolic create contract
2022-10-03 14:48:29,115: [20899] m.e.manticore:INFO: Starting symbolic transaction: 0
2022-10-03 14:48:29,592: [20899] m.e.manticore:INFO: 1 alive states, 3 terminated states
2022-10-03 14:48:29,682: [20899] m.e.manticore:INFO: Starting symbolic transaction: 1
2022-10-03 14:48:30,683: [20899] m.e.manticore:INFO: 1 alive states, 5 terminated states
2022-10-03 14:48:30,949: [20996] m.c.manticore:INFO: Generated testcase No. 0 - REVERT(1 txs)
2022-10-03 14:48:30,956: [20996] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:30,972: [20997] m.c.manticore:INFO: Generated testcase No. 1 - REVERT(2 txs)
2022-10-03 14:48:30,974: [20997] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:30,993: [20998] m.c.manticore:INFO: Generated testcase No. 2 - REVERT(2 txs)
2022-10-03 14:48:30,995: [20998] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:31,297: [21000] m.c.manticore:INFO: Generated testcase No. 3 - REVERT(3 txs)
2022-10-03 14:48:31,298: [21000] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:31,315: [20995] m.c.manticore:INFO: Generated testcase No. 4 - STOP(3 txs)
2022-10-03 14:48:31,319: [20995] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:31,402: [21002] m.c.manticore:INFO: Generated testcase No. 5 - REVERT(3 txs)
2022-10-03 14:48:31,414: [21002] m.c.plugin:WARNING: Caught will_solve in state None, but failed to capture its initialization
2022-10-03 14:48:33,507: [20899] m.c.manticore:INFO: Results in /home/haraslub/echidna-tutorial/contracts/manticore/exercise1/mcore_8cmmnfn8
2022-10-03 14:48:33,507: [20899] m.c.manticore:INFO: Total time: 3.821932315826416

@zeroonechange
Copy link

Using eth-security-toolbox in Docker

WSL Ubuntu 18.04.6 LTS
Docker version 20.10.20, build 9fdeb9c

ethsec@c805cd48e755:/code$ manticore manticore/examples/evm/umd_example.sol
2022-11-15 09:57:17,372: [51] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2022-11-15 09:57:17,373: [51] m.main:INFO: Beginning analysis
2022-11-15 09:57:17,375: [51] m.e.manticore:INFO: Starting symbolic create contract
Process Process-12:
Traceback (most recent call last):
File "/usr/lib/python3.6/multiprocessing/process.py", line 258, in _bootstrap
self.run()
File "/usr/lib/python3.6/multiprocessing/process.py", line 93, in run
self._target(*self._args, **self._kwargs)
File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1756, in worker_finalize
finalizer(q.get_nowait())
File "/home/ethsec/.local/lib/python3.6/site-packages/manticore/ethereum/manticore.py", line 1747, in finalizer
if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
AttributeError: 'NoneType' object has no attribute 'result'
2022-11-15 09:57:17,527: [51] m.c.manticore:INFO: Results in /code/mcore_t13shgmc
2022-11-15 09:57:17,527: [51] m.c.manticore:WARNING: Manticore failed to run

@ekilmer ekilmer added this to the Manticore 0.4.0 milestone Nov 30, 2022
@sachinbal
Copy link

@bzhang42 did you get a solution to the bug which you have raised? I too am facing a similar problem. Please share in case you have found out a solution or workaround for this issue.

@bzhang42
Copy link
Author

No solution so far. I decided to use hevm symbolic execution instead.

@spaceh3ad
Copy link

Using python3.8 for manticore solves this

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
Manticore 0.4.0
Development

No branches or pull requests
8 participants
@ekilmer @sachinbal @zeroonechange @bzhang42 @Kaylee-Hsu @spaceh3ad @DaniWppner @0xharold