基于ARINC653標(biāo)準(zhǔn)的分區(qū)損傷系統(tǒng)隔離性的驗(yàn)證研究.pdf

1、安全關(guān)鍵系統(tǒng)在社會生產(chǎn)生活中扮演著重要的角色，尤其是應(yīng)用于一些對于可靠性要求極高的領(lǐng)域。安全內(nèi)核作為系統(tǒng)的核心組成，對于構(gòu)建一個可信系統(tǒng)至關(guān)重要。隔離內(nèi)核是基于安全內(nèi)核提出的，解決了大型、復(fù)雜的安全內(nèi)核在設(shè)計(jì)和驗(yàn)證過程中存在的問題，為系統(tǒng)提供了多層次的安全操作。如何提供隔離機(jī)制確保應(yīng)用間不存在未授權(quán)的信息交互，以及如何對隔離內(nèi)核進(jìn)行形式化驗(yàn)證已成為國際上的研究重點(diǎn)之一。形式化驗(yàn)證的方法主要有三種:模型檢驗(yàn)，等價(jià)性證明，定理證明。本文采用

2、定理證明的方式，通過對操作系統(tǒng)內(nèi)核進(jìn)行框架設(shè)計(jì)，進(jìn)而將內(nèi)核需要滿足的性質(zhì)進(jìn)行描述，最后對隔離性質(zhì)進(jìn)行證明。
　　本文研究的重點(diǎn)構(gòu)造一個經(jīng)過證明的分區(qū)隔離內(nèi)核，該內(nèi)核滿足GWV定理所描述的隔離性質(zhì)。GWV定理明確描述了隔離內(nèi)核可以提供的操作，構(gòu)建這一安全策略是隔離內(nèi)核形式化驗(yàn)證的基礎(chǔ)。通過對系統(tǒng)允許行為和保護(hù)系統(tǒng)的形式化規(guī)范進(jìn)行分析，描述出分區(qū)操作系統(tǒng)隔離內(nèi)核框架。
　　根據(jù)分區(qū)操作系統(tǒng)隔離內(nèi)核框架以及需要滿足的性質(zhì)，利用形式