隨著以智能合約（Smart Contract）及區塊鏈應用（DApp）為核心的區塊鏈2.0時代逐漸成為主流，智能合約及區塊鏈應用的安全性也越發成為業界備受關注的焦點。
尤其是，在經歷過諸如THE DAO、幣安被盜等事件，智能合約及區塊鏈應用的安全性究竟應該如何得到驗證和保障，業已成為當前區塊鏈業界亟待解決的痛點。
筆者作過簡單統計，自17年9月到18年9月期間，智能合約及區塊鏈應用的相關漏洞呈頻繁爆發的模式增長，並且所造成的後果都是影響深遠的。不僅直接造成了巨額的金額損失；從長遠發展角度上來看，更是影響到區塊鏈這項新興技術在未來的可持續發展。
另外，儘管當前智能合約及區塊鏈應用的潛在漏洞並未得到妥善解決，可現狀卻是，智能合約及區塊鏈應用的數量每天仍在以萬計的平均增長率飛速提升。
不難看出，智能合約及區塊鏈應用的增長率和安全性，正在以一種不太『健康』的關係並存。如果我們以供求關係來作類比（增長率為『供』；安全性為『求』），當下智能合約及區塊鏈應用的普遍現狀即是『供不應求』的狀態。
基於此，如何保證海量智能合約及區塊鏈應用的安全，已成為區塊鏈行業內具備前瞻性的企業和個人所思考的核心問題。其實，當前行業內已有特行的方法來攻略這個痛點，諸如特征代碼匹配、基於符號執行和符號抽象的自動審計、基於形式化驗證的自動審計等都是較為可行的辦法。其中，經過業界的廣泛探究和實踐，『基於形式化驗證的自動審計』已成為了業內相對成熟和主流的方式。
二級標題
二級標題
VaaS & Mythril工具簡介
01. VaaS工具簡介
VaaS工具是由Beosin成都鏈安採用自有知識產權獨立研發的自動形式化驗證工具，能夠為智能合約和區塊鏈應用提供『軍事級』的形式化驗證服務，可精確定位到有風險的代碼位置並指出風險原因，有效檢測出智能合約常規安全漏洞、安全屬性和功能正確性，精確度高達95%以上。
二級標題
二級標題
測試案例組成
合約測試案例組成包括代幣合約260個及業務合約20個。
二級標題
二級標題
測試結果總覽
VaaS工具可檢測出代幣類和業務類的所有合約測試案例；但Mythril工具僅能檢測出代幣類合約，卻無法對業務類合約進行檢測。因此需要注意的是，本次測試結果總覽僅是對代幣類合約所羅列的對比分析。
VaaS工具總計有28項漏洞檢查；但Mythril工具相對於VaaS工具只有9項漏洞檢測。因此VaaS工具的檢測項是遠遠多於Mythril工具的檢測項。具體檢測項對比如下：
VaaS & Mythril檢測項對比
01. 之於兩者相同檢測項的檢測結果
對於選擇的260個代幣測試用例，Mythril工具在15分鐘的時限內，可跑出184個合約結果，76個無檢測結果；而VaaS工具可跑出全部結果。取Mythril工具和VaaS工具雙方均可跑出的184個結果進行對比，結果如下。
命中率&誤報率
通過檢測結果對比，之於相同的檢測項，VaaS工具的檢測能力是遠遠高於Mythril工具的檢測能力。據計算，VaaS工具的檢測精度為96.9%；Mythril工具的檢測精度為36.6%；而VaaS工具的誤報率為15.3%；Mythril工具的誤報率為48.5%。具體見下圖。
需要注意的是，命中率和誤報率的計算公式為：
命中率= 命中個數/總問題個數
誤報率= 誤報個數/(誤報個數+命中個數)
筆者統計，VaaS工具和Mythril工具兩者都進行的檢測項共計655個問題：
VaaS工具總計檢測出635個問題，命中率為96.9%；誤報共115個，誤報率為15.3%
Mythril工具總計檢測出240個問題，命中率為36.6%；誤報共計226個，誤報率為48.5%。其中，Mythril工具重入攻擊和拒絕服務誤報率較高，佔總數的93.3%。
檢測總數值具體對比如下表：
測試時限
Mythril工具的平均測試時間為226.2s；而VaaS工具的平均測試時間為164.4s。說明VaaS工具的運行效率優於Mythril工具。
02. 之於VaaS工具特有檢測項的檢測結果
案例演示
二級標題
案例演示
案例：
Re Entrancy（重入）
案例：
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 誤報
}
function testFormal(address _testAdddress) public view returns(uint256 time){
TEST t = TEST(_testAdddress);
t.getBlocknumber();//mythril 誤報
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 明顯的誤報
emit WithdrawFunds(msg.sender,_weiToWithdraw);
}
}
VaaS工具測試結果：
Mythril工具測試結果：
▷筆者分析，VaaS工具報出存在重入攻擊的位置；而Mythril工具針對外部的call調用作了告警，總共有4處告警，其中2處是正常的外部調用，另1處是明顯的誤報，誤報率較高。
案例：
案例：
contract TxUserWallet {
address owner;
constructor() public {
owner = msg.sender;
}
function transferTo(address dest, uint amount) public {
require(tx.origin == owner);
dest.transfer(amount);
}
}
VaaS工具測試結果：
Mythril工具測試結果：
▷筆者分析，VaaS工具和Mythril工具均能對tx.origin關鍵字進行檢測報警。
案例：
案例：
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工具測試結果：
Mythril工具測試結果：
▷筆者分析，案例有兩處delegetacall調用，而Mythril工具僅報了一次，存在漏報風險。
案例：
案例：
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工具測試結果：
Mythril工具測試結果：
▷筆者分析，VaaS工具和Mythril工具均能對區塊參數依賴作出檢測；但Mythril工具存在漏報風險。
案例：
案例：
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工具測試結果：
Mythril工具測試結果：
▷筆者分析，VaaS工具和Mythril工具均能針對拒絕服務作出風險檢測。但在此案例中，highestBidder可能是惡意攻擊合約，而導致transfer恆不成功，從而導致合約拒接服務，此案例VaaS工具能夠檢測出拒絕服務風險，Mythril工具未檢出。
案例：
案例：
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工具測試結果：
Mythril工具測試結果：
▷筆者分析，VaaS工具和Mythril工具均能對未檢查call調用的返回值檢測；但Mythril工具存在漏報風險。
案例1：
案例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);
}
}
案例2：
案例2：
contract A {
uint c;
function add(uint8 a,uint8 b){
uint8 sum = a+b;
c=sum;
}
}
VaaS工具測試結果：
Mythril工具測試結果：
案例3：
案例3：
Mythril工具的一些檢測結果：
▷筆者分析，Mythrill工具對一些特定變量未作處理，導致誤報。比如數組，msg.value，now等。
案例1：
案例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);
}
案例2：
案例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;
}
}
測試結果：
▷筆者分析，在案例2中關於合約間的調用問題，在擁有源碼的情況下，VaaS工具是可以調用成功並進行測試的；而Mythril工具不行。這也是Mythril工具無法進行業務合約驗證的原因之一。
通過以上對VaaS工具和Mythril工具邏輯、維度、數據進行簡單的對比分析，筆者認為，讀者在閱後將能夠根據自身業務取向和側重作出相應的判斷和評估。
且毋論智能合約和區塊鏈應用，甚至整個區塊鏈行業的安全性，未來都將需要以一種供（增長率）求（安全性）關係平衡的模式向前發展，我們就更需要清楚地知道，當前現狀的痛點所在，以及如何針對該痛點進行改進和革新。
無論是作為前沿科技擁戴者，還是區塊鏈技術極客，但凡具備去中心化思維以及認可智能合約及區塊鏈應用在未來具備深遠影響力的有識之士，都能明白筆者針對『形式化驗證』作此篇測試報告的用意。
誠然，儘管當下更多的目光放是放在如何推進智能合約和區塊鏈應用的落地以及區塊鏈全生態的統籌建設上，但倘若底層技術架構方面本身都還存在各種漏洞風險尚未解決，就未免太過於好高騖遠了。
因此，筆者建議，為保障海量智能合約及區塊鏈應用的安全，以及維護區塊鏈生態的良好運維，『形式化驗證』業已成為了當下自動化審計的重要途徑。
通過漏報率、誤報率、命中率、測試時限等評估維度，來整體判別某種驗證和審計工具的可行性，是當前智能合約及區塊鏈應用發展的必經階段，也是作為區塊鏈從業者需要認真踐行的使命。
IOS
Android