[發明專利]一種高度自動化的智能合約形式化驗證系統及方法

有效

• 申請號: 201810790872.0
• 申請日: 2018-07-18
• 公開（公告）號: CN108985073B
• 公開（公告）日: 2020-05-22
• 發明（設計）人: 楊霞
• 申請（專利權）人: 成都鏈安科技有限公司
• 主分類號: G06F21/57
• 分類號: G06F21/57;G06Q40/04
• 代理公司: 成都四合天行知識產權代理有限公司 51274
• 代理人: 王記明

本發明公開了一種高度自動化的智能合約形式化驗證系統及方法，包括：步驟001：將智能合約功能需求描述文檔轉換為使用非自然語言描述的智能合約功能需求規范文檔，智能合約功能需求規范文檔內容包括目標合約功能規范描述和安全屬性描述；步驟002：建立形式化驗證規則模型庫。步驟003：通過自動化建模工具對合約源代碼和/或字節碼進行自動化建模；步驟004：對步驟003生成的抽象語法樹解析，為代碼中常量、變量分配內存地址；步驟005：形式化證明。本發明適應于多種的高級編程語言編寫的程序代碼，也適應多種形式化語言，同時提供源代碼建模和字節碼建模兩種自動化建模方式，能夠針對用戶的不同建模需求進行建模，進一步提高驗證效率。

技術領域

本發明涉及區塊鏈智能合約安全領域和形式化驗證方法，具體涉及一種高度自動化的智能合約形式化驗證系統及方法。

背景技術

區塊鏈是分布式數據存儲、點對點傳輸、共識機制、加密算法等計算機技術的新型應用模式。使用去中心化共識機制去維護一個完整的、分布式的、不可篡改的賬本數據庫的技術，它能夠讓區塊鏈中的參與者在無需建立信任關系的前提下實現一個統一的賬本系統。一個智能合約是一套以數字形式定義的承諾，包括合約參與方可以在上面執行這些承諾的協議。在區塊鏈技術背景下，智能合約是指運行在區塊鏈上，能夠執行某些功能的程序代碼。將智能合約以數字化的形式寫入區塊鏈中，由區塊鏈技術的特性保障存儲、讀取、執行整個過程透明可追蹤、不可篡改。同時，由區塊鏈自帶的共識算法構建出一套狀態機系統，使得智能合約能夠高效地運行。

由于區塊鏈不可篡改特性，一旦因為程序自身設計的問題，導致智能合約的安全漏洞，或將產生不可逆轉的重大損失。形式化驗證方法是使用數學的公式、定理和系統來驗證一個系統的功能正確性和安全屬性，與傳統檢測方法相比，形式化驗證方法可以發現目標與系統描述的不一致性問題，因此使用形式化驗證方法來驗證智能合約，可以有效的檢驗智能合約的安全性，檢測合約是否存在漏洞。但是常見的形式化驗證方法存在著下列問題：

1、對程序員要求極高。不僅要求程序員對所驗證代碼的編程語言熟悉，還要求程序員具有較高的數學基礎。

2、現有技術主要依賴于手工驗證，工作量大，自動化程度低，因此時間成本太高，建立的模型的正確性無法保障，需求一旦變化，前面的工作都要重新開始，且模型的正確性依賴于程序員的建模經驗和技術程度。

3、閱讀性差，不利于程序員之間對接工作。常見形式化驗證方法所建立的模型沒有統一規范，僅與程序員習慣及素質有關，不方便代碼對接。

4、目前常見的驗證方法，大都是驗證合理輸入得到合理結果，對于不合理輸入的結果往往忽略，這種做法存在很大的安全隱患。如果不合理輸入仍能得到符合函數功能規范的結果，說明該智能合約代碼存在漏洞。

發明內容

本發明為了解決上述技術問題，目的在于提供一種高度自動化的智能合約形式化驗證系統及方法，這種方法建立形式化驗證規則模型庫，并對智能合約源代碼和字節碼進行自動化建模，再由程序員針對不同模型和形式化驗證規則模型庫以及智能合約功能需求描述文檔，分別描述定理并證明。通過將自動化建模和人工驗證相結合，能夠減少時間成本，縮短驗證周期，提高效率，同時自動化建模能夠統一模型規范，減少驗證模型對程序員個人素質的依賴程度，保證正確性。

本發明通過下述技術方案實現：

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

形式化驗證規則模型庫用于支持自動化建模工具、定理生成器的工作；形式化驗證規則模型庫包括區塊鏈平臺模型庫和智能合約安全屬性模型庫；

智能合約安全屬性模型庫是通過對智能合約常見安全漏洞形式化描述建立的安全屬性庫；