[發明專利]基于邊界模型檢測技術的微內核操作系統接口的形式化驗證方法

有效

• 申請號: 202010315705.8
• 申請日: 2020-04-21
• 公開（公告）號: CN111679964B
• 公開（公告）日: 2022-07-26
• 發明（設計）人: 郭建;周城程;蒲戈光;何積豐
• 申請（專利權）人: 華東師范大學;上海工業控制安全創新科技有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 上海德禾翰通律師事務所 31319
• 代理人: 陳艷娟

本發明公開了一種基于邊界模型檢測技術的微內核操作系統接口的形式化驗證方法。首先從微內核操作系統規范中提取微內核API的性質，把性質抽象為一階邏輯公式；并將程序要滿足的基本性質從通用基本性質庫提取其一階邏輯公式；微內核操作系統待驗證的API從源代碼中提取出來，包括相關的數據結構和內部調用的函數；將提取的微內核API分別和微內核API性質、通用性質進行合并獲得含有API性質的微內核API、含有通用性質的微內核API；分別對兩個API程序進行抽象建模，獲得一階邏輯公式；最后應用SMT求解器驗證，如果驗證失敗，則根據驗證公式給出的錯誤提示修改微內核API代碼并重新驗證，直到驗證通過，說明該接口程序滿足性質。

技術領域

本發明涉及微內核操作系統領域，具體涉及一種基于邊界模型檢測技術的微內核操作系統接口的形式化驗證方法。

背景技術

隨著計算機軟硬件的快速發展，計算機軟件的規模越來越大，復雜度越來越高。操作系統作為計算的一個系統性軟件，在計算機整個運行過程中起著承上啟下的核心作用。而在安全領域，操作系統的安全性起著至關重要的作用，因此操作系統的可信性變得極為重要。所以，為了確保操作系統的正確性與可靠性，在開發之前要制定操作系統規范策略，在整個操作系統設計完成后，投入實現之前需要對其進行測試，以確保操作系統的功能正確性和實現與編寫的規范的一致性。由于有些對安全要求較高的領域對操作系統的正確性有著嚴格的要求，僅僅對操作系統做測試是不能夠保證在所有的運行條件下都是正確的，所以在測試之外需要增加形式化的驗證來確保所有的條件下都是可靠的。

近年來，隨著計算機計算能力的不斷發展，以及可滿足理論的不斷發展，可滿足求解器被廣泛地應用于各個領域，例如大數據、人工智能、云計算、程序驗證等。而可滿足求解器(SAT求解器)的計算能力有了很大的提高，能處理含有成百上千個變量、數百萬個子句的布爾公式。

發明內容

本發明提出的對微內核操作系統形式化的驗證方法。首先將微內核操作系統中待驗證的接口從完整的代碼中提取出來，包括與目標接口相關的數據結構和內部調用的函數；獲得接口程序的控制流圖；根據控制流圖，對程序進行建模并展開循環，獲得用一階邏輯公式表達的路徑公式；根據微內核操作系統的規范提取其性質并編寫一階邏輯公式；根據微內核操作系統接口得到的布爾公式和提取微內核操作系統性質得到的布爾公式，應用SAT求解器進行驗證；如果驗證失敗，則根據驗證公式給出的錯誤提示修改微內核操作系統接口代碼并重新驗證，直到驗證通過，說明該接口程序滿足性質。本發明應用到基于事件總線的微內核操作系統的時間片管理接口、線程管理接口、IPC接口的驗證中，以提高其安全性、可靠性。

本發明提出了一種基于邊界模型檢測技術的微內核操作系統接口的形式化驗證方法，包括：

步驟一：在微內核操作系統的自然語言規范中提取微內核API的性質，并把所述性質抽象為一階邏輯公式；

步驟二：從通用基本性質庫中提取程序要滿足的基本性質的一階邏輯公式；

步驟三：在微內核操作系統源代碼中提取待驗證的API；

步驟四：將提取的微內核API分別和對應的微內核API性質、通用性質進行合并，獲得含有API性質的微內核API、含有通用性質的微內核API；

步驟五：分別對含有API性質的微內核API和含有通用性質的微內核API進行抽象建模，獲得一階邏輯公式；

步驟六：將所述一階邏輯公式作為SMT求解器的輸入，判斷待檢測API是否滿足性質；如果待檢測API不滿足性質，則修改該API的代碼，并重新建模生成一階邏輯公式，再次輸入SMT求解器；如果所有待檢測接口均已滿足性質，則該微內核API滿足微內核操作系統規范和通用程序性質。

本發明提出的基于邊界模型檢測技術的微內核操作系統接口的形式化驗證方法中，所述步驟一包括以下步驟：