在這個教程中，我們将學習Mythril的安裝與使用方法，了解Mythril的工作原理，掌握如何利用Ether Thief和Suicide子產品分析合約的安全漏洞，以及如何配置Mythril安全分析的交易數量參數和執行逾時參數。
用自己熟悉的語言學習以太坊DApp開發： Java | Php Python .Net / C# Golang Node.JS Flutter / Dart
1、安裝Mythril安全分析工具
執行如下指令安裝Mythril：
$ pip install mythril 使用如下指令檢查安裝是否成功，確定版本不低于0.21.7：
$ myth version
Mythril version v0.21.15 Mythril最基本的安全分析指令是
myth analyze
，例如：
$ myth analyze <Solidity file>
$ myth analyze -a <contract address> 沒有其他參數的話，myth analyze指令将執行适合大多數情況的通用分析。
2、Mythril工作原理
Mythril通過在一個特制的以太坊虛拟機裡運作智能合約位元組碼來檢查合約的安全問題，它使用
符号執行技術來檢查程式可能的狀态，分析過程包含以下步驟：
1、擷取合約位元組碼
2、初始化合約賬戶的狀态
3、利用n個交易來探索合約的狀态空間，n預設為2，但可以設定為任意值
4、當發現不希望的狀态時，證明或否定其在特定假設下的可到達性
當發現一個漏洞狀态時，我們可以計算到達該狀态所需的交易。這不僅有助于确定問題的根源，而且也可以用于漏洞利用。
3、Mythril的基本使用方法
現在讓我們用Mythril分析一個智能合約。TOkenSale是一個簡單的用于買賣token的智能合約，下面是其源代碼：
分析solidity源碼要比分析鍊上的合約執行個體簡單一些：在提供源碼的情況下，Mythril可以展示其發現的bug所對應的代碼位置。下載下傳
TokenSale并将其另存為tokensale.sol，然後運作如下指令分析該合約的安全問題：
$ myth analyze -m ether_thief tokensale.sol -m
參數用來聲明一組要執行的
Mythril分析子產品, 彼此之間用逗号隔開。下面讓我們先了解一下Ether Thief子產品。
4、使用Ether Thief子產品檢測合約的以太币洩露問題
正如其名稱所示，Ether Thief子產品檢查從合約中提取以太币的交易序列，它搜尋滿足以下條件的狀态：
- 可以從合約提取的非零數量的以太币
- 從合約提取以太币的賬号不是合約的建立賬号
- 從合約提取的以太币數量超過了該賬号之前存入合約的數量
這是一個發現合約存在以太币洩露問題的好辦法。現在讓我們用
Ether Thief子產品分析一下TokenSale合約：
$ myth analyze -m ether_thief tokensale.sol==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: TokenSaleChallenge
Function name: sell(uint256)
PC address: 696
Estimated Gas Usage: 6373 - 27034
Anyone can withdraw ETH from the contract account.
Arbitrary senders other than the contract creator can withdraw ETH
from the contract account without previously having sent an
equivalent amount of ETH to it. This is likely to be a vulnerability.
--------------------
In file: tokensale.sol:25
msg.sender.transfer(numTokens * PRICE_PER_TOKEN)
--------------------
Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0xde0b6b3a7640000
Caller: [ATTACKER], data: 0xd96a094ab000000000000000000000000000000000000000000000000000000000000000, value: 0x0
Caller: [ATTACKER], data: 0xe4849b323000180504000000000300013b45000000380000000002c00000020400801080, value: 0x0 Mythtril報告說在withdrawal函數中發現了一個問題，但是根源還不清楚。如果你還沒找出bug在哪裡，可以再仔細檢查下TokenSale的代碼并嘗試找出攻擊。
可能你已經推斷出來，上面的代碼中存在整數溢出問題。要利用這個漏洞，我們需要向buy()函數傳入一個特定的值 —— 好消息是，Mythril已經自動幫我們計算了這個值！看一下上面的執行結果中transaction Sequence部分的輸出：
Transaction Sequence:Caller: [CREATOR], data: [CONTRACT CREATION], value: 0xde0b6b3a7640000
Caller: [ATTACKER], data: 0xd96a094a2000000000000000000000000000000000000000000000000000000000000000, value: 0x0
Caller: [ATTACKER], data: 0xe4849b323000180504000000000300013b45000000380000000002c00000020400801080, value: 0x0 這一部分列出了3個交易：1個合約建立交易（由合約的creator發送）和2個攻擊者發送的交易。交易的value字段的值标明沒有以太币從攻擊者轉入合約。讓我們仔細看一下data字段：
第一個交易包含4位元組的函數簽名以及看起來沒什麼危害的一個額外的位元組—— 0x20 —— 表示uint256類型的num_tokens參數的最左端位元組，是以最終傳入num_tokens的值是：
buy(0x2000000000000000000000000000000000000000000000000000000000000000) 現在讓我們看一下這個輸入值對第16行require語句的影響：
require(msg.value == numTokens * PRICE_PER_TOKEN); PRICE_PER_TOKEN 被設定為1 Ether，對應1e18 wei，将這個數量與上面Mythril給出的值相乘就會産生整數溢出。更确切地說，uint256(1e18) * uint256(numTokens) 的結果為0 。
是以require語句就會通過，然後海量的token就記在交易發送方的名下了，即時他們沒有發送任何以太币。
在第2個交易中，不合法的token被出售以換回以太币，即調用sell(uint256)。由于Mythril符号化表示合約賬戶餘額，它為numTokens輸出一個非常大的随機值。在現實中，攻擊者将會利用與賬戶實際以太币餘額比對的值。
5、配置Mythril安全分析的交易數量
在使用Mythril時需要了解的一個重要概念，就是交易數量。這個變量用來指定進行符号化執行的交易的數量。預設值2對于檢測許多常見bug都足夠了，例如整數溢出、未初始化的存儲變量以及錯誤指令的構造函數等。然而，隻有2個交易深度還無法發現那些在更多交易下才會顯現的bug。
因為每個交易都可以有多個有效的最終狀态，那麼當交易數量增加後，潛在的狀态空間數量（理論上）将指數級增長。幸運的是，Mythril還是很聰明的，它通過分析程式執行路徑之間的關系可以縮小後續交易的搜尋空間，這意味着你可以在合理的時間架構内執行多個交易。
下面讓我們看另一個例子，看看你是否能找出其中的安全問題，注意
合約名字：
這個合約有一個後門，它允許任何知道密碼的人成為合約的owner —— 我們知道，私有狀态變量并不是真的秘密，和公開狀态變量的差別在于，solc不會為私有變量生成通路函數。
另一個流行的Mythril子產品是Suicide，這個子產品檢查那些由合約建立者之外的賬号發送的可能殺掉合約的交易。運作Mythril分析上面的killme合約，就可以”意外地“殺掉合約：
$ myth analyze killme.sol
The analysis was completed successfully. No issues were detected. Mythril看起來忽略了合約存在的漏洞，原因是至少需要3個交易才能殺掉合約：發送方必須向activePassword(bytes11 password)方法傳入正确的密碼，然後調用pwnContract()成為owner，最後調用kill()觸發合約自毀。
現在讓我們看看如果用-t參數增加交易數量後會得到什麼結果：
$ myth analyze killme.sol -t3
==== Unprotected Selfdestruct ====
SWC ID: 106
Severity: High
Contract: Killme
Function name: kill()
PC address: 371
Estimated Gas Usage: 613 - 1038
The contract can be killed by anyone.
Anyone can kill this contract and withdraw its balance to an arbitrary address.
--------------------
In file: killme.sol:19
selfdestruct(msg.sender)
--------------------
Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0
Caller: [ATTACKER], data: 0xa6e0e35e63727970746f6b69747479747474747474747474747474747474747474747474, value: 0x0
Caller: [ATTACKER], data: 0x2eb00c1b, value: 0x0
Caller: [ATTACKER], data: 0x41c0e1b5, value: 0x0 這次檢測出了合約中的問題，我們得到了包含3個交易的序列。檢視交易的data可以了解被調用的函數名以及參數：
注意：交易1中的位元組序列0x747474(…) 是用于補齊uint256參數的随機資料，這部分資料可以是任意值。
6、設定Mythril安全分析的執行逾時
預設情況下，Mythril會嘗試執行-t參數指定數量的交易。然而，有時我們希望能指定執行時間的上限。如果增加--execution-timeout參數，Mythril就會在超過指定事件後終止，并傳回在此期間發現的所有問題。
注意你可以在任何時候使用CTRL+C來中斷分析任務的執行，這時Mythril也會傳回此前已經發現的漏洞。例如，可以用Mythril分析Parity的WalletLibrary并設定最多分析10分鐘：
$ myth analyze --execution-timeout 600 -t2 -mether_thief,suicide -c [WALLETLIBRARY-BYTECOE]
==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: MAIN
Function name: execute(address,uint256,bytes)
PC address: 4384
Estimated Gas Usage: 9518 - 32483
Anyone can withdraw ETH from the contract account.
Arbitrary senders other than the contract creator can withdraw ETH
from the contract account without previously having sent an
equivalent amount of ETH to it. This is likely to be a vulnerability.
--------------------
Transaction Sequence:
Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0
Caller: [ATTACKER], data: 0xe46dcfeb4000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080, value: 0x0
Caller: [ATTACKER], data: 0xb61d27f6000000000000000000000000deadbeefdeadbeefdeadbeefdeadbeefdeadbeef000000000000000000010000000000000000000000000000000000000000000108, value: 0x0
real 10m3.260s
user 9m11.115s
sys 0m7.727s 原文連結：
Mythril教程 — 彙智網