摘要
针对程序时序安全属性模型检测技术改进模型检测算法,使安全漏洞状态机以函数为单位进行扩展,简化程序模型检测过程,以提高检测效率。在检测过程中加入别名分析,考虑安全操作之间的数据流依赖关系,以提高检测的准确性。实验结果表明,改进后的方法比原检测方法具有更高的效率和准确性。
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.
出处
《计算机工程》
CAS
CSCD
北大核心
2011年第7期28-30,共3页
Computer Engineering
基金
国家自然科学基金资助项目(60773170
60721002
90818022)
国家"863"计划基金资助项目(2006AA01Z432)
高等学校博士学科点专项科研基金资助项目(200802840002)
上海市信息安全综合管理技术研究重点实验室开放课题基金资助项目(AGK2008003)
关键词
时序安全属性
模型检测
别名分析
temporal safety property
model checking
alias analysis