Introduction
Smart contracts are self-executing pieces of code that run on distributed ledgers called the “blockchain”. The Ethereum Virtual Machine and other blockchains that are compatible in architecture e.g. Celo are capable of resistance to censorship, downtime, and third-party interference, and have since invented changed how software is perceived. As exciting as smart contracts are, they could introduce high-risk of financial loss especially where exchanging of value (usually monetarily) is involved if not properly scrutinized. It then becomes crucial for developers to analyze contract code before deployment to a live network.
Prerequisites
This guide introduces you to working with a security tool called Manticore. I assume you already have experience working with smart contracts using solidity language. If you’re new to this, I recommend reading through Building a Solidity Smart Contract for NFT Royalty Fees - A Step-by-Step Guide - Technical Tutorials - Celo Academy by @Kunaldawar and Best Practices for Writing Smart Contracts with Real World Examples - Technical Tutorials - Celo Academy to get started.
Requirements
Manticore is a Python-based tool with unusual dependencies such as Z3, protobuf, etc, and performs better on Linux-based operating systems compared to Windows OS. I recommend using WSL if you are on Windows. Follow Install WSL | Microsoft Learn to set up WSL on Windows.
Install the following before proceeding.
-
Python3.7 or later
-
Manticore officially supports the latest LTS version of Ubuntu
-
Editor/IDE. VSCode recommended
-
Python package manager - PIP
sudo apt updatesudo apt install python3-pippip3 --version
What is Manticore?
Manticore is a symbolic execution tool for analyzing binaries and smart contracts. It can be used to check and analyze binaries in Linux, for WASM, and EVM using bytecode. With Manticore, developers are able to check for vulnerabilities in smart contracts code written in solidity that are compiled to the EVM bytecode via a technique that uses constraint solving to systematically explore a program’s state space. It is different from other analysis tools because it is property-based i.e. it runs a series of tests on the smart contracts using properties rather than testing a few behaviors.
Usually, as web3 developers, when we write tests, we want to check if our code is correct. We want the test to follow the patterns:
- Setting or specifying sequences of interactions such as
- Approve
- transferFrom
- the, expected balances should tally
- Examine the result
- Iterating the steps on every commit
If we think this way, then we could say writing unit tests for everything is hard and time-consuming.
Why Manticore?
The problem arises from the fact that as developers, we don’t test most behaviors by asking ourselves some unusual questions such as:
- What if the order of calls changes?
- What if
approvalortransferFromis called twice?
Let’s examine some of the differences between unit and property tests.
| SN | UNIT | PROPERTY |
|---|---|---|
| 1 | Most tests devs carried out cover only single input | Property test covers any possible inputs |
| 2 | Covers cases that you know about | Covers cases that you don’t know about |
| 3 | Specifies a single transaction sequence. Ex. If Alice calls "r()", it sends Bob 3 ETH. If she then calls "v()", she’ll have 4 ETH |
Using mathematical models, checks for all possible transaction sequences. Ex. Irrespective of which method is called by Alice, Bob can’t lose money |
| 4 | Reasons about a few possible inputs | The set of possible inputs are giant: reasons about all of them |
| 5 | One test : One-way to check | One test : two-way to check |
| 6 | - | If generates 10000 pairs of units, calls function “f” with all of them, and check the properties on each of them |
| 7 | - | Executes with any possible initial value |
| 8 | - | Checks for possibility of failure |
| 9 | - | Uses solvers for constraints e.g Z3, Yices etc |
| 10 | Easy to set up. You could miss stuff | Lots of effort to set up. It uses effective formal verification |
| 11 | Less assurance | Super high assurance |
Note: If you need a good test suite or correctness, use Manticore
Installing Manticore
To use Manticore, be sure Python is installed on your machine since we will need the Python package manager - Pip to install the tool. If you need to install it from scratch, please follow the steps I itemized here.
To get the best result and avoid dependency conflict, you could run Manticore in a Virtual box or create a virtual environment.
Steps
- I assume you have installed the necessary tools and running the Ubuntu OS
pip3 install manticore
Note: Installing Manticore also installs
capstoneandZ3solver But if you need to install is separate, run the command below
sudo pip3 install --no-binary capstone .
sudo apt-get update && sudo apt-get install z3
Open the Ubuntu terminal and type manticore. If the response is negative, then try to install with extra dependencies needed to execute native binaries. Run:
pip install "manticore[native]"
This should globally install Manticore.
- Check if Manticore is installed
manticore --version
It should return the installed version.
- We need a tool called
solc-selectto manage the solidity compiler. To confirm ifsolc-selectis installed, run:
solc --version
You should see a version printed in the terminal.
Version: 0.8.19+commit.7dd6d404.Linux.g++
This is the current version of solc installed on my system. If otherwise, install solc-select following these steps.
pip3 install solc-select
Check again if correctly installed. Perform step 2. This time, it should return success.
To use Manticore, we have to install the required compiler version in the contract files and tell solc-select which version to use during compilation. First, let’s check if we have versions of the compiler previously installed.
solc-select install
In my terminal, I got several available versions.
Install a specific version or simply get the latest version.
solc-select install <version>
or
solc-select latest
After installation, we have to explicitly tell solc which version we want to use for compiling our contracts.
solc-select use <version>
Example:
solc-select use 0.8.18
or simply use the latest version.
solc-select use latest
Now that we have told solc-select which version to use, let’s create a project to test if Manticore is working.
Project setup
- Create a project folder
mkdir <projectName> && cd <projectName>
- Create a virtual environment. I call my environment
env
python3 -m virtualenv env
- Navigate to the root folder, then activate the virtual environment
cd <projectRoot> && source env/bin/activate
- Inside the
envfolder, or anywhere in the project root, create aLock.solfile and the code below.
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.9;
// Uncomment this line to use console.log
// import "hardhat/console.sol";
contract Lock {
uint public unlockTime;
address payable public owner;
event Withdrawal(uint amount, uint when);
constructor(uint _unlockTime) payable {
require(
block.timestamp < _unlockTime,
"Unlock time should be in the future"
);
unlockTime = _unlockTime;
owner = payable(msg.sender);
}
function withdraw() public {
// Uncomment this line, and the import of "hardhat/console.sol", to print a log in your terminal
// console.log("Unlock time is %o and block timestamp is %o", unlockTime, block.timestamp);
require(block.timestamp >= unlockTime, "You can't withdraw yet");
require(msg.sender == owner, "You aren't the owner");
emit Withdrawal(address(this).balance, block.timestamp);
owner.transfer(address(this).balance);
}
}
The above code is the usual Lock.sol boilerplate contract. It doesn’t do much. To analyze the contract, we have to invoke Manticore. First,
navigate to the directory where the file resides, then invoke Manticore on the file.
cd <projectRoot>/env
manticore Lock.sol
When you run this command, Manticore will start to run a series of tests on the contract as shown below.
Inspect the log to see the outcome of the process. A folder will be output under the env folder containing the outcome of the analysis. Take your time to inspect the files.
Outcome
Three test cases were carried out on the contract using three different accounts tagged as:
- user_00000001
- user_00000002
- user_00000003
The summary of the analysis is kept in the "user_0000000<index>.summary" files. Let’s examine the content of thee file.
Message: RETURN
Last exception: RETURN
Last instruction at contract cb37f4304de8d1ca2df2474c6e3a00ab3e720462 offset 63
8 uint public unlockTime
3 accounts.
* owner::
Address: 0x10000
Balance: 9999926613 (*)
Storage: STORAGE_10000
* attacker::
Address: 0x20000
Balance: 9999953097 (*)
Storage: STORAGE_20000
* contract0::
Address: 0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462
Balance: 0 (*)
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[0] = 0
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
Storage: (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store STORAGE_cb37f4304de8d1ca2df2474c6e3a00ab3e720462 #x0000000000000000000000000000000000000000000000000000000000000000 SVALUE_1) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000)
Code:
b'608060405234801561001057600080fd5b50600436106100415760003560e01c'
b'8063251c1aa3146100465780633ccfd60b146100645780638da5cb5b1461006e'
b'575b600080fd5b61004e61008c565b60405161005b91906101ba565b60405180'
b'910390f35b61006c610092565b005b61007661017b565b604051610083919061'
b'0216565b60405180910390f35b60005481565b6000544210156100d757604051'
b'7f08c379a0000000000000000000000000000000000000000000000000000000'
b'0081526004016100ce9061028e565b60405180910390fd5b7fbf2ed60bd5b596'
b'5d685680c01195c9514e4382e28e3a5a2d2d5244bf59411b9347426040516101'
b'089291906102ae565b60405180910390a1600160009054906101000a900473ff'
b'ffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffff'
b'ffffffffffffffffff166108fc47908115029060405160006040518083038185'
b'8888f19350505050158015610178573d6000803e3d6000fd5b50565b60016000'
b'9054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681'
b'565b6000819050919050565b6101b4816101a1565b82525050565b6000602082'
b'0190506101cf60008301846101ab565b92915050565b600073ffffffffffffff'
b'ffffffffffffffffffffffffff82169050919050565b6000610200826101d556'
b'5b9050919050565b610210816101f5565b82525050565b600060208201905061'
b'022b6000830184610207565b92915050565b6000828252602082019050929150'
b'50565b7f596f752063616e277420776974686472617720796574000000000000'
b'00000000600082015250565b6000610278601683610231565b91506102838261'
b'0242565b602082019050919050565b6000602082019050818103600083015261'
b'02a78161026b565b9050919050565b60006040820190506102c3600083018561'
b'01ab565b6102d060208301846101ab565b939250505056fea264697066735822'
b'122023dc9151a50dafe183f4ab9c60238df87a7da647e837600b5a1235f7cfbe'
b'db5a64736f6c63430008120033'
Coverage 44% (on this state)
(*) Example solution given. Value is symbolic and may take other values
Possible Error
While invoking Manticore, you might likely encounter an error as displayed in the image below.
This error is due to a disparity in the version of protobuf on which Manticore depends to run smoothly. Manticore is compatible with the earlier version of protobuf. Most versions greater than 3.20 have conflicts. If your version is higher than v3.20, the error demands that you downgrade the version to v3.20. To downgrade protobuf, follow these steps.
-
pip3 install protobuf==3.20.* - Then set the path to be
"python".export PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION=python - Confirm if this was successful.
echo $PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION
After, you may now invoke the command again. This should work fine. The only setback is that the process will be much slower.
The complete code for this tutorial is available at Manticore.
Conclusion
In this guide, we learned :
- what Manticore is.
- Why you should use it
- Its advantage over other tools for unit testing
- Installation and set up.
- Invoking Manticore to analyze smart contracts.
- How to solve common errors.
What next?
Start analyzing your contracts using Manticore to give you more insight into your code. Please leave your comment if you encounter any difficulty while setting up the environment or share with us on Discord.
To learn how to deploy your dream project on the Celo blockchain, visit the Celo documentation
About the Author
Isaac Jesse , aka Bobelr is a smart contract/Web3 developer. He has been in the field since 2018, worked as an ambassador with several projects like Algorand and so on as a content producer. He has also contributed to Web3 projects as a developer.