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

在審

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

1.一種基于符號執(zhí)行對智能合約功能屬性進(jìn)行形式化驗(yàn)證的方法，首先將自定義功能屬性形式化為屬性斷言，然后抽象該屬性斷言通過符號執(zhí)行嘗試可歸納性驗(yàn)證，若其具有可歸納性，則可直接證明；若其不具有可歸納性，則通過深度的符號執(zhí)行不斷擴(kuò)充可達(dá)抽象狀態(tài)集，迭代計(jì)算可達(dá)抽象狀態(tài)的不動點(diǎn)，最終從不動點(diǎn)去嘗試推導(dǎo)屬性斷言，若均能成功推導(dǎo)，則已證明了該屬性斷言，否則，嘗試構(gòu)造反例輸出；具體包括如下步驟：

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

2)將輸入的一系列合約合并為一個(gè)合約C₀；

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

4)根據(jù)插樁合約C_φ及等價(jià)變換后的屬性斷言□φ₁’，□φ₂’…□φ_n’解析所需的抽象狀態(tài)α；

5)對于一條需要驗(yàn)證的屬性斷言φ’，通過init來構(gòu)建初始化的抽象狀態(tài)α_init，檢查在α_init下屬性斷言是否成立，若成立則進(jìn)入步驟6，不成立則插樁合約C_φ不滿足屬性斷言φ’，即證明了輸入合約C₁，C₂…C_m不滿足屬性斷言φ；

6)將初始化的抽象狀態(tài)α_init轉(zhuǎn)換為初始符號狀態(tài)集S₀{s₁₀，s₂₀…s_m0}；

7)以初始符號狀態(tài)集中各狀態(tài)為初始狀態(tài)，執(zhí)行函數(shù)f_i，得到符號狀態(tài)集S_i{s_1i，s_2i…s_mi}，并轉(zhuǎn)化為抽象狀態(tài)集A_i{α_1i，α_2i…α_mi}；

8)若對于某屬性斷言φ’生成的初始符號狀態(tài)集S₀分別執(zhí)行{f₁，f₂…f_k}得到的符號狀態(tài)集S_i及其對應(yīng)的抽象狀態(tài)集A_i，若φ’均仍然成立，則φ’是可歸納證明屬性斷言且φ’恒成立，即證明了輸入合約C₁，C₂…C_m滿足屬性斷言φ；若不成立，則進(jìn)入步驟9；

9)根據(jù)步驟5)中構(gòu)建的初始化的抽象狀態(tài)α_init，初始化可達(dá)抽象狀態(tài)集合reach(C_φ)₀＝{α_init}；

10)以符號方式執(zhí)行一次while循環(huán)，調(diào)用f_i，并在交易結(jié)束后計(jì)算精確的符號狀態(tài)s，s實(shí)際上是不同路徑約束p1∪p2∪…∪p_k的所有可能，包括s₁，s₂…s_k；

11)根據(jù)精確的符號狀態(tài)s₁，s₂…s_k計(jì)算出抽象狀態(tài)α₁，α₂…α_m，由于不同的符號狀態(tài)可能得到相同的抽象狀態(tài)，故有k≥m；

12)將抽象狀態(tài)α₁，α₂…α_m加入可達(dá)抽象狀態(tài)集合reach(C_φ)₀得到可達(dá)抽象狀態(tài)集合reach(C_φ)₁，重復(fù)步驟10)和11)；由于抽象狀態(tài)域是有限的，故最終reach(C_φ)一定會達(dá)到不動點(diǎn)reach(C_φ)_i+1＝reach(C_φ)_i；

13)根據(jù)可達(dá)抽象狀態(tài)集不定點(diǎn)reach(C_φ)_fix驗(yàn)證是否滿足屬性斷言φ’，若滿足則證明此合約C_φ滿足屬性斷言φ’，等價(jià)于證明了輸入合約C₁，C₂…C_m滿足屬性斷言φ，若不滿足則進(jìn)入步驟14)；

14)嘗試根據(jù)該抽象狀態(tài)對應(yīng)的符號狀態(tài)回查已記錄的符號執(zhí)行的路徑信息，嘗試構(gòu)建一個(gè)反例{(user,func,args)₁，(user,func,args)₂…(user,func,args)_n}并輸出，證明了輸入合約C₁，C₂…C_m不滿足屬性斷言φ。