L4虚拟内存子系统的形式化验证

Formal Verification of Virtual Memory Subsystem in L4

第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等;形式化了功能正确性、功能安全和信息安全三方面的属性;通过部分正确性、不变式以及展开条件的推理,在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中,发现源代码在功能正确性和信息安全方面共存在3点问题,给出了相应的解决方案或建议.

L4,the second-generation of microkernel,greatly compensates for the shortcomings of the first-generation of microkernel in flexibility and performance,which has attracted the attention of academia and industry.The kernel is the basic component for implementing the operating system.Once it has errors,it may cause the breakdown of whole system,further causing losses to users.Therefore,it is very important to improve the correctness and reliability of the kernel.Virtual memory subsystem is a key mechanism to implement L4 kernel.This study focuses on the formal modeling and verification of this mechanism.A formal model is presented,which involves all operations of mapping mechanism,all management operations of address space,and MMU behavior with TLB.The properties of functional correctness,safety,and security are formalized.Through reasoning about partial correctness,invariants and unwinding conditions,it is shown that the proposed model satisfies these properties in the theorem prover Isabelle/HOL.During modeling and verification,three problems are found related to functional correctness and security in source code.The corresponding solutions or suggestions are given in this study as well.