作为计算机软件的核心,操作系统的安全对于所有的计算机软件来说都至关重要。但是由于操作系统的规模非常庞大,而且结构极其复杂,这使得操作系统的安全问题存在非常多的不确定性。形式化方法是目前被认可的可以保证系统软件的可靠性、安全性的一种方法。形式化方法是指以严格的数学逻辑系统的为基础,将对应的操作系统抽象成用数学逻辑语言表示的系统(称为形式化系统),通过验证这个系统相关的安全性质来保证操作系统的安全性。OCAP(Open Certified Assembly Programming)是一个出色的形式化验证框架,它不但成功地将操作系统中的不同模块的验证结合起来,同时还保证了框架良好的扩展性。以OCAP为参考,本文在汇编语言层次上建立了一个验证微内核操作系统的形式化验证框架,并用这个框架对我们项目组实现的操作系统VTOS的内核中的消息模块进行验证。本文主要的研究工作及成果主要体现在如下几点：1.在定理证明工具Isabelle里借鉴OCAP验证框架实现一个操作系统VTOS的验证框架,并在这个基础上扩展了OCAP的类型表达能力,使得后面说明形式化系统与实现的系统的一致性更加简单。2.借鉴霍尔逻辑,为指令设置前置条件,并将前置条件分为两个部分：一部分是这个指令所在的特定函数的前置条件,另一个是这个指令本身的前置条件。本框架为每个指令本身设置了合适的前置条件。3.通过这个框架对我们项目组实现的操作系统内核中的消息模块进行验证,主要证明两个方面：第一,证明执行每一条指令时其对应的状态都满足该指令的前置条件(本文称这个性质为代码的良构性)；第二,消息模块的函数功能的正确性。