Mythril工作原理是什么，很多新手對此不是很清楚，為了幫助大家解決這個難題，下面小編將為大家詳細講解，有這方面需求的人可以來學(xué)習(xí)下，希望你能有所收獲。

創(chuàng)新互聯(lián)建站是一家專業(yè)提供睢陽企業(yè)網(wǎng)站建設(shè),專注與做網(wǎng)站、成都網(wǎng)站制作、HTML5建站、小程序制作等業(yè)務(wù)。10年已為睢陽眾多企業(yè)、政府機構(gòu)等服務(wù)。創(chuàng)新互聯(lián)專業(yè)的建站公司優(yōu)惠進行中。

Mythril是一個基于符號執(zhí)行技術(shù)的以太坊智能合約安全工具，其預(yù)置的檢測模塊可以發(fā)現(xiàn)合約中存在的一些安全問題，例如整數(shù)溢出和重入漏洞。本文的目的是學(xué)習(xí)理解Mythril的符號執(zhí)行機制，以便開發(fā)自己的Solidity安全分析模塊。

用自己熟悉的語言學(xué)習(xí)以太坊DApp開發(fā)：Java | Php | Python | .Net / C# | Golang | Node.JS | Flutter / Dart

Mythril的設(shè)計目標(biāo)之一是讓安全分析工具更簡單易用。換句話說 就是你不需要是計算機科學(xué)領(lǐng)域的博士就可以從符號化分析中獲益。

1、符號執(zhí)行概述

為了說明Mythril的運行機制，我們需要先了解Mythril使用的核心技術(shù) —— 符號執(zhí)行（Symbolic Execution）。如果你之前已經(jīng)比較了解符號執(zhí)行的一般思路，那么本文有助于幫助你梳理相關(guān)的概念。

我認為解釋符號執(zhí)行的最簡單的方法是真正執(zhí)行它并畫圖展示出執(zhí)行過程中發(fā)生的事情。為此，我們將使用下面的solidity函數(shù)作為我們分析的目標(biāo)，讓我們看看是否可以使用符號化分析來得出函數(shù)的結(jié)果為10。

2、具體執(zhí)行： Concrete Execution

在我們開始符號執(zhí)行之前，先看看具體執(zhí)行的結(jié)果。我們可以用多個不同的輸入來執(zhí)行函數(shù)execute(uint256)。例如對于輸入4，將產(chǎn)生如下的執(zhí)行過程：

Initial state (function entry): 
- currently executing: line 1 
- input = 4 
step1: 
- currently executing: line 2 
- input = 4 
- result = uninitialized 
step2: 
- currently executing: line 3 
- input = 4 
- result = 0 
step3: 
- currently executing: line 6: 
- input = 4 
- result = 0

上述過程的圖形化表示如下：

我們可以嘗試不同的輸入，直到找出可以讓函數(shù)返回10的輸入，這種方法被稱為模糊測試（Fuzzing）。

3、符號執(zhí)行：Symbolic Execution

最后我們要符號化執(zhí)行程序了。這意味著我們不再將具體的輸入（例如4）帶入程序執(zhí)行，而是用一個符號來指代具體的輸入。將該符號稱為x，x可以是任何有效的uint256值?，F(xiàn)在讓我們再次執(zhí)行程序。

前兩步的執(zhí)行簡單直白，容易理解：

現(xiàn)在開始進入有趣的部分。在第3行輸入與10進行比較，但是輸入是x，它可以是任何具體的值，因此，x > 10和 x < 10都是可能的。如果這種情況發(fā)生，我們可以創(chuàng)建兩個新的狀態(tài)分支，其中一個對應(yīng) x > 10，另一個對應(yīng)x <= 10。我們還需要記錄這些約束，這樣就可以決定具體的輸入將執(zhí)行哪個路徑。

現(xiàn)在讓我們將狀態(tài)圖擴展到下一步的執(zhí)行：

下面是我們通過符號化執(zhí)行生成的狀態(tài)。有了這些符號化的狀態(tài)，我們可以寫一個簡單的程序來找出什么輸入值可以得到輸出10。

for state in states:
  # Let's filter all the states that are not return statements
  if state.currently_executing != 6:
    continue
  # We want the result to be 10, let's formulate that as a constraint
  result_constraint = (state.result == 10)
  
  # If it is possible to satisfy both the path constraints (these are the constraints collected on each branch)
  # and the result constraint then there must be an input that makes the function return 10
  if is_possible(result_constraint and state.constraints):
    # Using SMT solving we can get an input that will satisfy all the constraints and make the function return 10
    print(give_satisfying_input(result_constraints and state.constraints))

查看上述代碼的執(zhí)行結(jié)果，可以清楚地了解只有狀態(tài)3和狀態(tài)5需要考慮。

對于狀態(tài)3，函數(shù)is_possible(result_constraint and state.constraints)將返回false，因為對于該狀態(tài)我們得到result =0。

現(xiàn)在看一下狀態(tài)5，我們發(fā)現(xiàn)了一些更有趣的東西。讓我們看一下這里考慮的兩個約束：result == 10 and x > 10 。容易看到第一個約束必須滿足，也容易確定 x > 10可以滿足，例如對于輸入11。我只是手動找了一個值來滿足上述約束。再Mythril中，實際上是利用一個SMT（Z3）求解器來找出是否可能滿足這些約束條件，而且Z3還可以給出一個可以滿足約束條件的具體示例，這讓我們可以構(gòu)建一個實際輸入來讓函數(shù)返回10。

作為函數(shù)execute分析的結(jié)論，我們可以說：

1. 輸出為10的可能性存在

2. 可以使用輸入11得到輸出10

看完上述內(nèi)容是否對您有幫助呢？如果還想對相關(guān)知識有進一步的了解或閱讀更多相關(guān)文章，請關(guān)注創(chuàng)新互聯(lián)行業(yè)資訊頻道，感謝您對創(chuàng)新互聯(lián)的支持。