基于Isabelle/HOL的安全操作系统形式化验证方法

摘要

操作系统作为信息时代的基石,其安全性不言而喻.常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法.本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性.重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况.%As the cornerstone of the information age, the importance of operating system security is self-evident.Conventional methods of software testing are not enough to guarantee the safety of the operating system, so we need to use more rigorous formal verification methods based on mathematical logic.This paper puts forward a new idea of formal verification of software: constructing a simulation running environment in Isabelle, and running the assembly code in it, recording the changes of the system state, and finally according to the changes of system state before and after run of the program, determining the correctness and safety of the program.It emphatically introduces the prove method of sequential, conditional and iterative structure, uses them on to a sample program, and gets the state changes under any preconditions.