一、Mythril是什么

Mythril是一個以太坊官方推薦的智能合約安全分析工具，使用符合執(zhí)行來檢測智能合約中的各種安全漏洞，在Remix、Truffle等IDE里都有集成。
其包含的安全分析模型如下。

SWC是弱安全智能合約分類及對應案例，https://swcregistry.io/

二、Mythril安裝

Mythril是使用python開發(fā)的，可以使用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 專業(yè)版（收費）
• list-detectors，列出可用的安全檢測模型
• read-storage，通過rpc讀取指定地址的存儲插槽
• leveldb-search，從本地leveldb中檢索
• function-to-hash，計算合約方法的函數(shù)標識碼
• hash-to-address，將hash轉(zhuǎn)換為以太坊地址
• version，版本號

這里以一個簡單的整型溢出合約為例，執(zhí)行analyze檢查命令，看看能不能檢測出整數(shù)溢出問題。
合約地址
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，執(zhí)行超時時間
• o 輸出格式，可選text/markdown/json/jsonv2
• t 交易個數(shù)

運行結(jié)果
運行結(jié)果如下圖所示，檢測出了swc 101漏洞。

image.png

2、交易數(shù)-t參數(shù)

在漏洞檢測中，有一個很重要的參數(shù)-t（--transaction-count 交易數(shù)），有必要單獨拿出來說一下。
在執(zhí)行analyze時，Mythril會在一個特制的EVM虛擬機中執(zhí)行合約，默認的交易數(shù)是2，對于大多數(shù)的漏洞（如整數(shù)溢出）足矣被發(fā)現(xiàn)。

由于每個交易可以具有多個有效的最終狀態(tài)，在理論上，要探索的狀態(tài)空間與交易數(shù)量成指數(shù)關(guān)系，交易個數(shù)越大，執(zhí)行時間也越長。Mythril在處理多個交易方面通過分析程序路徑在讀寫狀態(tài)變量的過程關(guān)聯(lián)關(guān)系，可以縮小交易個數(shù)。

如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);
    }
}

在這個合約中要想銷毀合約，需要先調(diào)用killerize方法，為調(diào)用者授權(quán)，在調(diào)用activatekillability方法，將is_killable變量設置為true，最后調(diào)用commencekilling方法消耗合約。
也就是說，要想檢測出訪問控制不當造成的合約銷毀（SWC-106）漏洞，至少需要執(zhí)行3個交易。

指定交易數(shù)為2

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

運行結(jié)果如下所示。

image.png

指定交易數(shù)為3

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

運行結(jié)果如下所示。

image.png

可以看到，此時swc 106漏洞已被發(fā)現(xiàn)。

三、總結(jié)

自從以太坊橫空出世以來，智能合約安全問題層出不窮，給項目方和用戶帶來了巨大的損失。
Mythril安全檢查工具對于SWC中的一些安全漏洞能夠有效檢測出來，為智能合約的安全性提供了安全保障。
在使用Mythril工具時，也要謹記工具不是萬能的，對于一些隱藏的比較深或者測試用例復雜的漏洞，Mythril很難檢測出來。
如著名的由于整數(shù)溢出而導致項目歸零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