[發(fā)明專利]一種高度自動化的智能合約形式化驗證系統(tǒng)及方法

有效

• 申請?zhí)枺?/td>: 201810790872.0
• 申請日: 2018-07-18
• 公開（公告）號: CN108985073B
• 公開（公告）日: 2020-05-22
• 發(fā)明（設(shè)計）人: 楊霞
• 申請（專利權(quán)）人: 成都鏈安科技有限公司
• 主分類號: G06F21/57
• 分類號: G06F21/57;G06Q40/04
• 代理公司: 成都四合天行知識產(chǎn)權(quán)代理有限公司 51274
• 代理人: 王記明

1.一種高度自動化的智能合約形式化驗證系統(tǒng)，其特征在于，包括形式化驗證規(guī)則模型庫、智能合約編譯器、自然語言解釋器、自動化建模工具、語法樹解析器、定理生成器、定理證明器、智能合約漏洞檢測文檔生成器，其中，

所述智能合約編譯器用于接收區(qū)塊鏈智能合約源代碼，將區(qū)塊鏈智能合約源代碼編譯得到源碼和字節(jié)碼，再將得到的源碼和字節(jié)碼輸出至自動化建模工具進行建模；

所述自然語言解釋器用于接收智能合約功能需求描述文檔，將智能合約功能需求描述文檔轉(zhuǎn)化為使用非自然語言描述的智能合約功能需求規(guī)范文檔，并將智能合約功能需求規(guī)范文檔傳輸至定理生成器；

所述自動化建模工具用于接收智能合約編譯器輸出的源碼和字節(jié)碼，并依賴于形式化驗證規(guī)則模型庫對源碼和字節(jié)碼進行自動化建模，對源碼進行自動化建模得到智能合約代碼抽象語法樹文檔和源碼智能合約模型文檔；對字節(jié)碼進行自動化建模得到字節(jié)碼智能合約模型文檔；

所述語法樹解析器用于接收自動化建模工具中的智能合約代碼抽象語法樹文檔，并解析出智能合約代碼中的常量、變量、繼承關(guān)系、函數(shù)限定符，并為其分配內(nèi)存地址，生成語法樹解析文檔并輸出至定理生成器；

所述定理生成器用于接收自動化建模工具輸出的源碼智能合約模型文檔以及自然語言解釋器輸出的非自然語言描述的智能合約功能需求規(guī)范文檔以及語法樹解析器輸出的語法樹解析文檔，同時依賴于形式化驗證規(guī)則模型庫對非自然語言進行非形式化描述得到相關(guān)定理，生成智能合約定理文檔并將其輸出至定理證明器；

所述定理證明器用于接收定理生成器輸出的智能合約定理文檔，并對其進行形式化證明得到驗證結(jié)果，并將驗證結(jié)果傳輸至智能合約漏洞檢測文檔生成器；

所述智能合約漏洞檢測文檔生成器用于接收定理證明器輸出的驗證結(jié)果，并生成智能合約漏洞檢測文檔。

2.根據(jù)權(quán)利要求1所述的一種高度自動化的智能合約形式化驗證系統(tǒng)，其特征在于，所述自動化建模工具包括源碼建模器和字節(jié)碼建模器，所述源碼建模器用于對合約源代碼進行自動化建模并輸出智能合約代碼抽象語法樹文檔和源碼智能合約模型文檔；所述字節(jié)碼建模器用于對字節(jié)碼進行自動化建模并輸出字節(jié)碼智能合約模型文檔。

3.根據(jù)權(quán)利要求2所述的一種高度自動化的智能合約形式化驗證系統(tǒng)，其特征在于，所述源碼建模器包括詞法分析器、語法分析器、語法樹對接器、源碼形式化語言推導(dǎo)器，其中，

所述詞法分析器用于接收智能合約源代碼，并依賴于智能合約語言文法規(guī)則庫中存儲的不同編程語言的文法規(guī)則，對輸入的字符串進行掃描與分解，識別合法的詞素，產(chǎn)生特定規(guī)則的詞法單元序列并將詞法單元序列輸出至語法分析器；

所述語法分析器用于接收詞法分析器輸出的詞法單元序列以及用于存儲簡單優(yōu)先表，并將詞法單元序列與簡單優(yōu)先表進行比較判斷，得出詞法單元序列所屬的編程語言種類，并結(jié)合智能合約語言文法規(guī)則庫中對應(yīng)的文法規(guī)則，將詞法單元序列中的詞素生成抽象語法樹，并將抽象語法樹輸出至語法樹對接器，同時輸出智能合約代碼抽象語法樹文檔；

所述語法樹對接器用于接收語法分析器輸出的抽象語法樹以及用于存儲對接字典表，利用對接字典表將抽象語法樹中的內(nèi)容一一對應(yīng)替換生成形式化語言語法樹，并將形式化語言語法樹輸出至源碼形式化語言推導(dǎo)器；

所述源碼形式化語言推導(dǎo)器用于接收形式化語言語法樹并結(jié)合形式化語言文法規(guī)則庫將語法樹對接器中輸出的形式化語言語法樹翻譯成對應(yīng)的形式化語言代碼，整理得到源碼智能合約模型文檔。

4.根據(jù)權(quán)利要求2所述的一種高度自動化的智能合約形式化驗證系統(tǒng)，其特征在于，所述字節(jié)碼建模器包括字節(jié)碼形式化語言推導(dǎo)器，其中，

所述字節(jié)碼形式化語言推導(dǎo)器用于接收智能合約字節(jié)碼，同時依賴于形式化語言文法規(guī)則庫以及虛擬機指令系統(tǒng)規(guī)則庫建立智能合約字節(jié)碼與對應(yīng)形式化語言操作碼的對接字典表，并結(jié)合對接字典表將智能合約字節(jié)碼一一替換成對應(yīng)的形式化語言操作碼的內(nèi)容，從而得到形式化語言代碼，并將形式化語言代碼整理得到字節(jié)碼智能合約模型文檔。