[發(fā)明專利]一種基于符號執(zhí)行對智能合約功能屬性進行形式化驗證的方法及系統(tǒng)

在審

• 申請?zhí)枺?/td>: 202210047615.4
• 申請日: 2022-01-17
• 公開（公告）號: CN114510414A
• 公開（公告）日: 2022-05-17
• 發(fā)明（設(shè)計）人: 文偉平;肖遙;劉宇航;胡葉舟;劉軍杰;方瑩
• 申請（專利權(quán)）人: 北京大學(xué)
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京萬象新悅知識產(chǎn)權(quán)代理有限公司 11360
• 代理人: 李稚婷

本發(fā)明公開了一種基于符號執(zhí)行對智能合約功能屬性進行形式化驗證的方法及系統(tǒng)，通過合約屬性解析將自定義功能屬性的證明轉(zhuǎn)化為可達性驗證，提供一種利用符號執(zhí)行自動化進行形式化驗證的新途徑，對屬性斷言進行等價轉(zhuǎn)換嘗試進行歸納證明能對可歸納性屬性達到快速驗證的效果，有效提高驗證速度，對于不滿足的功能屬性能夠構(gòu)造對應(yīng)的反例提高可用性，另外，將符號執(zhí)行與抽象驗證分離開，能夠避免不必要的抽象降低符號執(zhí)行的效率，保證了符號執(zhí)行收斂的速度。本發(fā)明可以自動化對智能合約功能屬性進行形式化驗證并輸出不符合的屬性的反例，并通過對合約屬性的預(yù)處理，可歸納性驗證和迭代不動點法相結(jié)合有效提高符號執(zhí)行可達性驗證的效率。

技術(shù)領(lǐng)域

本發(fā)明涉及計算機安全技術(shù)領(lǐng)域，尤其涉及一種基于符號執(zhí)行對智能合約功能屬性進行形式化驗證的方法及系統(tǒng)。

背景技術(shù)

智能合約是一種無需中介、自我驗證、自動執(zhí)行合約條款的計算機交易協(xié)議。區(qū)塊鏈技術(shù)去中心化和數(shù)據(jù)防篡改等特性，解決了智能合約的信任問題，因此使得智能合約更適合在區(qū)塊鏈上進行實現(xiàn)。智能合約作為一種能自動執(zhí)行合約條款的計算機程序，對于正確性及其他屬性具有較高要求，需要盡量避免語法和語義錯誤，以保證用戶的財產(chǎn)安全。目前的審計實踐通常檢測兩類問題：1.通用安全錯誤，例如重入和溢出；2.自定義功能屬性，例如“存款總額永遠不會超過合約的余額”和“代幣總額不會發(fā)生變化”。前者主要通過自動化測試的方法檢測，后者則需要形式化方法來驗證。

形式化方法的本質(zhì)是基于數(shù)學(xué)的方法來描述目標(biāo)軟件系統(tǒng)屬性的一種技術(shù)，適用于計算機軟硬件系統(tǒng)的規(guī)范、開發(fā)和驗證。形式化驗證是使用基于數(shù)學(xué)變換的靜態(tài)分析方法來確定程序規(guī)范和代碼行為，如從協(xié)議規(guī)約出發(fā)驗證程序的安全屬性等，其是目前安全級別最高的一種驗證方法。由于缺少自動化驗證的工具，當(dāng)前的驗證工作需要使用重量級的交互式定理證明程序進行，這些需要大量的人工和專業(yè)知識，使審計過程既昂貴又耗時，導(dǎo)致開發(fā)人員和審計社區(qū)很少采用，迄今為止只有少數(shù)智能合約項目得到了正式驗證。

發(fā)明內(nèi)容

為了克服上述現(xiàn)有技術(shù)的不足，本發(fā)明提供一種基于符號執(zhí)行對智能合約功能屬性進行形式化驗證的方法及系統(tǒng)，將自定義功能屬性形式化為屬性斷言之后，可將自定義功能屬性的證明轉(zhuǎn)化為可達性檢查，進而通過符號執(zhí)行精確地驗證，通過自動化能有效地減輕審計人員的工作量，并提升審計結(jié)果的精確度。

本發(fā)明提供的技術(shù)方案是：一種基于符號執(zhí)行對智能合約功能屬性進行形式化驗證的方法，首先需要由合約審計者將自定義功能屬性形式化為屬性斷言(屬性斷言采用與solidity相同的語法形式，并額外添加了時間屬性運算符如Once、Always)，然后抽象該屬性斷言通過符號執(zhí)行嘗試可歸納性驗證，若其具有可歸納性，則可直接證明；如果其不具有可歸納性，則通過深度的符號執(zhí)行不斷擴充可達抽象狀態(tài)集，迭代計算可達抽象狀態(tài)的不動點，最終從不動點去嘗試推導(dǎo)屬性斷言，若均能成功推導(dǎo)，則已證明了該屬性斷言，否則，嘗試構(gòu)造反例輸出。該技術(shù)方案主要包括四個階段：預(yù)處理階段、歸納證明階段、迭代不動點階段、屬性驗證階段。其中：

預(yù)處理階段執(zhí)行如下步驟：

步驟1，接收一個或多個合約C₁，C₂…C_m以及輸入一系列自定義屬性斷言φ₁，φ₂…φ_n，將屬性斷言進行等價變換，變換為□φ₁’，□φ₂’…□φ_n’的形式，其中□φ_i’表示屬性斷言φ_i’恒成立，m、n、i代表自然數(shù)。

步驟2，將輸入的一系列合約合并為一個合約C₀。

步驟3，根據(jù)屬性斷言在合約相應(yīng)的位置添加新屬性變量，插入監(jiān)測代碼，得到插樁合約C_φ，其包含函數(shù){f₁，f₂…f_k}，其中k代表自然數(shù)。