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.

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.

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.

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.

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.

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 Slither is as simple as

Or outside of Truffle:

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.

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.

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.

Once again alternatively you can run it via Docker.

Use the following command to run Mythril:

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:

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 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.

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?