基于k近邻最弱前置条件的程序多路径验证方法

• 作者: 张焕国 王建勇 王盼 郭曦
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 程序验证 静态分析 最弱前置条件 符号执行 控制流图
• 年，卷（期）: 2015,（11）
• 所属期刊栏目: 软件工程
• 页码范围: 2203-2214
• 页数: 12页
• 分类号: TP311
• 字数: 10975字
• 语种: 中文
• DOI: 10.11897/SP.J.1016.2015.02203

摘要

程序多路径验证方法是对软件性质进行发掘的重要方法之一，现有的验证方法主要通过求解路径条件或者自动构造不同的输入来触发生成不同的路径，从而分析程序中潜在的安全问题，但存在对路径条件不加选择地进行多路径扩展而生成缺乏针对性的路径的问题，另外由于路径条件过长而难以求解也限制了它的使用范围。该文提出基于 k 近邻最弱前置条件的程序多路径验证方法，该方法通过后向符号分析对程序调用图的构建过程进行改进，同时对指定的程序检测点生成最弱前置条件，并以该最弱前置条件为引导信息使用符号执行的方法在保证检测点可达的前提下有针对性地生成对程序性质进行验证的精简路径集合。实验结果表明，该方法可以提高程序验证的精度和准确性，并减少误报。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王建勇	华中农业大学信息学院	22	139	7.0	11.0
2	王盼	武汉电力职业技术学院电力工程系	19	69	4.0	8.0
3	郭曦	华中农业大学信息学院	8	18	3.0	4.0
5	张焕国		2	18	2.0	2.0