CAJ | 학술논문

程序多路径验证方法是对软件性质进行发掘的重要方法之一，现有的验证方法主要通过求解路径条件或者自动构造不同的输入来触发生成不同的路径，从而分析程序中潜在的安全问题，但存在对路径条件不加选择地进行多路径扩展而生成缺乏针对性的路径的问题，另外由于路径条件过长而难以求解也限制了它的使用范围。该文提出基于 k 近邻最弱前置条件的程序多路径验证方法，该方法通过后向符号分析对程序调用图的构建过程进行改进，同时对指定的程序检测点生成最弱前置条件，并以该最弱前置条件为引导信息使用符号执行的方法在保证检测点可达的前提下有针对性地生成对程序性质进行验证的精简路径集合。实验结果表明，该方法可以提高程序验证的精度和准确性，并减少误报。
정서다로경험증방법시대연건성질진행발굴적중요방법지일，현유적험증방법주요통과구해로경조건혹자자동구조불동적수입래촉발생성불동적로경，종이분석정서중잠재적안전문제，단존재대로경조건불가선택지진행다로경확전이생성결핍침대성적로경적문제，령외유우로경조건과장이난이구해야한제료타적사용범위。해문제출기우 k 근린최약전치조건적정서다로경험증방법，해방법통과후향부호분석대정서조용도적구건과정진행개진，동시대지정적정서검측점생성최약전치조건，병이해최약전치조건위인도신식사용부호집행적방법재보증검측점가체적전제하유침대성지생성대정서성질진행험증적정간로경집합。실험결과표명，해방법가이제고정서험증적정도화준학성，병감소오보。
Program multiple paths verification is one of the key methods in the exploring of soft-ware 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 k proximity 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 paths that 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.