Comparative Tests of Popular Automated Smart Contract Audit Tools

This article is transferred from Mars Finance:

Recently, many theft cases occurred in the blockchain due to smart contract issues, but there are not many companies that do smart contract security audits around the world, not to mention the formal verification tool. Below is a summary of the formal certification platforms including SmartDec, Securify, QSP, and VaaS, each with its own advantages and disadvantages.

I have done a test on the audit platforms in terms of token contract security audit and the auction contract. The following are the comparisons of their security detection accuracy, detection capability, result analysis, user experience and other important aspects. Every blockchain enthusiast and developer is welcomed to read and draw comparison.

ERC20 Standard

ERC20 Standard: The number of return value in function transfer should be 1.

Line 52

ERC20 Standard: The function approve should emit Approval event

Line 63

ERC20 Standard: The function approveAndCall should emit Approval event

Line 69

ERC20 Standard: Message: Should check zero address in transferOwnership

Line 12

Solidity Coding Conventions

Solidity Coding Conventions: Compiler version should be fixed.

Line 1

Security Items

Safe Item: Lack of safemath library.

Integer Overflows

Integer Overflow: There may be an Integer Overflow error.

Line 126

Integer Overflow: There may be an Integer Overflow error.

Line 125

Integer Overflow: There may be an Integer Overflow error.

Line 147

Integer Overflow: There may be an Integer Overflow error.

Line 149

Integer Overflow: There may be an Integer Underflow error.

Line 82

Integer Overflow: There may be an Integer Underflow error.

Line 92

Ø Summary:

1. Accurately locating vulnerabilities, accuracy rate reaches 95%

2. Results are displayed in categories and corresponding explanations are given.

3. Risk levels are analyzed statistically. Provides detailed notification according to Ethereum vulnerabilities, and notify of possible consequences.

4. No false positives and false negatives.

Ø Audit Result Content:

l Lines: 1

Compiler version not fixed

l Lines: 17–17

Implicit visibility level (This is a false positive)

l Lines: 63–67

Using the approve function of the ERC-20 standard (Related risk not given)

l Lines: 136–139

Overpowered user (Users rely on the Setting Price function of owner, which is a legitimate logic, so this is also a false positive)

l Lines: 17–17

l Lines: 32–32

l Lines: 33–33

l Lines: 69–69

l Lines: 109–109

l Lines: 110–110

Upgrade code to Solidity 0.5.0.

Ø Summary:Smartdec didn’t find high-risk vulnerabilities such as integer overflow, audit results contain lots of false and useless information

Ø Audit Result Content:

l Line 46、47、82、90、92、119、120:

Contract fields that can be modified by any user must be inspected.

l Line 12、56、63、87、124、131、136、146:

Method arguments must be sanitized before they are used in computations.

l Line 149:

The amount of ether transferred must not be influenced by other transactions.

The execution of ether flows should be restricted to an authorized set of users.

The target of a call instruction can be manipulated by an attacker.

Ø Summary:Securify always shows as running and incomplete, results are almost all false positives. Vulnerability details have little useful information

Ø Audit Result Content

Sensitive Function Call

Sensitive Function Call: Avoid using “now”.

Line 15

Sensitive Function Call: Avoid using “now”.

Line 18

Sensitive Function Call: Avoid using “now”.

Line 31

Sensitive Function Call: There may be a denial of service risk.

Line 24

Solidity Coding Conventions

Solidity Coding Conventions: Compiler version should be fixed.

Line 1

Security Items

Safe Item: Lack of safemath library.

Integer Overflows

Integer Overflow: There may be an Integer Overflow error.

Line 22

Ø Summary:Audit results are precise, and DoS was detected, which proved the use of formal verification.

Smartdec Test Results

Ø Detailed Audit Result File:

Ø Audit Result Content

l Lines: 1–1

Compiler version not fixed

l Lines: 8–8

l Lines: 9–9

l Lines: 13–16

l Lines: 17–28

l Lines: 30–36

Implicit visibility level

l Lines: 24–24

Send instead of transfer

Ø Summary:Mentioned the risk of using ‘send’, yet missing the detailed information. Missing the obvious integer overflow risk.

Securify Test Results:

Ø Detailed Audit Result File:No Result

Ø Audit Result ContentNo Result

Ø Summary:Audit can not be completed.

Ø Detailed Audit Result File:No result.

Ø Audit Result Content:No result

Ø Summary:Not available to use even after payment.

Here is the original source of Mars Finance:

https://www.huoxing24.com/newsdetail/20181115145351595083.html

Blockchian Security · IDE · Beosin-VaaS · Formal Verification · SAS | China leading enterprise in blockchain security field

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store