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

Program Multiple Execution Paths Verification Based on k Proximity Weakest Precondition

程序多路径验证方法是对软件性质进行发掘的重要方法之一,现有的验证方法主要通过求解路径条件或者自动构造不同的输入来触发生成不同的路径,从而分析程序中潜在的安全问题,但存在对路径条件不加选择地进行多路径扩展而生成缺乏针对性的路径的问题,另外由于路径条件过长而难以求解也限制了它的使用范围.该文提出基于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.