How to use Oyente, a smart contract security analyzer — Solidity Tutorial

In our previous blogs, we have learned how to create a simple valid smart contract based on Ethereum’s browser-based IDE, how to deploy a “Hello World” script in Solidity with Truffle and Ganache CLI tools, and how to review your smart contract codes with an auto-auditing tool, Mythril.

With the explosive growth of ICOs that are mostly based on Ethereum smart contracts, code review and code safety are becoming more important than ever. As the primary smart contract language, Solidity was influenced by C++, Python and JavaScript and is designed to target the Ethereum Virtual Machine (EVM). In a recent Blackhat Ethereum conference, Trail of Bits claims that “Solidity is the source of nearly all of Ethereum’s issues”.

Trail of Bits’s Blackhat Ethereum Presentation

In our own code review practices, we have noticed that Oyente, another smart contract auto-auditing tool, has helped us accurately pinpoint several legitimate bugs, rather than just raising a bunch of false alarms.

In Jan 2016, Oyente was developed by researchers from National University of Singapore. You can find the original research paper here. Oyente is a symbolic execution tool that works directly with Ethereum virtual machine (EVM) byte code without access to the high level representation (e.g., Solidity, Serpent). This mechanism is critical as the Ethereum blockchain only stores EVM byte code of contracts, not their source.

Oyente is able to detect some of the latest security flaws of Ethereum, including TheDAO bug, which caused a loss of 60 million US dollars in June 2016.

In this article, we will demo how to install, deploy and use Oyente in the Ubuntu system. The version of Ubuntu I’m using for this article is Ubuntu 64-bit, 16.04.4. We highly recommend that you run Ubuntu in VMWare, because it is much smoother than VirtualBox, and much cheaper(free) than Parallels.

Linux Working Environment Setup:

sudo apt-get install python
sudo apt install python-pip
pip install virtualenv
sudo apt install vim

Execute a Python Virtualesbinv:

python -m virtualenv envsp
source env/bin/activate

Install Oyente:

pip2 install oyente

You might encounter the following error:

It’s due to an improper python3 version. Try to solve this problem by doing the following:

sudo apt-get install python3-venv
Python3 -m venv venv
pip install web3

Then, check the python3 version, and have your Ubuntu set up with your python3 version’s Python.h header file., by running:

python3 — version

And then run:

sudo apt-get install python3.6-dev

Note that you need to replace the “3.6” with your Python3 version number.

Now try Oyente installation again:

pip2 install oyente

Install Solidity:

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

Install Ethereum Virtual Machine(EVM):

sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum

Install Z3:

This step might take up to 30 minutes. Grab yourself a coffee and enjoy a video.

python scripts/mk_make.py — python
cd build
make
sudo make install

🙌Hurray!! You’ve got Oyente installed!! Now let’s evaluate a smart contract with it.

python oyente.py -s <contract filename>

Check if your output is something like the above. If yes, Oyente is working completely fine with your Ubuntu! You’re good to go.

Conclusion

Here is my suggestion for using auto-auditing tools: manually review first, and then use a tool for uncovering unnoticed issues, instead of the other way around. It’s helpful to maintain a good workflow, so that results generated by the auto tools don’t mislead your own judgment.

Also, it is worth mentioning that compared to other smart contract audit-tools, such as Mythril, Oyente delivers better results. We conclude this by carefully analyzing and comparing our manual review reports and auto tools’ reports in several Uint underflow and overflow errors. Although Mythril generates more alerts, the majority of them are obvious false alarms. We believe that Mythril doesn’t take the code context into consideration as much as Oyente does.

In conclusion, developers and crypto bug diggers should really consider Oyente if you want to secure your smart contracts.

By Yuan He, Security Researcher from HaloBlock.io