基于静态分析的XSM正确性验证

• 作者: 丁丽萍 贺也平 邓程 韩伟
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 静态分析 正确性验证 XSM 钩子函数 Saturn
• 年，卷（期）: 2012,（9）
• 所属期刊栏目: 基金项目论文
• 页码范围: 1-5,22
• 页数: 6页
• 分类号: TP312
• 字数: 7541字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2012.09.001

摘要

XSM(Xen Security Module)是虚拟机Xen的安全模型框架,对系统的安全性具有决定性的作用.目前,对类似的强制访问框架的正确性验证研究主要集中于对钩子函数放置的验证.现有检测方法通常路径覆盖不够完整,或者有较高的误报率.对XSM框架的正确性验证问题进行分析,提出一种过程间流敏感、过程内路径敏感的,适用于XSM框架的静态分析方法.该方法通过扩展静态分析工具Saturn,实现了对XSM框架的钩子函数设置的正确性和完备性的验证.经实验验证,该方法具有完全的路径覆盖性,并且具有较高的精确度.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	贺也平	中国科学院软件研究所	46	727	16.0	26.0
2	韩伟	中国科学院软件研究所	40	192	9.0	13.0
6	丁丽萍	中国科学院软件研究所	32	379	10.0	19.0
7	邓程	中国科学院软件研究所	1	1	1.0	1.0