SWC 是弱安全智慧合約分類及對應案例，https://swcregistry.io/[1]
二、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[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 /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 漏洞。
2、交易數-t 引數
在漏洞檢測中，有一個很重要的引數-t（--transaction-count 交易數），有必要單獨拿出來說一下。在執行 analyze 時，Mythril 會在一個特製的 EVM 虛擬機器中執行合約，預設的交易數是 2，對於大多數的漏洞（如整數溢位）足矣被發現。
由於每個交易可以具有多個有效的最終狀態，在理論上，要探索的狀態空間與交易數量成指數關係，交易個數越大，執行時間也越長。Mythril 在處理多個交易方面透過分析程式路徑在讀寫狀態變數的過程關聯關係，可以縮小交易個數。
如 Mythril 官方提供的 KillBilly 合約例子。程式碼如下(原始碼來自：https://gist.github.com/b-mueller/2b251297ce88aa7628680f50f177a81a#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 /Users/aaa/go/src/six-days/blockchain:/contract mythril/myth a /contract/killbilly.sol -t 2
執行結果如下所示。
指定交易數為 3
docker run -v /Users/aaa/go/src/six-days/blockchain:/contract mythril/myth a /contract/killbilly.sol -t 3
執行結果如下所示。
可以看到，此時 swc 106 漏洞已被發現。
三、總結
自從以太坊橫空出世以來，智慧合約安全問題層出不窮，給專案方和使用者帶來了巨大的損失。Mythril 安全檢查工具對於 SWC 中的一些安全漏洞能夠有效檢測出來，為智慧合約的安全性提供了安全保障。在使用 Mythril 工具時，也要謹記工具不是萬能的，對於一些隱藏的比較深或者測試用例複雜的漏洞，Mythril 很難檢測出來。如著名的由於整數溢位而導致專案歸零 BEC 的 ERC20 合約https://swcregistry.io/docs/SWC-101#bectokensol[18]，Mythril 並沒有檢測出溢位漏洞。
四、參考
https://github.com/ConsenSys/mythril[19]
https://mythril-classic.readthedocs.io/en/master/[20]
https://swcregistry.io/[21]
https://medium.com/hackernoon/practical-smart-contract-security-analysis-and-exploitation-part-1-6c2f2320b0c[22]
