As the blockchain 2.0 era centered on smart contracts (Smart Contracts) and blockchain applications (DApps) has gradually become mainstream, the security of smart contracts and blockchain applications has increasingly become the focus of attention in the industry.
In particular, after experiencing incidents such as THE DAO and the theft of Binance, how to verify and guarantee the security of smart contracts and blockchain applications has become an urgent pain point in the current blockchain industry.
The author has made simple statistics. From September 2017 to September 2018, the related vulnerabilities of smart contracts and blockchain applications showed a pattern of frequent outbreaks, and the consequences were far-reaching. Not only did it directly cause a huge amount of money loss; from the perspective of long-term development, it also affected the sustainable development of the emerging technology of blockchain in the future.
In addition, although the potential vulnerabilities of current smart contracts and blockchain applications have not been properly resolved, the status quo is that the number of smart contracts and blockchain applications is still increasing rapidly at an average growth rate of tens of thousands every day.
It is not difficult to see that the growth rate and security of smart contracts and blockchain applications are coexisting in an unhealthy relationship. If we use the analogy of supply and demand (growth rate is "supply"; security is "demand"), the current general status of smart contracts and blockchain applications is the state of "supply exceeds demand".
Based on this, how to ensure the security of massive smart contracts and blockchain applications has become a core issue for forward-looking enterprises and individuals in the blockchain industry. In fact, there are currently special methods in the industry to overcome this pain point, such as feature code matching, automatic auditing based on symbolic execution and symbolic abstraction, and automatic auditing based on formal verification. Among them, after extensive exploration and practice in the industry, "automatic audit based on formal verification" has become a relatively mature and mainstream method in the industry.
Therefore, the author specifically focuses on "formal verification", selects two major formal verification tools (VaaS & Mythril) in the current industry, and conducts a simple test comparison. In particular, the version of the Mythril tool used for testing is "0.21.12".
secondary title
Introduction to VaaS & Mythril Tools
01. Introduction to VaaS tools
The VaaS tool is an automatic formal verification tool independently developed by Beosin Chengdu Lianan using its own intellectual property rights. It can provide "military-level" formal verification services for smart contracts and blockchain applications, and can accurately locate risky codes The position and the cause of the risk are pointed out, and the conventional security loopholes, security attributes and functional correctness of the smart contract are effectively detected, with an accuracy of over 95%.
02. Introduction to Mythril Tool
secondary title
Test case composition
The contract test case consists of 260 token contracts and 20 business contracts.
Token contracts include Top200 token contracts and 60 typical token contracts for auditing, covering functions such as ICO, lock-up, minting and burning.
secondary title
Overview of test results
VaaS tools can detect all contract test cases of tokens and business classes; however, Mythril tools can only detect token contracts, but not business contracts. Therefore, it should be noted that this overview of test results is only a comparative analysis of the list of token contracts.
VaaS tools have a total of 28 vulnerability checks; but Mythril tool has only 9 vulnerability checks compared to VaaS tools. Therefore, the detection items of VaaS tools are far more than those of Mythril tools. The specific detection items are compared as follows:
Comparison of VaaS & Mythril detection items
01. Test results for the same test items
For the selected 260 token test cases, the Mythril tool can run 184 contract results within 15 minutes, and 76 have no detection results; while the VaaS tool can run all the results. Take the 184 results that both the Mythril tool and the VaaS tool can run for comparison, and the results are as follows.
Hit Rate & False Positive Rate
Through the comparison of detection results, compared with the same detection items, the detection ability of VaaS tools is much higher than that of Mythril tools. According to calculations, the detection accuracy of the VaaS tool is 96.9%; the detection accuracy of the Mythril tool is 36.6%; the false positive rate of the VaaS tool is 15.3%; the false positive rate of the Mythril tool is 48.5%. See the figure below for details.
It should be noted that the calculation formulas of hit rate and false alarm rate are:
Hit rate = number of hits/total number of questions
False positive rate = number of false positives/(number of false positives + number of hits)
According to the author's statistics, the detection items performed by both the VaaS tool and the Mythril tool totaled 655 questions:
The VaaS tool detected a total of 635 problems, with a hit rate of 96.9%; a total of 115 false positives, with a false positive rate of 15.3%
The Mythril tool detected a total of 240 problems, with a hit rate of 36.6%; a total of 226 false positives, with a false positive rate of 48.5%. Among them, the Mythril tool re-entrancy attack and denial of service false alarm rate are relatively high, accounting for 93.3% of the total.
The total value of detection is compared in the following table:
Test time limit
The average test time of Mythril tool is 226.2s; while the average test time of VaaS tool is 164.4s. It shows that the operating efficiency of VaaS tools is better than that of Mythril tools.
02. The detection results of specific detection items for VaaS tools
See the table below for details:
secondary title
Case presentation
01. The case of the same detection items
Re Entrancy
case:
interface TEST {
function test123() external view returns (uint256);
function getBlocknumber() external view returns (uint256);
}
contract test2 {
function testCalling(address _testAdddress) public {
TEST t = TEST(_testAdddress);
t.test123();//mythril false positive
}
function testFormal(address _testAdddress) public view returns(uint256 time){
TEST t = TEST(_testAdddress);
t.getBlocknumber();//mythril false positive
return time;
}
}
contract Reentrancy {
mapping(address => uint256) public balances;
event WithdrawFunds(address _to,uint256 _value);
function depositFunds() public payable {
balances[msg.sender] += msg.value;
}
function showbalance() public view returns (uint256 ){
return address(this).balance;
}
function withdrawFunds (uint256 _weiToWithdraw) public {
require(balances[msg.sender] >= _weiToWithdraw);
require(msg.sender.call.value(_weiToWithdraw)());
balances[msg.sender] -= _weiToWithdraw;//mythril obvious false positive
emit WithdrawFunds(msg.sender,_weiToWithdraw);
}
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, the VaaS tool reported the location of the reentrancy attack; while the Mythril tool issued an alarm for the external call, there were a total of 4 alarms, 2 of which were normal external calls, and the other was an obvious false alarm , with a high false positive rate.
TXOriginAuthentication (tx.origin usage error)
case:
contract TxUserWallet {
address owner;
constructor() public {
owner = msg.sender;
}
function transferTo(address dest, uint amount) public {
require(tx.origin == owner);
dest.transfer(amount);
}
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, both the VaaS tool and the Mythril tool can detect and alarm the tx.origin keyword.
Invoke Low Level Calls (call call, delegatecall call, suicide function call)
case:
contract Delegatecall{
uint public q;
bool public b;
address addr = 0xde6a66562c299052b1cfd24abc1dc639d429e1d6;
function Delegatecall() public payable {
}
function call1() public returns(bool) {
b = addr.delegatecall
(bytes4(keccak256("fun(uint256,uint256)")),2,3);
return b;
}
function call2(address add) public returns(bool){
b=add.delegatecall
(bytes4(keccak256("fun(uint256,uint256)")),2,3);
return b;
}
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, there were two delegetacall calls in the case, while the Mythril tool only reported once, so there is a risk of underreporting.
BlockMembers Manipulation (block parameter dependency)
case:
function createTokens() payable external {
if (isFinalized) throw;
if (block.number < fundingStartBlock) throw;
if (block.number > fundingEndBlock) throw;
if (msg.value == 0) throw;
uint256 tokens = safeMult(msg.value, tokenExchangeRate);
uint256 checkedSupply = safeAdd(totalSupply, tokens);
if (tokenCreationCap < checkedSupply) throw;
totalSupply = checkedSupply;
balances[msg.sender] += tokens;
CreateBAT(msg.sender, tokens);
}
function finalize() external {
if (isFinalized) throw;
if (msg.sender != ethFundDeposit) throw;
if(totalSupply < tokenCreationMin) throw;
if(block.number <= fundingEndBlock && totalSupply != tokenCreationCap) throw;
// move to operational
isFinalized = true;
if(!ethFundDeposit.send(this.balance)) throw;
}
function refund() external {
if(isFinalized) throw;
if (block.number <= fundingEndBlock) throw;
if(totalSupply >= tokenCreationMin) throw;
if(msg.sender == batFundDeposit) throw;
uint256 batVal = balances[msg.sender];
if (batVal == 0) throw;
balances[msg.sender] = 0;
totalSupply = safeSubtract(totalSupply, batVal);
uint256 ethVal = batVal / tokenExchangeRate;
LogRefund(msg.sender, ethVal);
if (!msg.sender.send(ethVal)) throw;
}
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, both the VaaS tool and the Mythril tool can detect block parameter dependencies; however, the Mythril tool has the risk of false positives.
Denial of service
case:
contract Auction {
address public highestBidder = 0x0;
uint256 public highestBid;
function Auction(uint256 _highestBid) {
require(_highestBid > 0);
highestBid = _highestBid;
highestBidder = msg.sender;
}
function bid() payable {
require(msg.value > highestBid);
highestBidder.transfer(highestBid);
highestBidder = msg.sender;
highestBid = msg.value;
}
function auction_end() {
}
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, both VaaS tools and Mythril tools can perform risk detection for denial of service. However, in this case, the highestBidder may have maliciously attacked the contract, resulting in the constant failure of the transfer, resulting in the contract’s refusal to accept the service. In this case, the VaaS tool can detect the risk of denial of service, but the Mythril tool did not detect it.
Unchecked Call Or Send Return Values (call and send return value detection)
case:
if (lastTimeOfNewCredit + TWELVE_HOURS < block.timestamp) {
msg.sender.send(amount);
creditorAddresses[creditorAddresses.length - 1].send(profitFromCrash);
corruptElite.send(this.balance);
...
return true;
}
else {
msg.sender.send(amount);
return false;
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, both the VaaS tool and the Mythril tool can detect the return value of unchecked call calls; however, the Mythril tool has the risk of false positives.
Integer Overflow
Case 1:
function distributeBTR(address[] addresses) onlyOwner {
for (uint i = 0; i < addresses.length; i++) {
balances[owner] -= 2000 * 10**8;
alances[addresses[i]] += 2000 * 10**8;
Transfer(owner, addresses[i], 2000 * 10**8);
}
}
▷ According to the analysis of the author, the value of balances[owner] is not checked in the above case, which may cause underflow, but Mythrill tool will not report an error, which means that Mythrill tool will not check the constant operation.
Case 2:
contract A {
uint c;
function add(uint8 a,uint8 b){
uint8 sum = a+b;
c=sum;
}
}
VaaS tool test results:
Mythril tool test results:
▷ According to the author’s analysis, the Mythrill tool’s overflow detection for non-uint256 data types is not accurate.
Case 3:
Some detection results of the Mythril tool:
▷ According to the author’s analysis, the Mythrill tool did not process some specific variables, resulting in false positives. Such as arrays, msg.value, now, etc.
02. Cases of specific detection items for VaaS tools
Case 1:
...
contract ERC20 is ERC20Basic {
function allowance(address owner, address spender) constant returns (uint);
function transferFrom(address from, address to, uint value);
function approve(address spender, uint value);
event Approval(address indexed owner, address indexed spender, uint value);
}
...
function transfer(address _to, uint _value) onlyPayloadSize(2 * 32) {
balances[msg.sender] = balances[msg.sender].sub(_value);
balances[_to] = balances[_to].add(_value);
Transfer(msg.sender, _to, _value);
}
Test Results:
Case 2:
contract A {
B b;
uint c;
function test(uint a){
b = new B(a);
c = b.get(200);
}
}
contract B {
uint b;
function B(uint e){
b=100;
}
function get(uint a)returns(uint){
require(a<100);
return a;
}
}
Test Results:
▷ According to the author’s analysis, in Case 2, regarding the call between contracts, if the source code is available, the VaaS tool can be successfully called and tested; but the Mythril tool cannot. This is one of the reasons why the Mythril tool cannot perform business contract verification.
Through the above simple comparative analysis of the logic, dimensions, and data of VaaS tools and Mythril tools, the author believes that readers will be able to make corresponding judgments and evaluations based on their own business orientation and focus after reading.
Regardless of smart contracts and blockchain applications, or even the security of the entire blockchain industry, in the future, we will need to develop in a model that balances the relationship between supply (growth rate) and demand (security), and we need more Clearly know where the pain points of the current status quo are, and how to improve and innovate in response to the pain points.
Whether as a supporter of cutting-edge technology or a geek of blockchain technology, anyone with insight who has decentralized thinking and recognizes that smart contracts and blockchain applications will have far-reaching influence in the future can understand the author's aim at "form" Chemical verification" is the purpose of this test report.
It is true that although more attention is currently being paid to how to promote the implementation of smart contracts and blockchain applications and the overall construction of the blockchain ecosystem, if there are still various loopholes and risks in the underlying technical architecture that have not been resolved , it would be too ambitious.
Therefore, the author suggests that in order to ensure the security of massive smart contracts and blockchain applications, as well as maintain the good operation and maintenance of blockchain ecology, "formal verification" has become an important way of automated auditing.
It is a necessary stage for the development of current smart contracts and blockchain applications to judge the feasibility of a certain verification and audit tool through evaluation dimensions such as false negative rate, false positive rate, hit rate, and test time limit. Chain practitioners need to earnestly implement the mission.
IOS
Android