程序状态条件合并中变量隐式关联分析方法
|
摘要
程序分析的主要目标是对程序的性质进行研究,符号执行作为目前主流的分析方法在生成高效的测试用例集或提高路径覆盖率等方面发挥着重要的作用,其中路径条件表达式的提取以及约束求解是路径分析过程中的关键步骤.现有的路径分析方法普遍存在约束求解效率不高而导致的路径覆盖率较低的问题.由于符号执行引擎所采用的搜索策略不尽相同,在符号执行分析过程中存在状态合并的过程,该抽象过程可能导致产生不正确的测试用例.以提高路径分析效率为目标,提出一种高效的程序分析方法:首先对传统的符号执行树的表示方法进行改进,提取不同路径共享的符号表达式和路径约束条件以提高符号执行过程中状态合并的效率,然后采用隐式关联分析方法,产生逆向分析中的依赖条件集合,并给出基于依赖条件重构的算法以提高路径覆盖率.实验结果表明:相对于传统的状态合并以及符号执行方法,该方法有更为高效的状态合并效率以及更高的路径约束条件分析精度.
The main purpose of program analysis is researching the properties of programs.Symbolic execution,which is the current popular analysis method,plays an important role in the aspects of generating efficient test cases,improving the path coverage ratio and so on.The key processes are extracting the path constraint and constraint solving.The current analysis methods have the shortcomings with low efficient of constraint solving,which results to low path coverage ratio.Due to different search strategies used by symbolic execution engine,the process of state merging may exist during symbolic execution,which may result to incorrect path information.This paper aims at improving the efficiency of path analysis,and a high efficient program analysis method is proposed.The shape of conventional symbolic execution tree is improved,and extracting the symbolic expression and path constraints in different paths to improve the efficiency of state merging;and then we use the potential relation analysis to generate the dependent relation set in backward analysis.The algorithm of dependent relation reorder is proposed to improve the path coverage ratio.Experimental results demonstrate that our method can improve the efficiency of state merging and improve the accuracy of path constraint analysis compared with conventional methods of state merging and symbolic execution.
The main purpose of program analysis is researching the properties of programs.Symbolic execution,which is the current popular analysis method,plays an important role in the aspects of generating efficient test cases,improving the path coverage ratio and so on.The key processes are extracting the path constraint and constraint solving.The current analysis methods have the shortcomings with low efficient of constraint solving,which results to low path coverage ratio.Due to different search strategies used by symbolic execution engine,the process of state merging may exist during symbolic execution,which may result to incorrect path information.This paper aims at improving the efficiency of path analysis,and a high efficient program analysis method is proposed.The shape of conventional symbolic execution tree is improved,and extracting the symbolic expression and path constraints in different paths to improve the efficiency of state merging;and then we use the potential relation analysis to generate the dependent relation set in backward analysis.The algorithm of dependent relation reorder is proposed to improve the path coverage ratio.Experimental results demonstrate that our method can improve the efficiency of state merging and improve the accuracy of path constraint analysis compared with conventional methods of state merging and symbolic execution.
引文
[1] Kuznetsov V,Kinder J,Bucur S,et al.Efficient state merging in symbolic execution[J].ACM SIGPLAN Notices,2012,47(6):193-204
[2] Godefroid P.Compositional dynamic test generation[C]//Proc of the 34th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages.New York:ACM,2007:47-54
[3] Avgerinos T,Rebert A,Cha S K,et al.Enhancing symbolic execution with veritesting[C]//Proc of the 36th Int Conf on Software Engineering.New York:ACM,2014:1083-1094
[4] Godefroid P,Nori A V,Rajamani S K,et al.Compositional may-must program analysis:Unleashing the power of alternation[C]//Proc of the 37th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages.New York:ACM,2010:43-56
[5] Wang Chong,LüYinrun,Chen Li,et al.Survey on development of solving methods and state-of-the-art application of satisfiability modulo theories[J].Journal of Computer Research and Development,2017,54(7):1405-1425(in Chinese)(王翀,吕荫润,陈力,等.SMT求解技术的发展及最新应用研究综述[J].计算机研究与发展,2017,54(7):1405-1425)
[6] Torlak E,Bodik R.A lightweight symbolic virtual machine for solver-aided host languages[J]. ACM SIGPLAN Notices,2014,49(6):530-541
[7] Visser W,Reanu C S,Nek R.Test input generation for java containers using state matching[C]//Proc of the 5th Int Symp on Software Testing and Analysis.New York:ACM,2006:37-48
[8] Boonstoppel P,Cadar C,Engler D.RWset:Attacking path explosion in constraint-based test generation[C]//Proc of the 14th Int Conf on TOOLS and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2008:351-366
[9] Majumdar R, Xu Rugang. Reducing test inputs using information partitions[C]//Proc of the 21st Int Conf on Computer Aided Verification.Berlin:Springer,2009:555-569
[10] Chakrabarti A, Godefroid P. Software partitioning for effective automated unit testing[C]//Proc of the 6th Int Conf on Embedded Software.New York:ACM,2006:262-271
[11] Sharir M,Pnueli A.Two Approaches to Interprocedural Dataflow Analysis[M].Englewood:Prentice-Hall,1981:189-234
[12] Reps T, Horwitz S,Sagiv M. Precise interprocedural dataflow analysis via graph reachability[C]//Proc of the22nd ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages.New York:ACM,1995:49-61
[13] Tu Peng, Padua D. Gated SSA-based demand-driven symbolic analysis for parallelizing compilers[C]//Proc of the9th Int Conf on Supercomputing.New York:ACM,1995:414-423
[14] Sen K,Necula G,Gong Liang,et al.MultiSE:Multi-path symbolic execution using value summaries[C]//Proc of the10th Joint Meeting on Foundations of Software Engineering.New York:ACM,2015:842-853
[15] Qi Dawei, Nguyen H D T, Roychoudhury A. Path exploration based on symbolic output[J].ACM Trans on Software Engineering and Methodology,2011,22(4):278-288
[16] Wang Weiguang,Zeng Qingkai,Sun Hao.Dynamic symbolic execution method oriented to critical operation[J].Journal of Software,2016,27(5):1230-1245(in Chinese)(王伟光,曾庆凯,孙浩.面向危险操作的动态符号执行方法[J].软件学报.2016,27(5):1230-1245)
[17] Zhou Yanhong,Wang Tiancheng,Li Huawei,et al.Test generation for multiple target states using path constraint solving[J].Chinese Journal of Computers,2016,39(9):1829-1842(in Chinese)(周艳红,王天成,李华伟,等.基于路径约束求解的多目标状态激励生成方法[J].计算机学报,2016,39(9):1829-1842)
[18] Qin Xiaojun,Zhou Lin,Chen Zuoning,et al.Software vulnerable trace’s solving algorithm based on lazy symbolic execution[J].Chinese Journal of Computers,2015,38(11):2290-2300(in Chinese)(秦晓军,周林,陈左宁,等.基于懒符号执行的软件脆弱性路径求解算法[J].计算机学报,2015,38(11):2290-2300)
[19] Gyimothy T,Beszedes A,Forgacs I.An efficient relevant slicing method for debugging[C]//Proc of the 7th Int Symp on Foundations of Software Engineering.New York:ACM,1999:303-321
[2] Godefroid P.Compositional dynamic test generation[C]//Proc of the 34th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages.New York:ACM,2007:47-54
[3] Avgerinos T,Rebert A,Cha S K,et al.Enhancing symbolic execution with veritesting[C]//Proc of the 36th Int Conf on Software Engineering.New York:ACM,2014:1083-1094
[4] Godefroid P,Nori A V,Rajamani S K,et al.Compositional may-must program analysis:Unleashing the power of alternation[C]//Proc of the 37th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages.New York:ACM,2010:43-56
[5] Wang Chong,LüYinrun,Chen Li,et al.Survey on development of solving methods and state-of-the-art application of satisfiability modulo theories[J].Journal of Computer Research and Development,2017,54(7):1405-1425(in Chinese)(王翀,吕荫润,陈力,等.SMT求解技术的发展及最新应用研究综述[J].计算机研究与发展,2017,54(7):1405-1425)
[6] Torlak E,Bodik R.A lightweight symbolic virtual machine for solver-aided host languages[J]. ACM SIGPLAN Notices,2014,49(6):530-541
[7] Visser W,Reanu C S,Nek R.Test input generation for java containers using state matching[C]//Proc of the 5th Int Symp on Software Testing and Analysis.New York:ACM,2006:37-48
[8] Boonstoppel P,Cadar C,Engler D.RWset:Attacking path explosion in constraint-based test generation[C]//Proc of the 14th Int Conf on TOOLS and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2008:351-366
[9] Majumdar R, Xu Rugang. Reducing test inputs using information partitions[C]//Proc of the 21st Int Conf on Computer Aided Verification.Berlin:Springer,2009:555-569
[10] Chakrabarti A, Godefroid P. Software partitioning for effective automated unit testing[C]//Proc of the 6th Int Conf on Embedded Software.New York:ACM,2006:262-271
[11] Sharir M,Pnueli A.Two Approaches to Interprocedural Dataflow Analysis[M].Englewood:Prentice-Hall,1981:189-234
[12] Reps T, Horwitz S,Sagiv M. Precise interprocedural dataflow analysis via graph reachability[C]//Proc of the22nd ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages.New York:ACM,1995:49-61
[13] Tu Peng, Padua D. Gated SSA-based demand-driven symbolic analysis for parallelizing compilers[C]//Proc of the9th Int Conf on Supercomputing.New York:ACM,1995:414-423
[14] Sen K,Necula G,Gong Liang,et al.MultiSE:Multi-path symbolic execution using value summaries[C]//Proc of the10th Joint Meeting on Foundations of Software Engineering.New York:ACM,2015:842-853
[15] Qi Dawei, Nguyen H D T, Roychoudhury A. Path exploration based on symbolic output[J].ACM Trans on Software Engineering and Methodology,2011,22(4):278-288
[16] Wang Weiguang,Zeng Qingkai,Sun Hao.Dynamic symbolic execution method oriented to critical operation[J].Journal of Software,2016,27(5):1230-1245(in Chinese)(王伟光,曾庆凯,孙浩.面向危险操作的动态符号执行方法[J].软件学报.2016,27(5):1230-1245)
[17] Zhou Yanhong,Wang Tiancheng,Li Huawei,et al.Test generation for multiple target states using path constraint solving[J].Chinese Journal of Computers,2016,39(9):1829-1842(in Chinese)(周艳红,王天成,李华伟,等.基于路径约束求解的多目标状态激励生成方法[J].计算机学报,2016,39(9):1829-1842)
[18] Qin Xiaojun,Zhou Lin,Chen Zuoning,et al.Software vulnerable trace’s solving algorithm based on lazy symbolic execution[J].Chinese Journal of Computers,2015,38(11):2290-2300(in Chinese)(秦晓军,周林,陈左宁,等.基于懒符号执行的软件脆弱性路径求解算法[J].计算机学报,2015,38(11):2290-2300)
[19] Gyimothy T,Beszedes A,Forgacs I.An efficient relevant slicing method for debugging[C]//Proc of the 7th Int Symp on Foundations of Software Engineering.New York:ACM,1999:303-321