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

Manticore tutorial simple example incorrect #2583

Open bzhang42 opened 2 years ago

bzhang42 commented 2 years ago

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
Kaylee-Hsu commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

Hi, I am having similar issues:

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 commented 1 year ago

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

sachinbal commented 1 year ago

@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 commented 1 year ago

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

spaceh3ad commented 9 months ago

Using python3.8 for manticore solves this