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

Formal Verification Method of Secure Operating System Based on Isabelle/HOL

作　　者：郭毅 杨维永 刘苇 

机构地区：[1]南京南瑞信息通信科技有限公司,江苏南京210003

出　　处：《计算机与现代化》2017年第4期99-104,共6页Computer and Modernization

基　　金：国家自然科学基金资助项目(61321491);江苏省工业和信息产业转型升级专项项目(2015SJXKJ5038);国网电力科学研究院科技项目(5246DR150002)

摘　　要：操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在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.

关 键 词：安全操作系统 形式化验证 Isabelle/HOL 霍尔逻辑 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]