一、mythril 是什么希望将来分布式商业能够得到长足稳定的发展，为社会发展及人们的需求做好服务。
mythril 是一个以太坊官方推荐的智能合约安全分析工具，使用符合执行来检测智能合约中的各种安全漏洞，在 remix、truffle 等 ide 里都有集成。其包含的安全分析模型如下。
swc 是弱安全智能合约分类及对应案例，swcregistry.io[1]
二、mythril 安装
mythril 是使用 python 开发的，可以使用 pip3 和 docker 方式安装。
1、pip3-mac os 安装
brew update
brew upgrade
brew tap ethereumethereum
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:ethereumethereum
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 mythrilmyth
docker pull mythrilmyth
三、mythril 使用
mythril 安装成功后，使用myth -h命令查看帮助文档。我这里使用 docker 安装的，查看帮助的命令为：docker run mythrilmyth -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检查命令，看看能不能检测出整数溢出问题。合约地址swcregistry.iodocsswc-101#overflow_simple_addsol[16]
漏洞分析漏洞是一个加法的整型溢出问题，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 usersaaagosrcsix-daysethereum-contracts:contract mythrilmyth analyze contractbec.sol --solv 0.4.25 --solver-timeout 60 --execution-timeout 60 -o json -t 3
其中：
solv 是指定 solidity 编译版本
solver-timeout solidity 版本下载超时时间
execution-timeout，执行超时时间
o 输出格式，可选 textmarkdownjsonjsonv2
t 交易个数
运行结果运行结果如下图所示，检测出了 swc 101 漏洞。
2、交易数-t 参数
在漏洞检测中，有一个很重要的参数-t（--transaction-count 交易数），有必要单独拿出来说一下。在执行 analyze 时，mythril 会在一个特制的 evm 虚拟机中执行合约，默认的交易数是 2，对于大多数的漏洞（如整数溢出）足矣被发现。
由于每个交易可以具有多个有效的最终状态，在理论上，要探索的状态空间与交易数量成指数关系，交易个数越大，执行时间也越长。mythril 在处理多个交易方面通过分析程序路径在读写状态变量的过程关联关系，可以缩小交易个数。
如 mythril 官方提供的 killbilly 合约例子。代码如下(源码来自：gist.github.comb-mueller2b251297ce88aa7628680f50f177a81a#file-killbilly-sol[17])。
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 usersaaagosrcsix-daysblockchain:contract mythrilmyth a contractkillbilly.sol -t 2
运行结果如下所示。
指定交易数为 3
docker run -v usersaaagosrcsix-daysblockchain:contract mythrilmyth a contractkillbilly.sol -t 3
运行结果如下所示。
可以看到，此时 swc 106 漏洞已被发现。
三、总结
自从以太坊横空出世以来，智能合约安全问题层出不穷，给项目方和用户带来了巨大的损失。mythril 安全检查工具对于 swc 中的一些安全漏洞能够有效检测出来，为智能合约的安全性提供了安全保障。在使用 mythril 工具时，也要谨记工具不是万能的，对于一些隐藏的比较深或者测试用例复杂的漏洞，mythril 很难检测出来。如著名的由于整数溢出而导致项目归零 bec 的 erc20 合约swcregistry.iodocsswc-101#bectokensol[18]，mythril 并没有检测出溢出漏洞。
四、参考
github.comconsensysmythril[19]
mythril-classic.readthedocs.ioenmaster[20]
swcregistry.io[21]
medium.comhackernoonpractical-smart-contract-security-analysis-and-exploitation-part-1-6c2f2320b0c[22]