论文部分内容阅读
操作系统作为直接对硬件进行操作的软件,其安全性一直是工业界和学术界研究的热点。特别是在安全悠关的领域必须确保操作系统的安全性,比如航空航天、医疗和无人机等领域。目前公认的验证操作系统的最有效方法是形式化方法。研究人员大多致力于研究操作系统的功能正确性和完整性等属性,很少针对其安全性进行分析、建模和验证。本文总结了现有的研究方法,提取了操作系统的安全性需求,根据这些需求设计并实现了微内核操作系统——四线程操作系统(four threads operating system,FTOS),并用形式化的方法对其安全性进行建模和验证。本文的主要研究内容包括以下三个部分:(1)从利于形式化验证的角度设计和实现微内核操作系统,在开发FTOS的过程中就考虑验证相关的问题,避免在系统设计的过程中使用过多复杂的数据结构和算法,降低验证的难度。设计了关于进程和中断的形式化语义,提出并发与非确定性问题将增加对抢占式操作系统验证的难度,并提出采用并发分离逻辑来解决该问题。(2)从FTOS中提取出抽象功能规范,建立了描述系统行为双层精化模型。高层抽象规范描述了系统做了什么,不涉及具体的操作。相对于高层规范,底层具体规范是对FTOS的更具体的描述,描述了系统是如何做的,包括C代码和汇编代码的抽象语义。建立上下两层之间的精化关系,该关系考虑到并发带来的非确定性因素,引进了不变式概念,以此来确保上下层规范之间系统状态的一致性。最后以进程调度和中断处理行为为例,说明了底层规范实现了对高层规范的精化。(3)从微内核操作系统中提取出初始化、进程调度和中断处理这三个最主要的功能模块,组成对操作系统的形式化验证的论域。建立了并发分离逻辑的相关断言的语法和语义,并简述了主要的推理规则。设计系统初始化、进程调度行为和中断处理行为的前置条件和后置条件,并根据这些条件提出它们需要满足的不变式。在定理证明器Coq中定义并验证了上述行为的引理,并整合了上述功能模块的证明形成完整的系统正确性证明,对系统的设计和安全需求的一致性进行了验证。