XSM语义模型及安全需求形式化验证

• 作者: 孙磊 朱智强 祝现威
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: XSM 语义模型 形式化验证 安全性分析 Isabelle/HOL
• 年，卷（期）: 2017,（6）
• 所属期刊栏目: 安全技术
• 页码范围: 314-321
• 页数: 8页
• 分类号: TP311
• 字数: 6656字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2017.06.056

摘要

Xen作为一种开源流行的虚拟化工具,使用越来越频繁.作为Xen的安全框架XSM(Xen Security Module)也受到广泛的关注.许多研究者通过形式化的方式对现有的操作系统进行正确性的验证,目前已有的形式化研究主要是验证系统实现的代码正确性.从系统功能角度提出了一种以主体行为为操作系统语义模型对系统进行形式化建模,并采用CTL时序逻辑对XSM安全需求进行分析.语义模型作为系统设计合理性和形式化验证的联系,对XSM进行形式化验证,并使用Isabelle/HOL验证功能和安全需求的一致性,以说明XSM是否符合安全需求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙磊	信息工程大学密码工程学院	30	141	7.0	11.0
2	祝现威	信息工程大学密码工程学院	3	0	0.0	0.0
3	朱智强	信息工程大学密码工程学院	13	40	3.0	6.0