基于ARINC653標準的分區(qū)損傷系統(tǒng)隔離性的驗證研究.pdf

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

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