How to install Mythril, a smart contract security Tool — Tutorial

Published in

HaloBlock

4 min readJun 25, 2018

Smart contracts are programs that are self-executing and stored on the Ethereum blockchain, making them distributed and trustworthy. They regulate virtual currencies transactions, such as sending or receiving Ether or ERC20-tokens.

Like all computer programs, smart contracts are written in programming languages. Among other popular contract-oriented languages, Solidity, is the primary one. With the growth of Ethereum and Solidity communities, developers are consistently improving the smart contract semantics. The most renowned “SafeMath” library, tackling uint underflow/overflow, and digit truncating issues, has been implemented into many smart contracts.

There are semantic bugs and bad practices that could be detected by automated code auditing tools, including SmartCheck, Securify, Mythril, Manticore, Porosity, and Oyente.

In this article, we will introduce how to install, deploy and use Mythril.

Mythril

Mythril uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. The detailed installation tutorial for OSX, Window and Ubuntu is available on Github.

In this article, we will show you how to install Mythril on OSX.

Step 1: Environment preparation, Homebrew, Python and Python3 (skip this step if you already installed them)

1). Install HomeBrew:

/usr/bin/ruby -e “$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)

2). Install Python:

brew install Python

And then run Python to see if it could be launched properly:

Ctrl + D to exit Python’s command line mode.

3). Install Python 3:

brew install Python3

And then run Python3 to see if it could be launched properly:

Ctrl + D to exit Python3’s command line mode.

Step 2: Install Mythril

brew update
brew upgrade
brew tap ethereum/ethereum
brew install leveldb
brew install solidity
pip3 install mythril

Step 3: Check if Mythril is running properly

myth -x your_solidity_script.sol

If you got error message like below:

ImportError: dlopen(/usr/local/lib/python3.6/site-packages/coincurve/_libsecp256k1.cpython-36m-darwin.so, 2): Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib

Try reinstall Ruby this online instruction.

When running brew reinstall gmp rvm ruby, You might encounter an error message saying rvm is not found, but that is fine.

After reinstalling Ruby, rerun:

myth -x your_solidity_script.sol

Check if you get output like the following:

Then congrats! Your Mythril is successfully loaded and you’re ready to run some basic sanity check for your smart contracts!

Configurations, Speed vs. Coverage:

The maximum recursion depth for the symbolic execution engine can be controlled with the — max-depth argument. The default value is 12. Lowering this value reduces the analysis time as well as the coverage / number of explored states. For instance:

myth -x your_solidity_script.sol — max-depth 8

Conclusion

Mythril supports Markdown and JSON format output, making its output easily integrated into your own audit reports. Please don’t forget to manually go through Mythril-generated report first to filter out false alerts, for instance, “import errors”, which could be fixed by re-adjusting your package path. Another common false alarm is Integer Overflow / Underflow, which could be triggered by any basic operation (+, -, *). Surprisingly, Mythril’s Integer Overflow / Underflow false alarms could even occur in “SafeMath” library.

Although auto-auditing tools play an important role in large volume code review, it should only be used as a preliminary examination. A professional smart contract audit report requires manual reviews from security experts who have solid knowledge for Ether ecology.

By Yuan He, Security Researcher from HaloBlock.io