[發明專利]基于類型檢測的智能合約信息流完整性驗證方法及系統

在審

• 申請號: 202110293711.2
• 申請日: 2021-03-19
• 公開（公告）號: CN113051624A
• 公開（公告）日: 2021-06-29
• 發明（設計）人: 胡鐔文;莊毅;林尚威;章甫源;闞雙龍;曹子寧
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F21/64
• 分類號: G06F21/64
• 代理公司: 南京理工大學專利中心 32203
• 代理人: 朱炳斐

1.一種基于類型檢測的智能合約信息流完整性驗證方法，其特征在于，所述方法包括以下步驟：

步驟1，為智能合約編程語言構建形式化語法、語義；

步驟2，構建智能合約的安全類型系統STC，用于檢測智能合約信息流完整性；

步驟3，構建基于智能合約類型系統STC的類型驗證器STV，自動為智能合約的狀態變量尋找最優安全類型分配，即狀態變量中被分配為可信的數量最多，使得智能合約滿足信息流完整性。

2.根據權利要求1所述的基于類型檢測的智能合約信息流完整性驗證方法，其特征在于，步驟1中所述構建形式化語法，具體包括：

(1)將智能合約編程語言抽象為短語，這些短語為表達式或語句；

智能合約的表達式包括8種類型：值v、全局變量g、狀態變量id、表達式組智能合約實例表達式NewExp、操作表達式OperatorExp、智能合約數組或映射表達式IndexAccess，和自定義類型的數據字段訪問表達式MemberAccess；智能合約表達式的語法定義如下：

NewExp：：＝new id_c()

OperatorExp：：＝op_u exp|exp₁ op_b exp₂

IndexAccess：：＝exp[]|exp₁[exp₂]

MemberAccess：：＝exp.id|exp.IndexAccess

其中，new為實例化合約的標識符，op_u為一元操作符，op_b為二元操作符，id_c為合約名稱變量；

智能合約的語句包括3種類型：簡單語句SimpleStmt、語句塊BlockStmt和語句序列；其中，SimpleStmt表示單個基本語句，包括函數調用FunctionCall、普通賦值語句exp₁ op＝exp₂和接收函數調用返回值的賦值語句exp op＝FunctionCall；BlockStmt表示一個語句塊，包括分支結構語句if(exp)then stmt₁ else stmt₂、重復語句while(exp)stmt、變量定義語句letvar id op＝exp in stmt、需求語句require(exp)in stmt和一個花括號語句塊{stmt}；函數調用FunctionCall包括三種類型：內部函數調用外部函數調用和底層函數調用底層函數調用包括三類：call底層函數調用delegatecall底層函數調用和callcode底層函數調用智能合約語句的語法定義如下：

(Statements)stmt：：＝SimpleStmt；|BlockStmt|stmt₁ stmt₂

SimpleStmt：：＝FunctionCall|exp₁op＝exp₂|exp op＝FunctionCall

LowLevelCall：：＝call|delegatecall|callcode

BlockStmt：：＝if(exp)then stmt₁ else stmt₂|while(exp)stmt|letvar id op＝expin stmt|require(exp)in stmt|{stmt}

其中，id_f為函數名稱變量，op＝為賦值操作符；

(2)在編寫的智能合約中，函數類型分為普通函數normal function、構造函數constructor和回退函數fallback function；一個智能合約有且只有一個未命名的fallback function，其不能有輸入或輸出參數，并且必須有external可見性；其中，普通函數normal function的語法定義如下：

式中，id_c表示智能合約的名稱，id_f表示函數的名稱，表示函數的輸入參數，表示函數的輸出參數，Q表示函數的可見性；

構造函數constructor與普通函數normal function的區別在于：id_f被關鍵字constructor替換；

回退函數fallback function的語法定義如下：

fun_f：：＝id_c.function()external{stmt}

(3)智能合約包括狀態變量聲明和函數聲明，其語法的定義如下：

(Contracts)ctr：：＝contract id{ctrPart}

ctrPart：：＝letvar id op＝exp|fun|ctrPart ctrPart

步驟1中所述構建形式化語義具體包括：

(1)智能合約的表達式的操作語義形式為聲明表達式exp在求值環境μ中計算為值v；同時使用dom(μ)和ran(μ)分別表示μ的定義域和值域；并假設按合約名索引的表CA存儲NewExp的地址，以模擬隨機合約地址；

(2)智能合約的語句的操作語義形式為其中μ，μ′分別為執行語句stmt之前和之后的求值環境，S表示stmt所屬的調用方智能合約；同時假設函數定義存儲在按函數名索引的表FD中。