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

Program Multiple Execution Paths Verification Based on k Proximity Weakest Precondition

作　　者：郭曦[1,4] 王盼[2] 王建勇[1] 张焕国[3] 

机构地区：[1]华中农业大学信息学院,武汉430070 [2]武汉电力职业技术学院电力工程系,武汉430079 [3]软件工程国家重点实验室(武汉大学),武汉430072 [4]佐治亚理工学院计算机科学系,美国亚特兰大30332

出　　处：《计算机学报》2015年第11期2203-2214,共12页Chinese Journal of Computers

基　　金：国家自然科学基金(61332019,61173138,61272452,91118003);国家“九七三”重点基础研究发展规划项目基金(2014CB340600);国家“八六三”高技术研究发展计划项目基金(2015AA016002);湖北省自然科学基金(2014CFB144);中央高校基本科研业务费专项基金(2662015QC009)资助~~

摘　　要：程序多路径验证方法是对软件性质进行发掘的重要方法之一,现有的验证方法主要通过求解路径条件或者自动构造不同的输入来触发生成不同的路径,从而分析程序中潜在的安全问题,但存在对路径条件不加选择地进行多路径扩展而生成缺乏针对性的路径的问题,另外由于路径条件过长而难以求解也限制了它的使用范围.该文提出基于k近邻最弱前置条件的程序多路径验证方法,该方法通过后向符号分析对程序调用图的构建过程进行改进,同时对指定的程序检测点生成最弱前置条件,并以该最弱前置条件为引导信息使用符号执行的方法在保证检测点可达的前提下有针对性地生成对程序性质进行验证的精简路径集合.实验结果表明,该方法可以提高程序验证的精度和准确性,并减少误报.Program multiple paths verification is one of the key methods in the exploring of software properties.Current verifications usually trigger the generation of different execution paths via solving the path conditions or constructing inputs automatically to verify the underlying security problems in programs.However,this method extends the multiple paths without choosing the proper path conditions,which leads to the generation of redundant paths,meanwhile,the length of path conditions is usually too long,which restrains its application domain.A method of program multiple paths verification based on kproximity weakest precondition is proposed in this paper,which improves the generation of call graph of the program,and combines the backward symbolic analysis to generate the weakest preconditions in specific checking points.The results of weakest precondition are used as the guidance for symbolic execution to generate proper pathsthat can verify the properties of the program on the premise of reaching the specific checking points.The experimental results demonstrate that this method can enhance the precision and accuracy of program verification,and reduce the false positive.

关 键 词：程序验证 静态分析 最弱前置条件 符号执行 控制流图 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]