[發明專利]形式化驗證的系統和方法

在審

• 申請號: 201880087842.1
• 申請日: 2018-11-28
• 公開（公告）號: CN112119423A
• 公開（公告）日: 2020-12-22
• 發明（設計）人: 邵中;顧榮輝;威廉·舍貝里;金志應;熱雷米·凱尼格
• 申請（專利權）人: 耶魯大學
• 主分類號: G06Q50/18
• 分類號: G06Q50/18
• 代理公司: 北京集佳知識產權代理有限公司 11227
• 代理人: 唐京橋;楊林森

用于程序的形式化驗證的系統和方法。系統和方法提供了用于并發的新的基于博弈論策略的組合語義模型，用于組合多線程和多核的并發層的一組形式化鏈接定理，以及支持認證的線程安全編譯和鏈接的編譯器。覆蓋接口的驗證可以包括確定用于在底層接口上運行的原語操作的中間策略，以及通過應用垂直和水平組合規則將中間策略細化為在覆蓋接口上運行的策略。然后，可以根據并行組合規則將細化的策略與在覆蓋接口上運行的兼容策略組合。當由每個策略施加的依賴條件滿足由其他策略提供的保證時，策略可以是兼容的。形式化驗證的系統和方法可以應用于智能合約的形式化驗證。

相關申請的交叉引用

本申請要求于2017年11月28日提交的法國專利申請第17/61318號的優先權，其全部內容通過引用并入本文中。

聯邦政府資助的研究

本發明是在國家科學基金會授予的1521523以及美國空軍科學研究辦公室授予的FA8750-12-2-0293的政府支持下作出的。政府對發明有一定的權利。

背景技術

抽象層是構建大規模并發軟件和硬件時使用的關鍵技術。由于多線程編程和多核硬件的普遍性，并發抽象層普遍存在于現代計算機系統。使用抽象層來隱藏實現細節(例如，細粒度同步)并且減少處于不同抽象級的部件之間的復雜依賴性。盡管并發抽象層具有明顯的重要性，但是并沒有對并發抽象層進行形式上的處理。這嚴重限制了基于層的技術的適用性，并且使得難以跨多個并發層擴展驗證。

分布式分類賬提供了并發執行的另一示例。這樣的系統(例如基于區塊鏈的數據庫)使得能夠以安全且透明的方式對記錄進行分散管理。例如，區塊鏈可以用作用于記錄各方之間的交易的開放式分類賬，并且可以由節點網絡維護。這些節點可以各自維護區塊鏈的本地副本，并且可以共同執行協議以確保在新交易被記錄時本地副本彼此保持一致。區塊鏈技術可以適合于期望高度安全性的各種應用，例如，身份管理、交易處理、醫療記錄保持、物流的可追溯性等。然而，由于節點之間執行的并發性以及整個分布式分類賬與實現分布式分類賬的節點的硬件之間的多個抽象級，因此使區塊鏈技術適合于這樣的高價值應用的相同的特性還使得難以對這樣的應用進行形式化驗證。

發明內容

實施方式可以用于構建認證的并發抽象層。這些實施方式可以包括應用細粒度并發層演算(calculus)的用于并發C和匯編的程序驗證器、認證的鏈接工具和線程安全驗證的C編譯器。實施方式還可以包括將這些工具應用于智能合約的驗證。

實施方式可以包括一種用于覆蓋接口(overlay interface)的形式化驗證的方法。方法可以包括將覆蓋接口建模為在底層接口上構建的多個層實現，底層接口由多個線程集參數化。方法還可以包括通過執行以下操作中的至少之一來驗證覆蓋接口。

第一操作可以驗證到在底層接口上構建的程序的映射實現到策略的映射。在底層接口上運行共享原語的語義可以由策略來模擬。

第二操作可以驗證第一程序模塊根據第一模擬關系實現覆蓋接口。在底層接口上構建的第二程序模塊可以根據第二模擬關系來實現第一中間接口。在第一中間接口上構建的第三程序模塊可以根據第三模擬關系來實現覆蓋接口。第一程序模塊可以是第二程序模塊和第三程序模塊的組合，并且第一模擬關系可以是第二模擬關系和第三模擬關系的組合。

第三操作可以驗證第四程序模塊根據第四模擬關系實現覆蓋接口。在底層接口上構建的第五程序模塊可以根據第四模擬關系來實現第二中間接口。在底層接口上構建的第六程序模塊可以根據第四模擬關系來實現第三中間接口。第四程序模塊可以是第五程序模塊和第六程序模塊的組合，并且覆蓋接口可以是第二中間接口和第三中間接口的組合。

第四操作可以驗證在第四中間接口上構建的第七程序模塊根據第五模擬關系實現第五中間接口。第四中間接口可以由底層接口根據第六模擬關系來模擬。第七程序模塊可以根據第七模擬關系來實現覆蓋接口。覆蓋接口可以由第五中間接口根據第八模擬關系來模擬。第五模擬關系可以是第六模擬關系、第七模擬關系和第八模擬關系的組合。