微内核架构内存管理的形式化设计和验证方法研究

摘要

由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare 三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.%The correctness of design and implementation of operating systems is difficult to be described with the traditional quantitative methods,because of the enormous size and complexity.This paper illustrates our method of formal design and verification of microkernel operating system.We construct the system model with the non-deterministic automaton in the assembly level,and use the Hoare triples to describe the previous and post conditions of the interface functions,as the definitions of function correctness.We take the module of memory management in the self-implemented VSOS (Verified Secure Operating System) as an example,to illustrate our formal method.Meanwhile,we formally describe the constructed memory management model and operation semantics of system behaviors in the Isabelle/HOL theorem prover,and verify the correctness of design and implementation of the memory management.The result shows that the method proposed is feasible and efficient.