作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2011, Vol. 37 ›› Issue (7): 28-30. doi: 10.3969/j.issn.1000-3428.2011.07.010

• 软件技术与数据库 • 上一篇    下一篇

改进的程序时序安全属性模型检测技术

张 志1a,1b,张 林1a,1b,曾庆凯1a,1b,2   

  1. (1. 南京大学 a. 计算机软件新技术国家重点实验室;b. 计算机科学与技术系,南京 210093;2. 上海市信息安全综合管理技术研究重点实验室,上海 200030)
  • 出版日期:2011-04-05 发布日期:2011-03-31
  • 作者简介:张 志(1984-),男,硕士研究生,主研方向:信息安全;张 林,硕士研究生;曾庆凯,教授、博士、博士生导师
  • 基金资助:
    国家自然科学基金资助项目(60773170, 60721002, 9081 8022);国家“863”计划基金资助项目(2006AA01Z432);高等学校博士学科点专项科研基金资助项目(200802840002);上海市信息安全综合管理技术研究重点实验室开放课题基金资助项目(AGK2008 003)

Improved Model Checking Technology for Program Temporal Safety Properties

ZHANG Zhi  1a,1b, ZHANG Lin  1a,1b, ZENG Qing-kai  1a,1b,2   

  1. (1a. State Key Laboratory for Novel Software 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)
  • Online:2011-04-05 Published:2011-03-31

摘要: 针对程序时序安全属性模型检测技术改进模型检测算法,使安全漏洞状态机以函数为单位进行扩展,简化程序模型检测过程,以提高检测效率。在检测过程中加入别名分析,考虑安全操作之间的数据流依赖关系,以提高检测的准确性。实验结果表明,改进后的方法比原检测方法具有更高的效率和准确性。

关键词: 时序安全属性, 模型检测, 别名分析

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.

Key words: temporal safety property, model checking, alias analysis

中图分类号: