关于形式化验证两大工具VaaS 、 Mythril测试对比报告

随着以智能合约（Smart Contract）及区块链应用（DApp）为核心的区块链2.0时代逐渐成为主流，智能合约及区块链应用的安全性也越发成为业界备受关注的焦点。

尤其是，在经历过诸如THE DAO、币安被盗等事件，智能合约及区块链应用的安全性究竟应该如何得到验证和保障，业已成为当前区块链业界亟待解决的痛点。

笔者作过简单统计，自17年9月到18年9月期间，智能合约及区块链应用的相关漏洞呈频繁爆发的模式增长，并且所造成的后果都是影响深远的。不仅直接造成了巨额的金额损失；从长远发展角度上来看，更是影响到区块链这项新兴技术在未来的可持续发展。

另外，尽管当前智能合约及区块链应用的潜在漏洞并未得到妥善解决，可现状却是，智能合约及区块链应用的数量每天仍在以万计的平均增长率飞速提升。

不难看出，智能合约及区块链应用的增长率和安全性，正在以一种不太『健康』的关系并存。如果我们以供求关系来作类比（增长率为『供』；安全性为『求』），当下智能合约及区块链应用的普遍现状即是『供不应求』的状态。

基于此，如何保证海量智能合约及区块链应用的安全，已成为区块链行业内具备前瞻性的企业和个人所思考的核心问题。其实，当前行业内已有特行的方法来攻略这个痛点，诸如特征代码匹配、基于符号执行和符号抽象的自动审计、基于形式化验证的自动审计等都是较为可行的办法。其中，经过业界的广泛探究和实践，『基于形式化验证的自动审计』已成为了业内相对成熟和主流的方式。

因此，笔者特地将着眼点聚焦于『形式化验证』，选取当前行业内主流的两大形式化验证工具（VaaS & Mythril），进行了一个简单的测试对比。特别指出，用以测试的Mythril工具版本为『0.21.12』。

以下为相关的测试报告，希望能够抛砖引玉，为广大读者带来一些直观感受和客观建议。若有不妥之处，欢迎留言指出。（本文仅代表笔者作测试后的个人建议，不对任何产品和工具作相关背书）

1

VaaS & Mythril工具简介

01.VaaS工具简介

VaaS工具是由Beosin成都链安采用自有知识产权独立研发的自动形式化验证工具，能够为智能合约和区块链应用提供『军事级』的形式化验证服务，可精确定位到有风险的代码位置并指出风险原因，有效检测出智能合约常规安全漏洞、安全属性和功能正确性，精确度高达95%以上。

02.Mythril工具简介

Mythril工具是由以太坊开源社区所提供的安全分析工具，能够检测出Solidity智能合约中的安全漏洞并实现深入分析，是用以分析以太坊智能合约及区块链应用安全性的安全分析工具及引擎，支持常用IDE集成。

2

测试案例组成

合约测试案例组成包括代币合约260个及业务合约20个。

• 代币合约包括Top200的代币合约及60个用以审计的典型代币合约，覆盖到了ICO、锁仓、铸币和销毁等功能。

• 业务合约包括拍卖、商城、溯源等业务类合约共20个。

3

测试结果总览

VaaS工具可检测出代币类和业务类的所有合约测试案例；但Mythril工具仅能检测出代币类合约，却无法对业务类合约进行检测。因此需要注意的是，本次测试结果总览仅是对代币类合约所罗列的对比分析。

VaaS工具总计有28项漏洞检查；但Mythril工具相对于VaaS工具只有9项漏洞检测。因此VaaS工具的检测项是远远多于Mythril工具的检测项。具体检测项对比如下：

VaaS & Mythril检测项对比

漏洞检测项

Mythril

VaaS

ERC20 标准规范

Fake Recharge Vulnerability（假充值）

TransferToZeroAddress（目标零地址检测）

Re Entrancy（重入）

TXOriginAuthentication（tx.origin使用错误）

Invoke Low Level Calls（call调用,delegatecall调用,自杀函数调用）

BlockMembers Manipulation（区块参数依赖）

Invoke Extcodesize（调用Extcodesize函数）

Invoke Ecrecover（调用Ecrecover函数）

Unchecked Call Or Send Return Values（call和send的返回值检测）

Denial of service（拒绝服务）

Redefine Variable From Base Contracts（合约继承中的变量覆盖）

Unprotected Ether Withdrawal（无保护的转账）

Check This Balance（合约资金受到严格限制）

ArbitraryJumpwith Function（具有函数类型变量的任）

Overload Assert（重写assert函数）

CompilerVersionDeclaration（编译器版本声明）

Constructor Mistyping（构造函数失配）

Complex Code In Fallback Function（fallback函数使用）

Unary Operation（+= 写成=+ ）

No Return（返回值适配）

Unchecked Api Return Values（没检查API返回值）

Emit Event Beforerevert(事件在revert前触发了)

Integer Overflow（整数溢出）

Exception State（异常检测，包括数组越界、除0、assert失败等）

Call problem

Function problem

Require Fail

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%。

检测总数值具体对比如下表：

—

VaaS

Mythril

检测用例个数

184

184

问题总数

655

655

命中个数

635

240

误报个数

115

226

命中率

96.9%

36.6%

误报率

15.3%

48.5%

针对每项详细结果对比如下表：

漏洞检测项

总数

Mythril

VaaS

命中

误报

命中

误报

Re Entrancy（重入）

14

7

115

14

0

50%

94.2%

100%

0

TXOrigin

Authentication

（tx.origin使用错误）

4

4

0

4

0

100%

0

100%

0

BlockMembers

Manipulation

（区块参数依赖）

116

21

0

116

0

18.1%

0

100%

0

Denial of service

（拒绝服务）

14

7

83

14

0

50%

92.2%

100%

0

Invoke Low Level Calls

（call调用,delegatecall调用,自杀函数调用）

54

7

0

54

0

12.9%

0

100%

0

Unchecked Call Or Send Return Values

（call和send的返回值检测）

25

4

0

25

0

16%

0

100%

0

Integer Overflow

（整数溢出）

356

126

28

336

90

35.3%

18.1%

94.3%

20.1%

Exception State

（assert失败）

72

64

0

72

25

88.8%

0

100%

25.7%

• 测试时限

Mythril工具的平均测试时间为226.2s；而VaaS工具的平均测试时间为164.4s。说明VaaS工具的运行效率优于Mythril工具。

02.之于VaaS工具特有检测项的检测结果

具体见下表：

VaaS工具特有检测项用例结果展示说明

分类

VaaS log 关键字

说明

ERC20 标准规范（ERC20 Standard）

Erc20 Variable

ERC20 变量命名规范

Erc20 Function

Erc20函数命名规范

Erc20 Event

Erc20 event使用规范

Fake Recharge Vulnerability

假充值

Transfer To Zero Address

目标地址非零检查

敏感函数调用（Sensitive Function Call）

Invoke Extcodesize

调用Extcodesize函数

Invoke Ecrecover

调用Ecrecover函数

不推荐使用（Deprecated Usage）

Redefine Variable From Base Contracts

合约继承中的变量覆盖

check_this_balance

合约资金受到严格限制

unused_variables

未使用的变量

Arbitrary Jump with Function Type Variable

具有函数类型变量的任意跳转

Overload Assert

重写assert函数

Solidity编码规范（Solidity Coding Conventions）

Compiler Version Declaration

编译器版本声明

Constructor Mistyping

构造函数失配

Complex Code In Fallback Function

fallback函数使用

Unary Operation

+= 写成=+

Constructor Warning

缺少主构造函数

No Return

返回值适配

Unchecked Api Return Values

没检查API返回值

Emit Event Beforerevert

事件在revert前触发了

逻辑验证

Call problem

call调用执行总是revert

Function problem

Function执行总是失败

4

案例演示

01.两者相同检测项案例

• 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处是明显的误报，误报率较高。

• TXOriginAuthentication（tx.origin使用错误）

案例：

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关键字进行检测报警。

• Invoke Low Level Calls（call调用,delegatecall调用,自杀函数调用）

案例：

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工具仅报了一次，存在漏报风险。

• BlockMembers Manipulation（区块参数依赖）

案例：

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工具存在漏报风险。

• Denial of service（拒绝服务）

案例：

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工具未检出。

• Unchecked Call Or Send Return Values（call和send的返回值检测）

案例：

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工具存在漏报风险。

• Integer Overflow（整数溢出）

案例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);

}

}

笔者分析，以上案例没有对balances[owner]的值作检测，可能会产生下溢，但Mythrill工具不会报错，说明Mythrill工具对常数的运算不会作检测。

案例2：

contract A {

uint c;

function add(uint8 a,uint8 b){

uint8 sum = a+b;

c=sum;

}

}

• VaaS工具测试结果：

• Mythril工具测试结果：

笔者分析，Mythrill工具对非uint256数据类型的溢出检测不准确。

案例3：

• Mythril工具的一些检测结果：

笔者分析，Mythrill工具对一些特定变量未作处理，导致误报。比如数组，msg.value，now等。

02.VaaS工具特有检测项案例

案例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：

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工具逻辑、维度、数据进行简单的对比分析，笔者认为，读者在阅后将能够根据自身业务取向和侧重作出相应的判断和评估。

且毋论智能合约和区块链应用，甚至整个区块链行业的安全性，未来都将需要以一种供（增长率）求（安全性）关系平衡的模式向前发展，我们就更需要清楚地知道，当前现状的痛点所在，以及如何针对该痛点进行改进和革新。

无论是作为前沿科技拥戴者，还是区块链技术极客，但凡具备去中心化思维以及认可智能合约及区块链应用在未来具备深远影响力的有识之士，都能明白笔者针对『形式化验证』作此篇测试报告的用意。

诚然，尽管当下更多的目光放是放在如何推进智能合约和区块链应用的落地以及区块链全生态的统筹建设上，但倘若底层技术架构方面本身都还存在各种漏洞风险尚未解决，就未免太过于好高骛远了。

因此，笔者建议，为保障海量智能合约及区块链应用的安全，以及维护区块链生态的良好运维，『形式化验证』业已成为了当下自动化审计的重要途径。

通过漏报率、误报率、命中率、测试时限等评估维度，来整体判别某种验证和审计工具的可行性，是当前智能合约及区块链应用发展的必经阶段，也是作为区块链从业者需要认真践行的使命。

—-

编译者/作者：成都链安科技

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。