复杂内核数据结构程序形式化验证

Formal Verification of Complex Kernel Data Structure Programs

操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节,但是,在实际的验证工作中,操作系统内核中全局性质的不变式定义,复杂数据结构程序的形式化描述和验证仍存在很多困难.本文针对操作系统内核中满足的全局性质,在代码层以函数为单位,用全局不变式进行定义,并在不同的函数中进行形式化验证,从而证明各个函数符合操作系统内核的全局性质;针对操作系统内核中经常使用的复杂数据结构程序,本文通过扩展形状图理论,提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序,并对该方法进行了正确性证明,最终成功验证操作系统内核中关于任务创建与调度,消息队列创建与操作相关的代码.

As a fundamental component of a software system,the kernel of an operating system plays a crucial role in constructing a highly trusted software system.However,in practical verification,there are still many difficulties in invariant definition of global properties,and formal description and verification of complex data structure programs in the kernel of an operating system.Given the global properties satisfied by the kernel of an operating system,this study defines these properties at the code level on a function-by-function basis through global invariants and conducts formal verification in different functions to prove that each function conforms to the global properties of the operating system kernel.To formalize the complex data structure programs frequently adopted in the kernel of an operating system,the study proposes a method employing nested shape graph logic by extending the shape graph theory and provides a correctness proof for this method.Finally,it verifies the code related to task creation and scheduling,and message queue creation and operation in the operating system kernel.