Top 3 smart contract audit tools

Smart contract security analysis tools

Previously, we wrote about deals in the digital age, describing in essence the operation and security of smart contracts. Today, as a follow-up to the topic of smart contract security, we share with you our review of the most common smart contract auditing tools.

Currently, our goal is to compare the most popular software tools for smart contract security analysis. For this purpose, we have used smart contracts deemed highly likely to be secure (hereafter, for simplicity, known-to-be-secure or just secure smart contracts) as well as known-to-be-vulnerable, or just vulnerable smart contracts. In total, we analysed 20 DeFi smart contracts from the Ethereum blockchain network, written in the Solidity programming language.

As secure smart contracts, we selected only those contracts that had professional security audit reports developed by reputable auditors. Using the resource etherscan.io, we found 10 smart contracts that had one or more successful transactions, as well as fixed vulnerabilities identified in professional independent audit reports. Below is a list of these known-to-be-secure smart contracts.

Name of smart contract	Address of smart contract
BAToken	0x0D8775F648430679A709E98d2b0Cb6250d2887EF
HumanStandardToken	0x0F4CA92660Efad97a9a70CB0fe969c755439772C
HBToken	0x6f259637dcD74C767781E37Bc6133cd6A68aa161
NPXSToken	0xA15C7Ebe1f07CaF6bFF097D8a589fb8AC49Ae5B3
FunctionXToken	0x8c15Ef5b4B21951d50E53E4fbdA8298FFAD25057
BlockWRKICO	0x0407B4c4eAEd35CE3C5B852bDFA1640B09EeEDF4
ThePoolz	0x000BaB4F6b5560d7942AC88cf0233b6028B5B465
EternalStorageProxy	0x69c707d975e8d883920003CC357E556a4732CD03
Layerx	0xfe56E974C1C85e9351325fb2D62963A022Ad624F
sHakka	0xd9958826Bce875A75cc1789D5929459E6ff15040

Also, to determine the effectiveness of the auditing tools, we selected smart contracts with commonly known verified vulnerabilities. These smart contracts were specifically designed by crypto-enthusiasts for testing, training, etc.

A list of known-to-be-vulnerable smart contracts:

Type of vulnerability	Name of smart contract
Access control	Unprotected0
Arithmetic	OverflowSingleTx
Bad randomness	Lottery
Denial of service	DosSimple
Front running	FindThisHash
Reentrancy	ReentrancySimple
Short addresses	ShortAddressExample
Time manipulation	Roulette
Unchecked low-level calls	Lotto
Other	NaiveReceiver

To audit smart contracts and analyse the results, we have selected three of the most common and relevant open source code tools, namely:

• Mythril
• Securify
• Slither

We installed them on an Oracle VirtualBox virtual machine running Linux Ubuntu 21.10. Also, we installed the Docker platform, Python 3 programming languages, and a number of Python libraries to make the tools work properly. We used exclusively console versions of the auditing tools.

The essence of our study is to determine the effectiveness of tool-based smart contract auditing by having each tool analyse secure smart contracts and vulnerable smart contracts. For secure smart contracts, any vulnerabilities found by the tools and not reported in the independent audit reports would be considered false positives (Type I error). For vulnerable smart contracts, unreported known vulnerabilities would be considered false negatives (Type II error).

Additionally, we tested whether the tools could find vulnerabilities that were fixed in secure smart contracts based on independent audit reports. We were almost certain that the vulnerabilities would not be found, but such a check would improve the objectivity of the analysis.

We used the following characteristics to assess the overall performance of the tools:

• The number of false-positive vulnerabilities.
• The number of false-negative (missed) vulnerabilities.
• Audit runtime.
• Ability to find ways to optimise gas consumption.
• Additional functionality and digitalisation of obtained results.

Below we consider each of the auditing tools in more detail.

What is Mythril, and how it works

Mythril is one of the most common tools for bytecode auditing of Ethereum virtual machines. Smart contacts are tested in a concolic method, which includes symbolic execution, SMT calculation, and taint analysis. The Mythril tool can be used for discovering vulnerabilities such as numeric overflow, owner overwrite, function re-run, etc. Below is an example of a Mythril report.

==== Unprotected Selfdestruct ====
SWC ID: 106
Severity: High
Contract: KillBilly
Function name: commencekilling()
PC address: 354
Estimated Gas Usage: 574 - 999
The contract can be killed by anyone.
Anyone can kill this contract and withdraw its balance to an arbitrary address.
--------------------
In file: killbilly.sol:22

selfdestruct(msg.sender)

In addition to the Ethereum network, the tool is able to analyse smart contracts of networks that support EVMs. These include Hedera, Quorum, Vechain, Roostock, Tron and others.

To run the analysis, you should execute the command “myth analyse ExampleName.sol”. You can also specify the maximum number of test transactions to be performed and the maximum duration of the analysis in seconds. To do so, you need to add the “-t” and “–execution-timeout” parameters to the start command, respectively.

The tool provides a fairly detailed and user-friendly audit report. This makes it easy to find the highlighted part of the code in the original file and manually check for potential vulnerabilities. Mythril cannot find ways to save gas.

What is Securify, and how it works

Securify is a smart contract security auditing tool developed by Ethereum Foundation and ChainSecurity in 2017. More than 22,000 Ethereum smart contracts have been scanned using Securify since its launch. This has helped their developers fix a large number of vulnerabilities with various risk levels.

Securify statically analyzes the bytecode of Ethereum virtual machines and obtains all the information about the algorithm and data flow in it. This process is fully automated by using Souffle, a programming language that was created for static analysis of Oracle and other software. The findings are then checked to find the vulnerabilities and provide recommendations on how to fix them.

The main steps of the Securify tool are depicted below:

The analysis proceeds in three main steps:

1. Parsing the EVM bytecode and decompiling it into a form suitable for analysis.
2. Identifying semantic facts about the smart contract.
3. Combining patterns and rules to identify vulnerabilities.

To start auditing a locally stored smart contract, the following command must be executed:

securify <contract_source>.sol [–use-patterns Pattern1]

It is also possible to scan smart contracts on the Ethereum network:

securify <contract_address> –from-blockchain [–key <key-file>]

After executing one of these commands, the following report can be generated:

Severity:    CRITICAL
Pattern:     Transaction Order Affects Execution of Ether Transfer
Description: Ether transfers whose execution can be manipulated by
             other transactions must be inspected for unintended
             behavior.
Type:        Violation
Contract:    Layerx
Line:        383
Source: 
>         
>         if(rwds.eth > 0) { msg.sender.transfer(rwds.eth); }
>                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>     }


Severity:    HIGH
Pattern:     Unhandled Exception
Description: The return value of statements that may return error
             values must be explicitly checked.
Type:        Warning
Contract:    Layerx
Line:        270
Source: 
>         require(payment > 0, 'Payment must be greater than 0.');
>         require(UNILAYER.balanceOf(msg.sender) >= payment, 'Holder does not have enough tokens.');
>                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>         require(UNILAYER.allowance(msg.sender, address(this)) >= payment, 'Call Approve function firstly.');

The Securify report provides information on vulnerability risk levels, the patterns that were found, vulnerability message types, smart contract name, and the fragment of potentially vulnerable code.

The Securify tool gives good results in a relatively short time. It has 37 templates for different types of vulnerabilities in its arsenal, which makes this tool stand out from its competitors. Securify can detect simple logic errors, but it cannot find ways to save and optimise gas costs.

What is Slither, and how it works

Slither is a tool for static code analysis of smart contracts. In addition to automatically finding vulnerabilities, Slither is capable of finding code optimization opportunities and visualising the execution algorithm, helping auditors to better and faster understand how a smart contract is structured. The tool can work with frameworks such as Truffle, Hardhat, Embark and Dapp without additional configuration.

Slither’s working algorithm:

1. Representing the source code as an abstract syntax tree using the Solidity compiler.
2. Constructing a diagram of element inheritance, a control flow diagram, and a list of all expressions in the smart contract.
3. Illustrating the source  code in an internal representative language of Slither, which simplifies the analysis.
4. All the information that was obtained is passed to the vulnerability search modules.
5. Auditing and reporting.

A schematic representation of the Slither algorithm is shown below:

The tool can be installed using Pypi, downloaded from the Github repository, or as part of a Docker image called eth-security-toolbox. To start the audit, run the following command: slither examplename.sol.

Example of a Slither report:

C.increment() (etheno-examples/ConstantinopleGasUsage/constantinople.sol#7-11) ignores return value by address(this).call(abi.encodeWithSignature(setStored(int256),newValue)) (etheno-examples/ConstantinopleGasUsage/constantinople.sol#10)
Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#unchecked-low-level-calls

Pragma version^0.5.4 (etheno-examples/ConstantinopleGasUsage/constantinople.sol#1) allows old versions
solc-0.5.5 is known to contain severe issues (https://solidity.readthedocs.io/en/latest/bugs.html)Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#incorrect-versions-of-solidity

Low level call in C.increment() (etheno-examples/ConstantinopleGasUsage/constantinople.sol#7-11):
	- address(this).call(abi.encodeWithSignature(setStored(int256),newValue)) (etheno-examples/ConstantinopleGasUsage/constantinople.sol#10)
Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#low-level-calls

setStored(int256) should be declared external:
	- C.setStored(int256) (etheno-examples/ConstantinopleGasUsage/constantinople.sol#4-6)
increment() should be declared external:
	- C.increment() (etheno-examples/ConstantinopleGasUsage/constantinople.sol#7-11)
echidna_() should be declared external:
	- C.echidna_() (etheno-examples/ConstantinopleGasUsage/constantinople.sol#12-14)
Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#public-function-that-could-be-declared-external

The report consists of a detailed description of the vulnerabilities that were found, lines in the code where the vulnerable functions are located, and links to external resources with recommendations. The level of vulnerability risk can be identified by the colour: red is critical and high, yellow is medium, and green is low.

Overall, the Slither application proved to be easy to use, with a large set of supplementary tools in addition to code security auditing. It allows describing briefly all the available smart contract functions, which greatly simplifies and speeds up the manual search for vulnerabilities and analysis of automatic audit results. In addition, the tool provides recommendations that can improve the overall security of a smart contract, such as limiting the pragma version, removing unused variables from the code, and others. Slither also can search for ways to optimise code and save gas, which is quite rare among similar tools. The results of the tool are satisfactory, and the report is informative and understandable.

Comparison of results

Audit results of secure smart contracts

The name of the secure smart contract	Number of false positives			Audit execution time (seconds)
	Mythril	Securify	Slither	Mythril	Securify	Slither
BAToken	2	4	3	5	112	2
BlockWRKICO	3	0	2	27	9	2
EternalStorageProxy	0	3	2	1	30	1
FunctionXToken	2	2	2	5	2	1
HBToken	0	5	1	16	118	1
LayerX	2	0	3	2	2	2
NPXSToken	2	10	1	3	316	3
sHakka	0	0	1	2	2	2
ThePoolz	1	1	3	5	5	1
HumanStandardToken	1	0	2	2	3	2
Total	13	25	20	68	599	17

As a result of the audit, the Mythril tool reported from 1 to 3 false positives in 7 out of 10 secure smart contracts, Securify reported from 1 to 10 false positives in 6 out of 10 secure smart contracts. All discovered vulnerabilities had “Warning” and “Informational” risk levels, which are regarded as low risk level.

Slither made 1 to 3 false positives in all 10 secure smart contracts. In addition, some of the alarms were assigned medium and high risk levels.

Results of the audit of vulnerable smart contracts.

The name of the vulnerable smart contract	Known vulnerabilities discovered?			Audit execution time (seconds)
	Mythril	Securify	Slither	Mythril	Securify	Slither
unprotected0	no	yes	no	3	2	2
overflow_single_tx	yes	no	no	9	9	2
lottery	no	yes	yes	3	30	3
dos_simple	yes	no	no	3	2	2
FindThisHash	yes	yes	yes	19	2	1
reentrancy_simple	yes	yes	yes	2	3	2
short_address_exampe	no	no	no	2	2	1
roulette	yes	yes	yes	25	2	2
lotto	yes	yes	yes	2	31	2
NaiveReceiver	no	no	no	10	9	2
Total	6	6	5	78	92	19

Among vulnerable smart contracts, Mythril and Securify correctly identified problems in 6 out of 10 DeFi smart contracts, and Slither in 5 out of 10.

Securify labelled most of the errors as Violation, which can be interpreted as the tool’s high confidence in correctly identifying security vulnerabilities. In addition, Securify found issues with the lack of validation for user-controlled data and the use of low-level calls, which are not in line with the best practices for secure development in the Solidity programming language.

In vulnerable smart contracts, all the tools also found vulnerabilities that were not declared by the developers:

The name of the vulnerable smart contract	Number of not declared vulnerabilities found
	Mythril	Securify	Slither
unprotected0	0	0	4
overflow_single_tx	0	6	1
lottery	1	1	1
dos_simple	0	0	1
FindThisHash	0	1	1
reentrancy_simple	0	3	1
short_address_exampe	1	0	1
roulette	0	1	1
lotto	0	5	2
NaiveReceiver	1	4	3
Total	3	21	16

When evaluating these tools, we did not take into account these vulnerabilities, as this would require their additional validation (whether they are false positives), and this was beyond the scope of our study.

Conclusions

We have reviewed three of the most popular tools for automated search for vulnerabilities in smart contracts, namely Mythril, Securify, and Slither.

The tools were studied by analysing ten known-to-be-secure smart contracts, verified by independent auditors, and ten known-to-be-vulnerable smart contracts designed for training, testing, etc.

To understand the overall set of vulnerabilities, here is a chart of the total number of vulnerabilities found in secure and vulnerable smart contracts based on the results of all three tools.

Our analysis determined the accuracy, speed, completeness of results, and additional features of the most popular smart contract auditing tools.

We considered the relative weight of false positives (Type I errors) in the overall assessment to be lower than the weight of false negatives (Type II errors) because the former are easier to verify than the latter.

The results are presented in the table below on a five-point scale, with higher scores indicating better tool properties.

	Mythril	Securify	Slither
False positives	4.5	4	3
False negatives	2	2	1.5
Analysis speed	4.5	4	5
Details and functionality	4	4	4.5
Overall score	3.75	3.5	3.5

The most important finding of our research is that today’s popular smart contract auditing tools are quite weak at finding vulnerabilities in code so far, missing up to half of the simple, typical vulnerabilities, not to mention the more complex ones.

The analysed smart contract analysis tools produce different types of erroneous results and find different problems in the same set of smart contracts. The basic and the additional functionality of these tools varies significantly.

As expected, none of the tools found the vulnerabilities in secure smart contracts that were fixed by professional, independent audit reports. 

Thus, at this point, it cannot be claimed that any one of the above-mentioned tools is significantly better than the others for practical smart contract security analysis. Several general-purpose and highly specialised tools must be used simultaneously to improve the effectiveness of the analysis.

At the same time, the high number of erroneous results indicates that using a limited number of tools with cross-verification between their reports is not sufficient to perform a reliable smart contract security audit. Instead, you need to manually verify the automatic results through a professional, independent smart contract audit, especially if your smart contract will manage large sums of money, or if the trust of your investors depends on a high-quality security audit report.

Use our free online smart contract security analyzer to get a quick insight into the results of automated tools.

If you have additional questions about Web3 and blockchain security, please contact us for a free consultation.

Subscribe to our Telegram channel so you do not miss new articles on our blog.