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 Content：No 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
