VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

VSOS-HAM:Research on Isabelle/HOL-based OS kernel hardware abstract model and formal verification method

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.

The formal method is a reliable one to ensure the correctness of design and implementation of operating system. The formal design and verification of operating system is still an extremely complex progress. Because of its low-level,it is difficult to validate the correctness of the assembly layer. How to effectively model for assembly codes,and easily validate the correctness of the semantics and effectiveness becomes a hot topic in the field of operating system formalization. In this paper, we present the method of formal verification of design and implementation of operating system on the assembly layer. We construct the kernel hardware abstract model of operating system, and describe the operational semantics of instructions. Based on this abstract model, we define the