摘要
动态符号执行是对程序进行安全性分析的重要技术.在动态符号执行过程中,存在着符号地址,系统调用,路径选择等问题.针对符号地址导致的别名分析问题,本文提出了一种基于约束的指针分析方法,对程序进行过程内的指向分析,并对指针分析过程引入约束条件,产生可以进行路径选择的测试用例,以提高指针分析的精度.在国内首款某型号商用编译器的开发过程中实现了该方法,实验结果表明,该方法可以准确地分析C语言测试用例,缩短用例测试的时间.
Dynamic symbolic execution is the vital technique in the security analysis of this program.There are several problems in the process of dynamic symbolic execution,such as symbolic address,system call,and path selection.In order to explore the aliasing problem due to the symbol address analysis,an improved pointer analysis based on constraint programming is proposed.Intraprocedural pointer-to analysis and specific constraints are used to improve the precise of pointer analysis.The method has been implemented during the development of a compiler,which is the first domestic commercial compiler.The results of experiment show that this method analysizes C programs correctly and reduces the execution time as well.
出处
《武汉大学学报（理学版）》
CAS
CSCD
北大核心
2011年第5期389-393,共5页
Journal of Wuhan University:Natural Science Edition
基金
国家自然科学基金(61003268
91018008)
空天信息安全与可信计算教育部重点实验室开放基金资助项目(AISTC2008_01
AISTC2008Q02)
关键词
约束求解
静态单指派
指向分析
路径选择
测试用例生成
constraint solving
static single assignment
pointer-to analysis
path selection
test data generation
