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. Generic detectors cannot infer every intended business rule; custom analyses and explicit properties can nevertheless detect some 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. Property checking can be automated, for example with Solidity’s SMTChecker. The hard work includes specifying intended behavior and understanding modeling limits; proofs need to be maintained as the code or assumptions change.

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 study discussed in this 2020 article, 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.

That result is specific to the study’s dataset and tool versions. It is not a current benchmark or a reason to skip property tests, manual review or other applicable analyses.

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:

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

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

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

Use the compiler version and settings required by your project. solc-select can install and select exact versions; do not rely on the old solidity@6 Homebrew example. With a supported framework, let Slither use that project’s normal build.

How to use Slither

Current Slither requires Python 3.10 or newer. Follow its installation instructions and use an isolated tool environment or the documented container. Pin the tool version in CI so changes to findings can be reviewed.

Running the Slither verification

Running Slither is as simple as

Terminal / configuration
$ slither . # inside a supported Hardhat or Foundry project

Or outside of Truffle:

Terminal / configuration
$ slither contracts/MyContract.sol # flattened contract file

Slither documents direct integrations for Hardhat and Foundry project builds with slither .. Use a supported combination of analyzer and framework versions, and compile the project successfully first. The old Buidler-to-Truffle conversion workaround is unnecessary and relies on retired tooling.

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.

The product description, $249 price and trial above are historical and were not verified as a current offer. Slither’s official repository also documents a maintained GitHub Action for CI.

How to use Mythril

Installation on MacOS:

The Mythril repository documents Python 3.7–3.10 for its PyPI installation. This is a different compatibility range from current Slither; use separate pinned environments or the documented container and check support for the target EVM/compiler.

Terminal / configuration
$ brew install leveldb
$ pip3 install mythril

Installation on Ubuntu:

Terminal / configuration
$ 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:

Terminal / configuration
$ 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:

solidity
Open in Remix 
$ 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:

The prices, quotas and CircleCI product setup above are a historical description. The website was reachable during review, but current service availability and plan terms were not verified; they should not be used for a purchasing decision.

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. Tools can already check some semantic properties when those properties are specified; their coverage still depends on the model, search limits and intended behavior.

Automate Raptor