操作系统形式化验证综述

Review of formal verification for operating system

介绍操作系统验证理论、语言和工具等技术基础,阐述验证路径、精化关系验证和大规模验证等新的验证方法和理念。比较分析多个操作系统验证项目研究内容、验证方法、主要贡献以及最新进展。分析操作系统验证过程中存在的问题,认为验证成本高、验证工具局限性是制约操作系统形式化验证的关键因素,随着验证工具、框架和定理库的完善,以及深度学习等新技术的应用,操作系统更多的安全性质能够被形式化验证。

This paper introduces the technical foundations of operating system verification theory,language,and tools,and elaborates new verification methods and concepts such as the verification path,refined relationship verification and large-scale verification.The research content,verification methods,main contributions,and latest developments of multiple operating system verification projects are compared and analyzed.Meanwhile,this study also analyzes the problems in the process of operating system verification and believes that the high cost of verification and the limitations of verification tools are the key factors that restrict the formal verification of operating system.With the improvement of verification tools,frameworks and theorem libraries,new technologies such as deep learning have been improved and applied,thus more security properties of the operating system can be formally verified.