| 改进的程序时序安全属性模型检测技术 |
| |
| 引用本文： | 张志,张林,曾庆凯.改进的程序时序安全属性模型检测技术[J].计算机工程,2011,37(7):28-30. |
| |
| 作者姓名： | 张志 张林 曾庆凯 |
| |
| 作者单位： | 1. 南京大学,计算机软件新技术国家重点实验室,南京210093;南京大学,计算机科学与技术系,南京210093
2. 南京大学,计算机软件新技术国家重点实验室,南京210093;南京大学,计算机科学与技术系,南京210093;上海市信息安全综合管理技术研究重点实验室,上海200030 |
| |
| 基金项目： | 国家自然科学基金资助项目，国家"863"计划基金资助项目，高等学校博士学科点专项科研基金资助项目，上海市信息安全综合管理技术研究重点实验室开放课题基金资助项目 |
| |
| 摘 要： | 针对程序时序安全属性模型栓测技术改进模型检测算法,使安全漏洞状态机以函数为单位进行扩展,简化程序模型检测过程,以提高检测效率.存检测过程中加入别名分析,考虑安全操作之间的数据流依赖关系,以提高检测的准确性.实验结果表明,改进后的方法比原检测方法具有更高的效率和准确性.
|
| 关 键 词： | 时序安全属性 模型检测 别名分析 |
Improved Model Checking Technology for Program Temporal Safety Properties |
| |
| ZHANG Zhi,ZHANG Lin,ZENG Qing.Improved Model Checking Technology for Program Temporal Safety Properties[J].Computer Engineering,2011,37(7):28-30. |
| |
| Authors: | ZHANG Zhi ZHANG Lin ZENG Qing |
| |
| Affiliation: | 1a,1b,2(1a.State Key Laboratory for Novel Software Technology;1b.Department of Computer Science and Technology,Nanjing University,Nanjing 210093,China;2.Shanghai Key Laboratory of Integrate Administration Technologies for Information Security,Shanghai 200030,China) |
| |
| Abstract: | This paper presents two points of improvements for model checking temporal safety properties of program： more efficient model checking algorithm is proposed,which can simplify the checking process and reduce the time cost by extending the state machine model with each function.Alias analysis is used to determine the dataflow dependency between safety operations,which makes the checking process more accurate.Experimental results show that the method can work more efficiently and exactly. |
| |
| Keywords: | temporal safety property model checking alias analysis |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
|
