Understanding the World of Automated Smart Contract Analyzers

What are the best tools today and how can you use them?

Automated Security Morpheus

As we all know, it's very difficult writing a complex, yet fully secure smart contract. Without the proper methods, chances are you will have many security issues. Automated security testing tools already exist and can be a great help. One of the main challenges for these tools is to maximize finding all vulnerabilities, while minimizing false positives.

A false positive is a detected vulnerability that in reality is actually not a problem. Obviously, we want to avoid those as much as possible. If a tools finds every single vulnerability in a contract, but shows you 20,000 different vulnerabilities of which 19,950 are false positives, that's not of much value. Nobody has the time to go through that many issues to decide if it's a false positive or not. So the tools always have to find a good trade-off.

FAQ

Can I use these tools instead of an audit? No! They are no audit replacement. Not even close. For any meaningful contracts, you will still need to get a professional audit. The tools can only find a specific subset of vulnerabilities. They have no capacity to find any semantic bugs.

Alternatively, you can also use formal verifications. Those are mathematical proofs showing the contract behaves given a specific specification. For example the ETH2.0 deposit contracts have been verified this way using the KEVM framework. This is also not a full audit replacement most of the times, but gives you much more security than the analyzer tools. They are however only feasible for a small smart contract that doesn't change very often as the procedure is quite complex and anything but automated.

Should I get only an audit and not use these tools? That depends, but most times I would recommend running the tools. Just look at this very recent hack of Lien Finance from one month ago here. One very interesting takeway from them was:

'Lien smart contracts were audited not by one firm, but by two firms that are well known and trusted in the industry. We made sure that each time we made changes to the audited code, the changes were verified by the auditors before they were deployed. The code that has been deployed to the Ethereum mainnet is the same code that has been audited and no changes or additions have been made since they have been audited. Code audits are an important part of assessing the validity and security of the code. However, audits do not eliminate risks completely, as this incident has reminded us. We have not taken this lightly and will be remediating and improving our internal control procedures over code development.'

So as you can see, an audit is anything but a fail-safe. You need to ensure best coding practices and minimal security issues during the whole process regardless. And in that sense these tools can be of great value.

Study: Empirical Review of Automated Analysis Tools

In a recent study from beginning of this year, the authors examined existing automatic smart contract analyzers. After looking at 35 different tools, they concluded a list of 9 tools to be examined:

Now they went and tested all tools with a set of 69 smart contracts with all kinds of injected vulnerabilities that in theory could be found by the tools. You can find the used contracts here. Most notably they include  vulnerabilities for

  • Reentrancy: Reentrant function calls make a contract to behave in an unexpected way
  • Access Control: Failure to use function modifiers or use of tx.origin
  • Arithmetic: Integer over/underflows
  • Unchecked Low Level Calls: call(), callcode(), delegatecall() or send() fails and it is not checked
  • Denial of Service: The contract is overwhelmed with time-consuming computations
  • Bad Randomness: Malicious miner biases the outcome
  • Front Running: Two dependent transactions that invoke the same contract are included in one block
  • Time Manipulation: The timestamp of the block is manipulated by the miner
  • Short Addresses: EVM itself accepts incorrectly padded arguments


The conclusion was that even when combining all 9 tools, only 42% of all vulnerabilities could be detected. So this shows us that you shouldn't rely too much on these tools and that they also still have a long way to go. Nevertheless, they are anything but useless. In particular reentrancy bugs were well detected and just earlier this year the cause for a 25 million $ hack.


Study Results

The other takeaway from the study was:


'The combination of Mythril and Slither allows detecting a total of 42/115 (37%) vulnerabilities, which is the best trade-off between accuracy and execution costs.'

So you don't need to run 9 different tools for now. Combining Mythril and Slither will give you almost the same amount of vulnerabilities with less false positives. Let's see how to use them.

Installing Native Solc

Unless you are going to use the Docker versions of Slither and Mythril, you will need a native solc installation for both Slither and Mythril on your system. You can find binaries and instructions here for Ubuntu, Mac and Windows.

If you're on Mac, the easiest way is to use Homebrew:

$ brew update
$ brew upgrade
$ brew tap ethereum/ethereum
$ brew install solidity

If you're on Ubuntu, the easiest way is to use the PPA:

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

Make sure you have the correct solc version installed that you need for your contracts. For example the latest 0.6 version can be installed via brew install solidity@6. If you want to install it manually, all binaries are available in the releases.

How to use Slither

Now lets first use Slither. It further requires Python 3.6+. brew install python on Mac is all you need or do a manual installation: https://www.python.org/downloads/.

To install Slither, you can run pip3 install slither-analyzer. Alternatively, run it via Docker.

Running the Slither verification

Running Slither is as simple as

$ slither . # inside Truffle environment

Or outside of Truffle:

$ slither contracts/MyContract.sol # flattened contract file

In case you have a Buidler project, just install Truffle and run truffle init followed by truffle compile. This should give you the ability to run the tools.

Usage of Slither inside VS Code

You can install the Slither VS Code Extension to run the tool directly inside VS Code. It will show you all affected functions inline and vulnerabilities sorted by how critical they are.

Slither VS Code

Premium Slither (Crytic) + Continuous Integration

You can integrate Slither into your continuous integration. If you haven't setup one yet, I highly recommend this. You can follow the instructions from my previous blog post here. The best way to integrate Slither is using the premium version called Crytic: https://crytic.io/ made by Trail of Bits.The setup works via Github and is very simple. Analysis happens automatically for each pull request. Pricing starts at $249/month with the first three months for free.

How to use Mythril

Installation on MacOS:

$ brew install leveldb
$ pip3 install mythril

Installation on Ubuntu:

$ sudo apt install libssl-dev python3-dev python3-pip
$ pip3 install mythril

Once again alternatively you can run it via Docker.

Running the Mythril verification

Use the following command to run Mythril:

$ myth analyze MyContract.sol

Truffle and Buidler projects are not supported, but you can use truffle-flattener to create a single Solidity file. There's currently an open issue for it due to the SPDX license strings, but you can avoid it using the command:

$ truffle-flattener ./contracts/MyContract.sol \
    | awk '/SPDX-License-Identifier/&&c++>0 {next} 1'  \
    | awk '/pragma experimental ABIEncoderV2;/&&c++>0 {next} 1' \
    > ./MyContract.full.sol

Premium Mythril (MythX) + Continuous Integration

Just like Slither, you can also integrate Mythril into your continuous integration. The best way to integrate Mythril is using the premium version called MythX: https://mythx.io/ made by Consensys. The setup with CircleCI is explained here. MythX also supports Truffle out of the box and has very convenient cloud analysis supported.

You will need to pay for scans with MythX. Either 10 USD for 3 scans or a monthly plan ranging from 50$ to 250$ monthly including 500 and 10,000 scans.

After a successful scan, you can access the results in the cloud. You will get a overview of all found vulnerabilities:

MythX Dashboard

Usage of MythX inside VS Code

MythX also has VS Code support. You can start an analysis directly inside the IDE using the extension here. Make sure you set a working API key.

The future of automated testing

As of right now the tools still have a long way to go. That doesn't mean they are useless, but they will certainly become more and more useful in the future. Maybe one day they will even be able to detect semantic errors?

Automate Raptor

Markus Waas

Solidity Developer

More great blog posts from Markus Waas

© 2024 Solidity Dev Studio. All rights reserved.

This website is powered by Scrivito, the next generation React CMS.