[發(fā)明專(zhuān)利]基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 202010315705.8
• 申請(qǐng)日: 2020-04-21
• 公開(kāi)（公告）號(hào): CN111679964B
• 公開(kāi)（公告）日: 2022-07-26
• 發(fā)明（設(shè)計(jì)）人: 郭建;周城程;蒲戈光;何積豐
• 申請(qǐng)（專(zhuān)利權(quán)）人: 華東師范大學(xué);上海工業(yè)控制安全創(chuàng)新科技有限公司
• 主分類(lèi)號(hào): G06F11/36
• 分類(lèi)號(hào): G06F11/36
• 代理公司: 上海德禾翰通律師事務(wù)所 31319
• 代理人: 陳艷娟

1.一種基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法，其特征在于，包括以下步驟：

步驟一：在微內(nèi)核操作系統(tǒng)的自然語(yǔ)言規(guī)范中提取微內(nèi)核API的性質(zhì)，并把所述性質(zhì)抽象為一階邏輯公式；

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

步驟三：在微內(nèi)核操作系統(tǒng)源代碼中提取待驗(yàn)證的微內(nèi)核API；

步驟四：將提取的微內(nèi)核API分別和對(duì)應(yīng)的微內(nèi)核API性質(zhì)、通用性質(zhì)進(jìn)行合并，獲得含有API性質(zhì)的微內(nèi)核API、含有通用性質(zhì)的微內(nèi)核API；

步驟五：分別對(duì)含有API性質(zhì)的微內(nèi)核API和含有通用性質(zhì)的微內(nèi)核API進(jìn)行抽象建模，獲得一階邏輯公式；

步驟六：將所述一階邏輯公式作為SMT求解器的輸入，判斷待驗(yàn)證的微內(nèi)核API是否滿足性質(zhì)；如果待驗(yàn)證的微內(nèi)核API不滿足性質(zhì)，則修改該微內(nèi)核API的代碼，并重新建模生成一階邏輯公式，再次輸入SMT求解器；如果所有待驗(yàn)證接口均已滿足性質(zhì)，則該微內(nèi)核API滿足微內(nèi)核操作系統(tǒng)規(guī)范和通用程序性質(zhì)。

2.如權(quán)利要求1所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述步驟一包括以下步驟：

步驟A1：從微內(nèi)核操作系統(tǒng)中的規(guī)范中提取所要驗(yàn)證的接口規(guī)范，包括進(jìn)程間通信、調(diào)度機(jī)制、內(nèi)存管理相關(guān)的自然語(yǔ)言規(guī)范；

步驟A2：根據(jù)自然語(yǔ)言規(guī)范提取性質(zhì)，并用一階邏輯公式對(duì)其進(jìn)行描述。

3.如權(quán)利要求1所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述步驟三包括以下步驟：

步驟B1：從微內(nèi)核源代碼中提取待驗(yàn)證的微內(nèi)核API的代碼到外部文件中；

步驟B2：將與所述待驗(yàn)證的微內(nèi)核API相關(guān)的所有數(shù)據(jù)結(jié)構(gòu)提取到外部文件中；

步驟B3：將與所述待驗(yàn)證的微內(nèi)核API相關(guān)的所有調(diào)用的函數(shù)提取到外部文件中。

4.如權(quán)利要求3所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述B2提取與待驗(yàn)證的微內(nèi)核API相關(guān)的所有數(shù)據(jù)結(jié)構(gòu)，包括待驗(yàn)證的微內(nèi)核API中用到的數(shù)據(jù)結(jié)構(gòu)和嵌套定義使用到的數(shù)據(jù)結(jié)構(gòu)。

5.如權(quán)利要求3所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述B3提取與待驗(yàn)證接口相關(guān)的所有調(diào)用的函數(shù)，包括待驗(yàn)證的微內(nèi)核API中直接調(diào)用的函數(shù)和嵌套使用到的函數(shù)。

6.如權(quán)利要求1所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述步驟四包括以下步驟：

步驟C1：分析提取的API，選擇與該API對(duì)應(yīng)的微內(nèi)核的API性質(zhì)插入，獲得含有API性質(zhì)的微內(nèi)核API；

步驟C2：分析提取的API，將通用性質(zhì)插入到API中，獲得含有通用性質(zhì)的微內(nèi)核API。

7.如權(quán)利要求1所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述步驟五包括以下步驟：

步驟D1：對(duì)API程序進(jìn)行詞法、語(yǔ)法分析，生成對(duì)應(yīng)的控制流圖；

步驟D2：對(duì)API程序進(jìn)行建模，獲得對(duì)應(yīng)的TS模型，獲得程序?qū)?yīng)的一階邏輯公式。

8.如權(quán)利要求7所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述對(duì)API程序進(jìn)行建模，是對(duì)含有API性質(zhì)的微內(nèi)核API和含有通用性質(zhì)的微內(nèi)核API分開(kāi)進(jìn)行建模，分別獲得含有API性質(zhì)的一階邏輯公式和含有通用性質(zhì)的一階邏輯公式。

9.如權(quán)利要求1所述的基于邊界模型檢測(cè)技術(shù)的微內(nèi)核操作系統(tǒng)接口的形式化驗(yàn)證方法中，其特征在于，所述步驟六包括如下步驟：

步驟E1：含有API性質(zhì)的一階邏輯公式作為SMT求解器的輸入；

步驟E2：驗(yàn)證接口程序是否正確，若驗(yàn)證失敗，根據(jù)驗(yàn)證工具給出的提示修改API代碼并重新驗(yàn)證；若驗(yàn)證通過(guò)，則表明該API滿足微內(nèi)核API性質(zhì)；

步驟E3：含有通用性質(zhì)的一階邏輯公式作為SMT求解器的輸入；

步驟E4：驗(yàn)證接口程序是否正確，若驗(yàn)證失敗，根據(jù)驗(yàn)證工具給出的提示修改API代碼并重新驗(yàn)證；若驗(yàn)證通過(guò)，則表明該API滿足程序通用性質(zhì)。