Maian

The repository contains Python implementation of Maian -- a tool for automatic detection of buggy Ethereum smart contracts of three different types: prodigal, suicidal and greedy. Maian processes contract's bytecode and tries to build a trace of transactions to find and confirm bugs. The technical aspects of the approach are described in our paper.

Evaluating Contracts

Maian analyzes smart contracts defined in a file <contract file> with:

1. Solidity source code, use -s <contract file> <main contract name>
2. Bytecode source, use -bs <contract file>
3. Bytecode compiled (i.e. the code sitting on the blockchain), use -b <contract file>

Maian checks for three types of buggy contracts:

1. Suicidal contracts (can be killed by anyone, like the Parity Wallet Library contract), use -c 0
2. Prodigal contracts (can send Ether to anyone), use -c 1
3. Greedy contracts (nobody can get out Ether), use -c 2

For instance, to check if the contract ParityWalletLibrary.sol given in Solidity source code with WalletLibrary as main contract is suicidal use

$ python maian.py -s ParityWalletLibrary.sol WalletLibrary -c 0

The output should look like this:

To get the full list of options use python maian.py -h

GUI

For GUI inclined audience, we provide a simple GUI-based Maian. Use python gui-maian.py to start it. A snapshot of one run is given below

Automated Fetching

The fetch_and_check.py utility can fetch one or more random contracts directly from a public Ethereum node and run the Maian checks on them. By default the script connects to Mainnet but other networks can be selected with the --network option. The number of contracts to scan is controlled with --count:

$ python fetch_and_check.py --network mainnet --count 5

Additional networks can be added to the tool in the future.

Contract Downloader

The repository also includes a contract_downloader.py script for gathering bytecode in bulk. It can pull data from the Etherscan API or from an RPC endpoint such as Infura. When the --verified option is used the tool stores results in contracts/EtherscanVerified.jsonl; otherwise contracts are stored in contracts/contracts.jsonl together with a metadata file describing the covered block range.

Using BigQuery

Contract bytecode can also be loaded from Google BigQuery. Create a free GCP Sandbox project and enable the BigQuery API. Install the additional dependency with pip install -r requirements-bigquery.txt. The DataGetterBigQuery class pulls data from bigquery-public-data.crypto_ethereum.contracts using the free tier (up to 1 TB/month of processed data). You can authenticate either with GOOGLE_APPLICATION_CREDENTIALS or an API key. When using an API key set the BIGQUERY_API_KEY environment variable and provide your project ID via BIGQUERY_PROJECT_ID or the constructor. Always choose a small block window to keep the queried data under the free limit.

Installation

Maian requires Python 3.8 or newer. Install the Python dependencies using:

pip install web3 z3-solver

For the optional GUI you also need PyQt5, which can be obtained with your package manager (for example sudo apt install python-pyqt5 on Debian based systems). The tool additionally relies on the following external software:

1. Go Ethereum – https://ethereum.github.io/go-ethereum/install/
2. Solidity compiler – https://docs.soliditylang.org/en/latest/installing-solidity.html
3. Z3 Theorem prover – https://github.com/Z3Prover/z3

Docker

A Dockerfile is provided to build an isolated environment with all dependencies preinstalled. From the repository root run:

docker build -t maian .

After building, the tool can be executed with:

docker run --rm maian python tool/maian.py -h

Running Maian

From the repository root you can analyze a contract using:

python tool/maian.py -s MyContract.sol MyContract -c 0

A list of all command line options is available with python tool/maian.py -h.

Random contracts can be scanned with fetch_and_check.py:

python tool/fetch_and_check.py --network mainnet --count 5

Running the tests

All tests are executed with pytest:

pytest -q

Supported Operating Systems

Maian should run smoothly on Linux (tested on Ubuntu/Mint) and macOS. Attempts to run it on Windows have failed.

Important

To reduce the number of false positives, Maian deploys the analyzed contracts (given either as Solidity or bytecode source) on a private blockchain, and confirms the found bugs by sending appropriate transactions to the contracts. Therefore, during the execution of the tool, a private Ethereum blockchain is running in the background (blocks are mined on it in the same way as on the Mainnet). Our code stops the private blockchain once Maian finishes the search, however, in some extreme cases, the blockchain keeps running. Please make sure that after the execution of the program, the private blockchain is off (i.e. top does not have geth task that corresponds to the private blockchain).

License

Maian is released under the MIT License, i.e. free for private and commercial use.