An Analysis Tool for Smart Contracts
Clone or download
luongnt95 Merge pull request #341 from yxliang01/docker-fix-geth-solc-versions
Fix dockerfile installing unsupported solc and evm problem
Latest commit 6c9d382 Jul 20, 2018


An Analysis Tool for Smart Contracts

Gitter License: GPL v3 Build Status

Quick Start

A container with the dependencies set up can be found here.

To open the container, install docker and run:

docker pull luongnguyen/oyente && docker run -i -t luongnguyen/oyente

To evaluate the greeter contract inside the container, run:

cd /oyente/oyente && python -s greeter.sol

and you are done!

Note - If need the version of Oyente referred to in the paper, run the container from here

To run the web interface, execute docker run -w /oyente/web -p 3000:3000 oyente:latest ./bin/rails server

Custom Docker image build

docker build -t oyente .
docker run -it -p 3000:3000 -e "OYENTE=/oyente/oyente" oyente:latest

Open a web browser to http://localhost:3000 for the graphical interface.


Execute a python virtualenv

python -m virtualenv env
source env/bin/activate

Install Oyente via pip:

$ pip2 install oyente


The following require a Linux system to fufill. macOS instructions forthcoming.

solc evm

Full installation

Install the following dependencies


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

evm from go-ethereum

  1. or
  2. By from PPA if your using Ubuntu
$ sudo apt-get install software-properties-common
$ sudo add-apt-repository -y ppa:ethereum/ethereum
$ sudo apt-get update
$ sudo apt-get install ethereum

z3 Theorem Prover version 4.5.0.

Download the source code of version z3-4.5.0

Install z3 using Python bindings

$ python scripts/ --python
$ cd build
$ make
$ sudo make install

Requests library

pip install requests

web3 library

pip install web3

Evaluating Ethereum Contracts

#evaluate a local solidity contract
python -s <contract filename>

#evaluate a local solidity with option -a to verify assertions in the contract
python -a -s <contract filename>

#evaluate a local evm contract
python -s <contract filename> -b

#evaluate a remote contract
python -ru

And that's it! Run python --help for a list of options.


The accompanying paper explaining the bugs detected by the tool can be found here.

Miscellaneous Utilities

A collection of the utilities that were developed for the paper are in misc_utils. Use them at your own risk - they have mostly been disposable.

  1. - Contains a number of functions to get statistics from contracts.
  2. - The get_contract_code function can be used to retrieve contract source from EtherScan
  3. - Contains functions to retrieve up-to-date transaction information for a particular contract.


Note: This is an improved version of the tool used for the paper. Benchmarks are not for direct comparison.

To run the benchmarks, it is best to use the docker container as it includes the blockchain snapshot necessary. In the container, run after activating the virtualenv. Results are in results.json once the benchmark completes.

The benchmarks take a long time and a lot of RAM in any but the largest of clusters, beware.

Some analytics regarding the number of contracts tested, number of contracts analysed etc. is collected when running this benchmark.


Checkout out our contribution guide and the code structure here.