操作系统作为基础软件,为上层的各种应用软件提供了支撑和服务的平台。为此,操作系统的安全性是计算机系统信息安全的重要基础。然而,操作系统设计和实现的正确性是安全性的基础,如何保证操作系统设计和实现的正确性是信息安全领域的研究热点。学术界高度关注对操作系统的正确性等属性进行形式化证明的方法的研究。本文认为,为了保证系统的安全性,应该通过需求分析和系统建模,归纳出系统安全性的条件,基于这些安全性条件来设计系统的功能,提出有针对性的设计原则或解决方案,以公认可以接受的方式证实系统的设计不存在违背安全性条件的漏洞,并以公认可以接受的方式证实系统的代码正确地实现了系统的设计。本文旨在形成一套易于建模、描述能力强、推理方便的形式化技术和方法,研究有效的OS设计理论、实现和验证方法,为设计功能正确、执行可信、可验证其安全性的操作系统提供有价值的理论依据和开发技术。本文主要从操作系统形式化设计和验证的角度,研究形式化方法在系统设计和验证过程中的可行性,形成了一套操作系统形式化设计和验证的方案,最大程度上地保证系统的正确性和安全性。本文的工作包括两个方面：系统功能设计与需求的验证,以及系统功能实现的正确性验证。具体包括以下三个部分：(1)从系统设计的角度,以高阶逻辑和类型论为基础,提出操作系统对象语义模型(OSOSM)。OSOSM采用分层结构,包括基本功效层、实现层和优化层。OSOSM将操作系统中的行为主体和资源抽象为操作系统对象,建立操作系统的论域,利用以操作系统对象变元集合为定义域到论域的映射表示操作系统的状态,描述操作系统系统调用等行为的语义,使用逻辑系统的谓词公式表达操作系统的安全属性,给出如何验证操作系统在运行过程中保持安全策略和属性的形式化描述方法。以实现并经过形式化验证的可信操作系统(Verified Trusted Operating System, VTOS)中的虚拟内存管理模块(Virtual Memory Management, VMM)为例,阐述OSOSM的语义正确性。使用Isabelle定理证明工具验证设计和安全需求的一致性,以说明VTOS具有预期的安全属性。(2)利用OSOSM对系统的设计进行形式化建模,阐述在VTOS微内核设计过程中构建OSOSM的方法,从系统行为功效完整性和进程行为隔离性的角度对微内核操作系统的安全需求进行了分析,使用带有时序逻辑的高阶逻辑对安全需求进行严格的定义和描述,并在定理证明器Isabelle/HOL环境中对系统的设计和安全需求的一致性进行验证,表明VTOS微内核系统行为的功效设计符合安全需求的定义。(3)提出一个操作系统状态自动机(OS State Automaton, OSSA)模型作为VTOS汇编语言层设计和验证的纽带,通过定义OSSA的合法状态和状态转换函数来建立OSSA的论域,并以此来描述VTOS汇编层的论域。通过验证汇编层的功能模块的正确性来保证VTOS汇编语言层的正确性。