操作系统形式化设计与安全需求的一致性验证研究

• 作者: 宋方敏 钱振江 黄皓
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 操作系统 形式化设计 安全需求 一致性验证 定理证明 信息安全 网络安全
• 年，卷（期）: 2014,（5）
• 所属期刊栏目: 安全与可信软件
• 页码范围: 1082-1099
• 页数: 18页
• 分类号: TP316
• 字数: 13814字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2014.01082

摘要

采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性。目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性。提出一种操作系统形式化设计和验证的方法，采用操作系统对象语义模型（OSOSM）对系统的设计进行形式化建模，使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义。对象语义模型作为系统设计和形式化验证的联系。以实现和验证过的可信微内核操作系统VTOS为实例，阐述形式化设计和安全需求分析，并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证，表明VTOS达到预期的安全性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄皓	南京大学计算机科学与技术系	140	1805	24.0	35.0
2	钱振江	南京大学计算机科学与技术系	16	90	6.0	8.0
8	宋方敏	南京大学计算机科学与技术系	29	191	9.0	13.0