[發明專利]一種智能合約驗證方法、計算機存儲介質

有效

• 申請號: 202011572924.0
• 申請日: 2020-12-24
• 公開（公告）號: CN112581140B
• 公開（公告）日: 2022-07-29
• 發明（設計）人: 不公告發明人
• 申請（專利權）人: 西安深信科創信息技術有限公司
• 主分類號: G06Q20/40
• 分類號: G06Q20/40;G06Q40/04
• 代理公司: 西安嘉思特知識產權代理事務所(普通合伙) 61230
• 代理人: 王海棟

本發明公開了一種智能合約驗證方法、計算機存儲介質，該智能合約驗證方法包括：步驟1、根據智能合約得到控制流圖，所述控制流圖包括標記有初始標記的節點和若干所述節點之間的邊，且所述節點為含有斷言的節點時，所述節點還標記有斷言，其中，所述節點包括非循環節點和循環節點；步驟2、基于預設順序，根據所述節點的類型得到每個所述節點的不變量；步驟3、根據所述節點的不變量的斷言隱含結果得到驗證結果。本發明的驗證方法可以驗證智能合約的正確性。另外，本發明的驗證方法對智能合約，適用面更廣。

技術領域

本發明屬于智能合約技術領域，具體涉及一種智能合約驗證方法、計算機存儲介質。

背景技術

區塊鏈是近年來發展迅速的研究領域，它首先由Satoshi Nakamoto在比特幣區塊鏈中提出概念，其基于多種技術，如區塊加密鏈、點對點通信、分布式系統等。比特幣網絡的出現使陌生人之間的金融交易在沒有第三方權威的參與下成為可能。后來，進一步出現了以太坊平臺，它是一個開源的有智能合約功能的公共區塊鏈平臺。此后，智能合約在金融機構和供應鏈等許多領域備受關注。

智能合約是一種計算機化的交易協議，它執行智能合約的條款以滿足用戶的要求，例如投票和交易。智能合約可以被看作是一個計算機程序，可以在區塊鏈上自定義交易執行邏輯，智能合約主要是用一種圖靈完備的編程語言編寫的，例如在以太坊中的solidity(一種契約型編程語言)。區塊鏈的不可更改特性使得智能合約一旦部署到區塊鏈上就無法更改。此外，solidity語言的一些語法特性跟其他計算及語言(如javascript)不太一樣，例如，變量的存儲性質和fallback(回退)函數的概念，即使一些開發者有使用傳統編程語言的經驗，也經常出錯。因此，由于代碼編寫不健壯，導致存在大量的攻擊，造成了巨大的經濟損失。例如，The DAO攻擊導致當時大約相當于6000萬美元的損失。攻擊者在splitDAO函數中發現了一個漏洞，他們可以通過在單筆交易的fallback函數隱式循環地一次又一次地重復的取走以太幣。因此在部署智能合約之前，驗證其正確性是至關重要的。

隨著對智能合約攻擊的不斷增加，人們開發了一些工具來分析智能合約的正確性。例如，Luu等人為Solidity智能合約開發了一個名為Oyente(智能合約分析工具)的符號執行引擎，該引擎系統地分析智能合約中的各個函數，以識別漏洞。Nikolic等人開發了一個名為MAIAN的符號分析器，它可以在智能合約執行期間進行符號執行分析，分析智能合約字節碼，以檢查智能合約中的“自殺”、“揮霍”和“貪婪”等漏洞。然而，上述工作的重點是測試智能合約，而不是驗證它們的正確性。例如，這些符號執行引擎通常在循環迭代或函數調用的數量上設置一個界限，目的是用生成的測試用例覆蓋那些有邊界的程序路徑。

目前，可用于驗證智能合約的現有方法包括Securify、Zeus、SOLC-verify和VerX。前三種方法將Solidity程序轉換為現有的中間語言(即Datalog、LLVM和Boogie)，并重用現有的驗證工具。這種方法有兩個局限性。首先，由于驗證設施不是為智能合約設計的，因此它們只能在智能合約的某些特定屬性上發揮有限的作用。其次，這些方法是基于抽象解釋的，而由于抽象方法和抽象域較粗略，往往會導致誤報。特別的，Securify無法驗證諸如溢出之類的數值屬性；Zeus誤報很嚴重，SOLC-verify路徑覆蓋率不高。VerX應用延遲謂詞抽象(基于符號執行和抽象)來驗證交易執行時智能合約的正確性。但是VerX不支持有fallback函數導致的隱含循環回調的情況，并且對于函數中的循環迭代需要設置邊界。

因此，提供一種能夠適用于智能合約，且能夠對智能合約準確進行驗證的方法成為了亟待解決的問題。

發明內容

為了解決現有技術中存在的上述問題，本發明提供了一種智能合約驗證方法、計算機存儲介質。本發明要解決的技術問題通過以下技術方案實現：

一種智能合約驗證方法，包括：