[發(fā)明專利]基于微內(nèi)核原型的進程間通信安全性形式化分析驗證系統(tǒng)

在審

• 申請?zhí)枺?/td>: 201611167121.0
• 申請日: 2016-12-16
• 公開（公告）號: CN106802863A
• 公開（公告）日: 2017-06-06
• 發(fā)明（設(shè)計）人: 毛俠;史建琦;黃滟鴻;李昂
• 申請（專利權(quán)）人: 華東師范大學(xué)
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 上海麥其知識產(chǎn)權(quán)代理事務(wù)所(普通合伙)31257
• 代理人: 董紅曼

1.一種基于嵌入式操作系統(tǒng)微內(nèi)核原型的進程間通信安全性形式化分析驗證系統(tǒng)，其特征在于，包括以下模塊：

原型預(yù)處理模塊，其包含所述形式化分析驗證系統(tǒng)的系統(tǒng)入口，并且以嵌入式操作系統(tǒng)微內(nèi)核原型為輸入，經(jīng)過微內(nèi)核模塊分類提取器處理從中提取出待驗證的IPC模塊，生成IPC功能相關(guān)的集合作為各模塊輸入的待驗證數(shù)據(jù)；

可數(shù)狀態(tài)特定屬性驗證模塊，其與所述原型預(yù)處理模塊通信，用于驗證有窮狀態(tài)下特定屬性的IPC安全性質(zhì)，可有針對性地對待驗證的IPC故障行為進行建模分析；

無窮狀態(tài)及泛化屬性驗證模塊，其與所述原型預(yù)處理模塊通信，用于驗證無窮狀態(tài)或非特定屬性的IPC安全性質(zhì)、驗證由規(guī)范化數(shù)據(jù)結(jié)構(gòu)抽象出的IPC外在性質(zhì)、及基于已有抽象性質(zhì)針對各興趣點深入抽象且進一步生成不同的模型并精化驗證。

2.根據(jù)權(quán)利要求1所述的基于嵌入式操作系統(tǒng)微內(nèi)核原型的進程間通信安全性形式化分析驗證系統(tǒng)，其特征在于，進一步設(shè)有：可視化模塊，其分別與所述原型預(yù)處理模塊、所述可數(shù)狀態(tài)特定屬性驗證模塊及所述無窮狀態(tài)及泛化屬性驗證模塊交互，所述可視化模塊用于驗證過程及結(jié)果中圖形、文本和信息的可視呈現(xiàn)。

3.根據(jù)權(quán)利要求1所述的基于嵌入式操作系統(tǒng)微內(nèi)核原型的進程間通信安全性形式化分析驗證系統(tǒng)，其特征在于，所述可數(shù)狀態(tài)特定屬性驗證模塊包括：

系統(tǒng)故障行為建模工具，其與所述原型預(yù)處理模塊通信，用于對系統(tǒng)微內(nèi)核故障行為建模，輸出狀態(tài)機元模型；

模型轉(zhuǎn)換引擎，其將所述狀態(tài)機元模型作為輸入，根據(jù)需要轉(zhuǎn)換成規(guī)范化故障模型；及

模型自動化分析工具，其將所述規(guī)范化故障模型輸入到對應(yīng)的模型自動化分析工具中，得到驗證結(jié)果。

4.根據(jù)權(quán)利要求1所述的基于嵌入式操作系統(tǒng)微內(nèi)核原型的進程間通信安全性形式化分析驗證系統(tǒng)，其特征在于，所述無窮狀態(tài)及泛化屬性驗證模塊包括：

可執(zhí)行規(guī)范化轉(zhuǎn)化引擎，將基于微內(nèi)核原型的IPC功能相關(guān)集合作為輸入，轉(zhuǎn)換成可執(zhí)行規(guī)范的數(shù)據(jù)結(jié)構(gòu)，且包括抽象出的IPC性質(zhì)；

定理證明器，其將抽象出的IPC性質(zhì)作為輸入，經(jīng)判定、深入抽象獲得包含可體現(xiàn)微內(nèi)核IPC外在功能特性的IPC抽象性質(zhì)集，并經(jīng)精化證明反復(fù)驗證系統(tǒng)微內(nèi)核的安全性質(zhì)。

5.根據(jù)權(quán)利要求4所述的基于嵌入式操作系統(tǒng)微內(nèi)核原型的進程間通信安全性形式化分析驗證系統(tǒng)，其特征在于，所述定理證明器包括：Isabelle/HOL、Coq、Maude。