操作系统形式化验证综述

摘要

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