Program Symbol Value Analysis Based on Dependent Condition Reconstruction

doi:10.3969/j.issn.0372-2112.2019.03.016

PDF(2268 KB)

ACTA ELECTRONICA SINICA ›› 2019, Vol. 47 ›› Issue (3) : 630-635. DOI: 10.3969/j.issn.0372-2112.2019.03.016

Program Symbol Value Analysis Based on Dependent Condition Reconstruction

GUO Xi¹, WANG Pan²

Author information +

History +

Abstract

Symbolic execution is of vital importance for software engineering activities,such as path exploration,debugging and verification.However,symbolic execution techniques do not scale well for complicated realistic programs,because the number of feasible executions paths increases exponentially.Path condition expression extracting and constraint solving are the bottlenecks of symbolic execution.State merging is a common method to tackle the problem of state explosion,but this abstract procedure would be prone to incorrect path information.According to different searching strategy of symbolic engine,symbolic execution tools could generate unsolved path conditions during the process of symbolic variable state combination.A symbol value analysis based on dependent condition reconstruction method is proposed,which analysize the logic path conditions and extracts the common variable symbols to enhance the combination efficiency.Meanwhile,the backward analysis method is used to generate dependent condition set to improve the accuracy of path analysis.The experimental results demonstrate that it has better execution efficiency and accuracy compare to the tradition state combination methods.

Key words

program analysis / symbolic execution / related dependency / constrain solving

Cite this article

EndNote

Ris (Procite)

Bibtex

Download Citations

GUO Xi, WANG Pan. Program Symbol Value Analysis Based on Dependent Condition Reconstruction[J]. Acta Electronica Sinica, 2019, 47(3): 630-635. https://doi.org/10.3969/j.issn.0372-2112.2019.03.016

References

[1] KUZNETSOV V,KINDER J,BUCUR S,et al.Efficient state merging in symbolic excution[J].ACM SIGPLAN Notices,2012,47(6):193-204.
[2] GODEFROID P.Compositional dynamic test generation[A].Proceeding of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,2007.47-54.
[3] AVGERINOS T,REBERT A,CHA S K,et al.Enhancing symbolic execution with veritesting[A].Proceeding of the 36th International Conference on Software Engineering[C].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[A].Proceeding of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,2010.43-56.
[5] TORLAK E,BODIK R.A lightweight symbolic virtual machine for solver-aided host languages[J].ACM SIGPLAN Notices,2014,49(6):530-541.
[6] VISSER W,REANU C S,NEK R.Test input generation for java containers using state matching[A].Proceeding of the 5th International Symposium on Software Testing and Analysis[C].New York:ACM,2006.37-48.
[7] BOONSTOPPEL P,CADAR C,ENGLER D.RWset:Attacking path explosion in constraint-based test generation[A].Proceeding of the 14th International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems[C].Berlin:Springer,2008.351-366.
[8] SHARIR M,PNUELI A.Two Approaches to Interprocedural Dataflow Analysis[M].Englewood:Prentice-Hall,1981.189-234.
[9] REPS T,HORWITZ S,SAGIV M.Precise interprocedural dataflow analysis via graph reachability[A].Proceeding of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,1995.49-61.
[10] SEN K,NECULA G,GONG Liang,et al.MultiSE:Multi-path symbolic execution using value summaries[A].Proceeding of the 10th Joint Meeting on Foundations of Software Engineering[C].New York:ACM,2015.842-853.
[11] QI Dawei,NGUYEN H T,ROYCHOUDHURY A.Path exploration based on symbolic output[J].ACM Transaction on Software Engineering and Methodology,2011,22(4):278-288.
[12] 王伟光,曾庆凯,孙浩.面向危险操作的动态符号执行方法[J].软件学报,2016,27(5):1230-1245.WANG Wei-guang,ZENG Qing-kai,SUN Hao.Dynamic symbolic execution method oriented to critical operation[J].Journal of Software,2016,27(5):1230-1245.(in Chinese)
[13] 周艳红,王天成,李华伟,等.基于路径约束求解的多目标状态激励生成方法[J].计算机学报,2016,39(9):1829-1842.ZHOU Yan-hong,WANG Tian-cheng,LI Hua-wei,et al.Test generation for multiple target states using path constraint solving[J].Chinese Journal of Computers.2016,39(9):1829-1842.(in Chinese)
[14] 秦晓军,周林,陈左宁,等.基于懒符号执行的软件脆弱性路径求解算法[J].计算机学报,2015,38(11):2290-2300.QIN Xiao-jun,ZHOU Lin,CHEN Zuo-ning,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)
[15] 王红阳,姜淑娟,王兴亚,鞠小林,张艳梅.基于子路径扩展的不可达路径检测方法[J].电子学报,2015,43(8):1555-1560.WANG Hong-yang,JIANG Shu-juan,WANG Xing-ya,JU Xiao-lin,ZHANG Yan-mei.An approach for detecting infeasible paths based on sub-path expansion[J].Acta Electronica Sinica,2015,43(8):1555-1560.(in Chinese)