Introduction to Manticore, a symbolic analysis tool for smart contract

In our previous blogs, we’ve explored two popular smart contract analysis tools, Mythril and Oyente. They deal with high level bug hunting for smart contracts, and output singular report to expose logic vulnerabilities, for instance code re-entry, uint wrapping, and etc. In this blog, we’re going to introduce another solidity audit tool that conducts detailed symbolic execution for smart contracts.

According to the official documentation of Manticore, it could:

• Auto-generate inputs for triggering different unique code paths
• Trace inputs that crashed the program
• Record instruction-level execution trace
• Expose its analysis engine via Python API

Manticore goes through different sections of code with a variety of attack scenarios (Therefore it runs extremely slow, but it’s all worth the waiting so be patient😆). What’s more, it not only aims at symbolic testing for solidity scripts, but also analyzes Linux ELF binaries (x86, x86_64 and ARMv7).

Installation:

• Dependencies:

Before installing Manticore, make sure your system is installed with solidity compiler solc and state-of-art theorem prover z3, by running:

solc --version && z3 --version

If you see something like this:

Then please skip installing solc and z3. If not, to install solc, run:

sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc

Then run in one line to install z3:

sudo apt-get update && sudo apt-get install z3 python-pip -y
python -m pip install -U pip

• Install Manticore:

git clone https://github.com/trailofbits/manticore.git 
cd manticore
sudo pip install --no-binary capstone .

• Check if it’s correctly installed:

Try testing if your system has correctly installed with Manticore, by analyzing a piece of binary code generated from gcc:

First, build the example .c files:

cd examples/linux
make

Secondly, “manticore” to try out the “basic.c”’s executable file “basic”:

manticore basic

The basic file is basically an “if statement”,which prints out “ Input message length > 0x41” or “Input message length ≤ 0x41”. Manticore would use symbolic execution to check this basic file and output the discovered two corresponding unique inputs into its report. This discovered “stdin” could be piped and checked by running:

cat mcore_*/*1.stdin | ./basic
cat mcore_*/*2.stdin | ./basic

• Usage:

(a) Manticore API:

$ manticore ./path/to/binary        # runs, and creates a mcore_* directory with analysis results
$ manticore ./path/to/binary ab cd  # use concrete strings "ab", "cd" as program arguments
$ manticore ./path/to/binary ++ ++  # use two symbolic strings of length two as program arguments
$ manticore ./path/to/contract.sol  # runs, and creates a mcore_* directory with analysis results

(b) Python API:

You could also use Python APIs to explore with your smart contract in detail, including executing concolic check, counting the number of instructions(which would come in handy when you’re concerned about the gas you’ll spend because more instructions cost more gas), and etc.

cd ../script
python Any_Python_Script_Listed_here.py Any_of_Your_Binarycode

Usage Experiments:

• Manticore Command Line Tool for safeMath.sol:

It took about 15 minutes to run the below in my Ubuntu VM:

manticore safeMath.sol

And it generates more than 80 test cases with detailed output:

Manticore Output for SafeMath.sol (1)

Manticore Output for SafeMath.sol (2)

The output reports are put into a folder, where inside of it, there are global reports(including .summary, .runtime_visited and etc.). For instance, the global.summary would summarize the vulnerabilities in this smart contract:

Global.summary

There are also different output reports for each specific test cases, for instance, .tx(reports this test case’s transaction type, contract address, owner address and etc), .summary(tested code’s offset, what’s the operation, whether this operation is successfully returned or reverted, and etc.), .trace, .logs, .pkl and etc.

• Python API “count_instructions.py” for HelloWorld.c:

The Python APIs can only take in binary code as input, so we chose to use HelloWorld.c’s executable binary file as input. We’ve already compiled the manticore/example/linux/ folder, so now we only have to:

cd ~/manticore/examples/script
python count_instructions.py ../example/linux/helloworld

Then it outputs with: “Executed 6251 instructions.”, which would be extremely useful when it comes to measure how much gas the smart contract would cost (But remember to use binary code for Python API). Feel free to experiment with the other APIs 🦁!

Conclusion:

Manticore is a super flexible smart contract audit tool. With its own command line tools and scriptable Python APIs, it could further answer questions like “Can the program reach this code at runtime?”, “ What is a program input that will cause execution of this code?” and etc(check Manticore’s blog for more details). Hope you’d enjoy exploring Manticore’s vast dynamic binary testing APIs and comment if you feel like a discussion.

By Yuan He, Security Researcher from HaloBlock.io