形式化验证下的分区操作系统内核隔离特性研究

本文主要探讨了在分区操作系统内核的设计和实现中如何确保隔离性质的重要性。针对安全关键系统的需求，作者提出了一种形式化的方法来验证操作系统内核的隔离特性。首先，通过顶层规范设计，明确阐述了隔离性质的需求，这涉及到航空电子应用软件的标准接口ARINC653，该接口为系统间交互提供了一个标准化框架。 ARINC653是一个行业标准，它在航空电子系统中被广泛应用，强调了可靠性和安全性。在此基础上，作者引入了GWV定理，这是一种用于系统验证的理论工具，与ARINC653结合，能够帮助分析和表达分区操作系统所必需的隔离特性。这种结合使得系统设计更加严谨，确保了隔离性质的精确性。 文章采用类Z/Z++作为形式化描述语言，这是一种强大的数学逻辑系统，能够用来构造严格的证明和验证。类Z/Z++提供了一种结构化的表达方式，有助于捕捉和证明操作系统的复杂行为和安全属性，如数据完整性、一致性以及隔离性等。 在隔离内核的设计上，文章提到的SephKernel（分离内核）和SKPP（分离内核保护文件）是两个重要的概念。SephKernel最初由Rushby在1981年提出，目的是在操作系统内核层面实现进程间的安全隔离，防止恶意交互。SKPP则进一步扩展了这个概念，允许分区包含多个组件，并支持每个分区有自己的操作系统，强化了隔离的要求。 Crailg在参考Rushby和SKPP的基础上，使用Z规范语言来详细描述了隔离内核的具体需求，包括数据域的划分、通信权限的控制，以及如何确保只有在分区明确授权的情况下才能进行信息交换。这确保了在分区环境中，不同区域的操作和数据不会互相干扰，提高了系统的可信性和安全性。 总结来说，本文的核心内容是利用形式化方法，结合ARINC653和GWV定理，通过类Z/Z++的形式化描述，深入研究和设计了分区操作系统的隔离性质，为构建安全关键系统提供了强有力的技术支持。同时，文中提及的隔离内核和SKPP概念也为实际操作系统的实现提供了实用的设计框架和规范。