一、Mythril是什么

Mythril是一个以太坊官方推荐的智能合约安全分析工具，使用符合执行来检测智能合约中的各种安全漏洞，在Remix、Truffle等IDE里都有集成。
其包含的安全分析模型如下。

SWC是弱安全智能合约分类及对应案例，https://swcregistry.io/

二、Mythril安装

Mythril是使用python开发的，可以使用pip3和docker方式安装。

1、pip3-Mac OS安装

brew update
brew upgrade
brew tap ethereum/ethereum
brew install leveldb
brew install solidity
pip3 install mythril

2、pip3-Ubuntu安装

# Update
sudo apt update

# Install solc
sudo apt install software-properties-common
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt install solc

# Install libssl-dev, python3-dev, and python3-pip
sudo apt install libssl-dev python3-dev python3-pip

# Install mythril
pip3 install mythril
myth --version

3、docker安装

# Pull the latest release of mythril/myth
docker pull mythril/myth

三、Mythril使用

Mythril安装成功后，使用myth -h命令查看帮助文档。
我这里使用docker安装的，查看帮助的命令为：
docker run mythril/myth -h

1、Mythril命令

通过帮助命令，可以看到Mythril的命令有：

• analyze (a)，分析智能合约
• disassemble (d)，拆解合约，返回合约对应的Opcodes
• pro (p)，使用Mythril 专业版（收费）
• list-detectors，列出可用的安全检测模型
• read-storage，通过rpc读取指定地址的存储插槽
• leveldb-search，从本地leveldb中检索
• function-to-hash，计算合约方法的函数标识码
• hash-to-address，将hash转换为以太坊地址
• version，版本号

这里以一个简单的整型溢出合约为例，执行analyze检查命令，看看能不能检测出整数溢出问题。
合约地址
https://swcregistry.io/docs/SWC-101#overflow_simple_addsol

漏洞分析
漏洞是一个加法的整型溢出问题，add方法中，初始时balance =1，此时deposit输入值为uint256的最大值2**256-1，计算得到的balance为0

pragma solidity 0.4.24;
contract Overflow_Add {
    uint public balance = 1;

    function add(uint256 deposit) public {
        balance += deposit;
    }
}

运行命令
docker run -v /Users/aaa/go/src/six-days/ethereum-contracts:/contract mythril/myth analyze /contract/bec.sol --solv 0.4.25 --solver-timeout 60 --execution-timeout 60 -o json -t 3
其中：

• solv 是指定solidity编译版本
• solver-timeout solidity版本下载超时时间
• execution-timeout，执行超时时间
• o 输出格式，可选text/markdown/json/jsonv2
• t 交易个数

运行结果
运行结果如下图所示，检测出了swc 101漏洞。

image.png

2、交易数-t参数

在漏洞检测中，有一个很重要的参数-t（--transaction-count 交易数），有必要单独拿出来说一下。
在执行analyze时，Mythril会在一个特制的EVM虚拟机中执行合约，默认的交易数是2，对于大多数的漏洞（如整数溢出）足矣被发现。

由于每个交易可以具有多个有效的最终状态，在理论上，要探索的状态空间与交易数量成指数关系，交易个数越大，执行时间也越长。Mythril在处理多个交易方面通过分析程序路径在读写状态变量的过程关联关系，可以缩小交易个数。

如Mythril官方提供的KillBilly合约例子。代码如下(源码来自：https://gist.github.com/b-mueller/2b251297ce88aa7628680f50f177a81a#file-killbilly-sol
)。

pragma solidity ^0.5.7;

contract KillBilly {
    bool public is_killable;
    mapping (address => bool) public approved_killers;

    constructor() public {
        is_killable = false;
    }

    function killerize(address addr) public {
        approved_killers[addr] = true;
    }

    function activatekillability() public {
        require(approved_killers[msg.sender] == true);
        is_killable = true;
    }

    function commencekilling() public {
        require(is_killable);
        selfdestruct(msg.sender);
    }
}

在这个合约中要想销毁合约，需要先调用killerize方法，为调用者授权，在调用activatekillability方法，将is_killable变量设置为true，最后调用commencekilling方法消耗合约。
也就是说，要想检测出访问控制不当造成的合约销毁（SWC-106）漏洞，至少需要执行3个交易。

指定交易数为2

docker run -v /Users/aaa/go/src/six-days/blockchain:/contract mythril/myth a /contract/killbilly.sol -t 2

运行结果如下所示。

image.png

指定交易数为3

docker run -v /Users/aaa/go/src/six-days/blockchain:/contract mythril/myth a /contract/killbilly.sol -t 3

运行结果如下所示。

image.png

可以看到，此时swc 106漏洞已被发现。

三、总结

自从以太坊横空出世以来，智能合约安全问题层出不穷，给项目方和用户带来了巨大的损失。
Mythril安全检查工具对于SWC中的一些安全漏洞能够有效检测出来，为智能合约的安全性提供了安全保障。
在使用Mythril工具时，也要谨记工具不是万能的，对于一些隐藏的比较深或者测试用例复杂的漏洞，Mythril很难检测出来。
如著名的由于整数溢出而导致项目归零BEC的ERC20合约https://swcregistry.io/docs/SWC-101#bectokensol
，Mythril并没有检测出溢出漏洞。

四、参考

• https://github.com/ConsenSys/mythril
• https://mythril-classic.readthedocs.io/en/master/
• https://swcregistry.io/
• https://medium.com/hackernoon/practical-smart-contract-security-analysis-and-exploitation-part-1-6c2f2320b0c