一种基于约束的指针程序路径选择方法

摘要：

　　动态符号执行是对程序进行安全性分析的重要技术。在动态符号执行过程中，存在着符号地址，系统调用，路径选择等问题。针对符号地址导致的别名分析问题，本文提出了一种基于约束的指针分析方法，对程序进行过程内的指向分析，并对指针分析过程引入约束条件，产生可以进行路径选择的测试用例，以提高指针分析的精度。在国内首款某型号商用编译器的开发过程中实现了该方法，实验结果表明，该方法可以准确地分析C语言测试用例，缩短用例测试的时间。

关键词： 约束求解 静态单赋值 符号动态执行 指针分析 路径选择

作者: 郭曦 张焕国

作者单位: 武汉大学计算机学院，湖北武汉 430072 武汉大学空天信息安全与可信计算教育部重点实验室，湖北武汉 430072

会议类型: 国内会议

会议名称: 2011年第五届中国可信计算与信息安全学术会议(CTCIS2011)

会议地点: 贵阳

会议语种:中文

页码: 147-151

在线出版日期: 2011-08-01（万方平台首次上网日期，不代表论文的发表时间）