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

• 作者: 刘苇 杨维永 郭毅
• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 安全操作系统 形式化验证 Isabelle/HOL 霍尔逻辑
• 年，卷（期）: 2017,（4）
• 所属期刊栏目: 信息安全
• 页码范围: 99-104
• 页数: 6页
• 分类号: TP309.2
• 字数: 5153字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2017.04.0020

摘要

操作系统作为信息时代的基石,其安全性不言而喻.常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法.本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性.重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭毅		1	1	1.0	1.0
2	杨维永		5	11	2.0	3.0
3	刘苇		1	1	1.0	1.0