[發明專利]一種基于符號執行驗證的智能合約漏洞檢測方法及裝置

在審

• 申請號: 202111243944.8
• 申請日: 2021-10-26
• 公開（公告）號: CN113688403A
• 公開（公告）日: 2021-11-23
• 發明（設計）人: 汪德嘉;王澤旭;宋超
• 申請（專利權）人: 江蘇通付盾科技有限公司
• 主分類號: G06F21/57
• 分類號: G06F21/57
• 代理公司: 北京弘權知識產權代理有限公司 11363
• 代理人: 逯長明;許偉群

本申請公開了一種基于符號執行驗證的智能合約漏洞檢測方法及裝置，包括獲取輸入初始值，所述輸入初始值包括符號值以及與所述符號值對應的、用于簡化約束條件的實際值；根據所述初始值或者經過路徑反求后的結果選擇將要執行的路徑并執行；當當前路徑執行到葉子節點時停止，根據執行結果生成所述當前路徑的約束條件；將約束條件反求得到路徑反求后的結果，所述結果對應下一個要執行的新路徑；當滿足第一預設規則后，停止路徑執行并生成包括所有執行路徑的執行樹；基于所述執行樹完成智能合約屬性驗證，得到驗證結果。本申請通過符號執行的方法對待檢測程序完成程序屬性驗證的工作，從而實現對代碼漏洞的精確檢測。

技術領域

本申請涉及智能合約技術領域，尤其涉及一種基于符號執行驗證的智能合約漏洞檢測方法及裝置。

背景技術

智能合約設計的初衷在于能夠自動、高效與公平地執行區塊鏈上的每一筆交易，在區塊鏈的日常活動中，智能合約扮演著較為重要的角色。隨著區塊鏈的應用場景日益豐富、功能不斷完善，智能合約的安全問題逐漸凸顯，智能合約的安全即為區塊鏈項目的命脈，因此智能合約的安全漏洞檢測工作尤為重要。

現有技術中，對于智能合約漏洞檢測技術主要包括符號執行、模糊測試、形式化驗證、程序分析技術及污點分析等手段。其中，符號執行相比于其他技術更適用于對程序進行精確全面的分析。符號執行的主要思想為：把程序執行中的不確定的輸入值轉換為符號值，從而推動程序執行分析、完成屬性驗證等工作，保證了檢測結果具有較好的真實性與可靠性。

目前常用的用于檢測智能合約漏洞的裝置有Oyente，Oyente以智能合約字節碼作為輸入，包含四個核心組件：控制流圖生成器 (CFG Builder)、探索器 (Explorer)、分析器(Core Analysis)和驗證器(Validator)。控制流圖生成器對合約進行預分析，為合約構建基本的控制流圖，以基本塊為節點，跳轉關系為邊。然而部分跳轉關系并不能由控制流圖生成器完全確定。因此，探索器會對智能合約進行符號執行，并在執行過程中將這些信息補齊。探索器承擔著收集合約信息的重要責任，它本質上是一個循環，依次執行合約控制流圖中各個基本塊的代碼。它利用Z3求解器對合約中的條件跳轉進行求解，探索器根據求解結果決定對哪個分支進行分析，當條件跳轉的兩個分支條件都有解時， 兩個分支都會被探索。分析器是 Oyente 的另一個重要組件，用于根據探索器收集的信息，識別合約漏洞。驗證器，用于過濾分析器所產生的誤報。

然而，Oyente 僅是一個字節碼層面的合約漏洞挖掘工具，在符號執行的過程中對程序控制流圖進行動態探索，并通過路徑約束、變量來源等信息對合約漏洞進行檢測。但是，Oyente的部分檢測方案并不完善，在實際的智能合約檢測工作中會報出大量假陽性誤報，涉及的漏洞也不夠全面，僅實現了條件競爭、時間戳依賴、未校驗返回值以及重入漏洞四種合約漏洞的檢測方案。同時，該工具也缺乏相關開發人員的維護與更新，已不能滿足目前智能合約發展對安全漏洞檢測的需求工作。

發明內容

本申請提供了一種基于符號執行驗證的智能合約漏洞檢測方法及裝置，以解決現有技術中執行智能合約漏洞檢測時精度低、準確度低等問題。

第一方面，本申請提供了一種基于符號執行驗證的智能合約漏洞檢測方法，所述方法包括：

獲取輸入初始值，所述輸入初始值包括符號值以及與所述符號值對應的、用于簡化約束條件的實際值；

根據所述初始值或者經過路徑反求后的結果選擇將要執行的路徑并執行；

當當前路徑執行到葉子節點時停止，根據執行結果生成所述當前路徑的約束條件；

將約束條件反求得到路徑反求后的結果，所述結果對應下一個要執行的新路徑；

當滿足第一預設規則后，停止路徑執行并生成包括所有執行路徑的執行樹；

基于所述執行樹完成智能合約屬性驗證，得到驗證結果。

在一些實施例中，所述第一預設規則包括：