How to interpret analysis results produced by Manticore?

OS / Environment

host: Ubuntu 18.04.2 , used provided Manticore docker image

Manticore version

0.2.5 (from docker image)

Python version

3.6.7 (from docker image)

Summary of the problem

Can you please answer my questions one by one?

[Question 1] When Manticore records "WARNING" message on command log, how can I know what line has the bug in the original source code? It seems there is no relevant documents. Although I do not know how to exactly interpret the analysis result, I have tried to understand it as follows.

According to the below log message that I attached (for entire log, see Any relevant logs below), Manticore says that it detected two overflow issues related to multiplication:

[21740] m.e.detectors: [[33mWARNING: [[0m Unsigned integer overflow at MUL instruction
[21740] m.e.detectors: [[33mWARNING: [[0m Unsigned integer overflow at MUL instruction

Manticore further says that the detailed analysis result is available in /mcore_tiskzgvy directory:

[21740] m.c.manticore: [[34mINFO: [[0m Results in /mcore_tiskzgvy

However, when I inspected the file global.findings in the directory, it contains only one issue:

- Unsigned integer overflow at MUL instruction -
  Contract: 0xafb6d63079413d167770de9c3f50db6477811bdb  EVM Program counter: 0xc2 (at constructor)
  Solidity snippet:
    54  totalSupply

which seems to say that only line 54 has the bug, which contradicts the command log (the log says Manticore produced two "WARNING" message as I described above).

[Question2] In my Question 1, why is there a discrepancy between the command log and the globals.finding file? Does Manticore detected just one issue?, i.e., is it enough to see globals.finding file to understand the analysis result?

[Question3] If Manticore does not record any "WARNING" messages on command log, then does this mean that Manticore detected no bugs?

Step to reproduce the behavior

I typed the following command to detect integer overflow bugs:

docker exec -it 2ad089fbd086 manticore --core.timeout 1800 //contract.sol --contract MyAdvancedToken --exclude delegatecall,reentrancy,reentrancy-adv,env-instr,ext-call-leak,suicidal,uninitialized-memory,uninitialized-storage,invalid,unused-return

where 2ad089fbd086 is a docker container's ID, and contract.sol is a contract available in: https://etherscan.io/address/0x9107C1B28d775E59f98BF3f4dE3b959816CF5526#code

Any relevant logs

[21740] m.c.manticore: [[34mINFO: [[0m Verbosity set to 1.
[21740] m.main: [[34mINFO: [[0m Registered plugins: DetectIntegerOverflow
[21740] m.main: [[34mINFO: [[0m Beginning analysis
[21740] m.e.manticore: [[34mINFO: [[0m Starting symbolic create contract 
[21740] m.e.detectors: [[33mWARNING: [[0m Unsigned integer overflow at MUL instruction
[21740] m.e.detectors: [[33mWARNING: [[0m Unsigned integer overflow at MUL instruction
[21740] m.e.manticore: [[34mINFO: [[0m Starting symbolic transaction: 0
[21740] m.e.manticore: [[34mINFO: [[0m 1 alive states, 5 terminated states
[21740] m.c.manticore: [[34mINFO: [[0m Generated testcase No. 0 - RETURN
[23710] m.c.manticore: [[34mINFO: [[0m Generated testcase No. 1 - REVERT
[23710] m.c.manticore: [[34mINFO: [[0m Generated testcase No. 2 - RETURN
[23710] m.c.manticore: [[34mINFO: [[0m Generated testcase No. 3 - REVERT
[23710] m.c.manticore: [[34mINFO: [[0m Generated testcase No. 4 - REVERT
[23710] m.c.manticore: [[34mINFO: [[0m Generated testcase No. 5 - REVERT
[21740] m.c.manticore: [[34mINFO: [[0m Results in /mcore_tiskzgvy
[21740] m.c.manticore: [[34mINFO: [[0m Total time: 1170.35377907753^M

Manticore tries to explore all possible paths of your contract and generate reproducible input for each case. The cli will send all kind of transactions until no more code coverage is discovered. Manticore cli comes with a pack of default detectors turned on (ex. int overflow). These will print warning as soon as they suspect that a state behaves in certain way and at the end this is going to be collapsed at global.findings. You can turn them off with --exclude-all.

[Question 1] The IO overflow reports the potential int overflow (*) as soon as possible and at every state/contract code path that has it. If there are a few ways to reach the same int overflow mcore will print warnings for each. Also, Manticore sends a lot of tx to the emulated contract, it even send that same tx a few times to see if that enables new code paths.

[Question 2]

In my Question 1, why is there a discrepancy between the command log and the globals.finding file?

Global.findings colapses findings that happen at different situations but at the same line. So the analyst can just go to that solidity line and see.

Does Manticore detected just one issue?

Yes. Mcore found 2 ways to reach that line with some input that would make it overflow in some way. The analyst, though, should check only that solidity line for an integer overflow.

, i.e., is it enough to see globals.finding file to understand the analysis result?

Yes. The findings and detected things depend on the default detectors enabled. IMO, the best part of the analysis is all the high coverage testcases you'll find in the output folder. Ideally you should check all of it to see if you can break any contract invariant (whatever that is for you) at any of them. (there is an API for that)

[Question 3] If no warning is printed and it finishes, then it has no detected "bugs". It means that the implemented detectors did not find any contract path that match with their specific property. You can check the obtained coverage as a measure of exploration completeness. Manticore will do a great effort to exercise all possible contract paths, though there are certain limitations (dynamic of great size arguments, calldata size, number of symbolic transactions, etc) In the output folder you will find the transaction trace fo all different contract states hat manticore found. You can see account balances and all that to check manually that nothing really bad happened.

trailofbits / manticore