Similar Execution Path Generation Based on Backward Symbolic Analysis

Abstract:

Similar execution paths generation is one of the fundamental tasks in code analysis and detection. The current methods usually target to the program behavior or program structure, and change the value of key predicates, but these methods has a low effectiveness due to the lack of the necessary guidance information, Meanwhile, the predicates set has a large size and usually hard to solve, thus it will reduce the analyze precision as well. A technique of similar execution paths generation based on dynamic synergy bidirectional mapping is proposed in this paper. According to extend the shape of Control Flow Graph and use the backward symbolic analysis, the weakest precondition of the candidate path is generated, which can be used as the guidance information to generate pointed similar execution paths set according to the edit distance via changing the distance factor. The experimental results show that this method has the advantage of precision and anti-inference.

• Periodical: Applied Mechanics and Materials (Volume 533)
• Pages: 427-431
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.533.427
• Online since: February 2014
• Authors: Xi Guo, Jian Yong Wang*
• Keywords: Control Flow Graph, Dynamic Analysis, Similar Execution Path, Symbolic Execution, Weakest Precondition

References

[1] Nipkow T, Paulson L. Isabelle/ HOL: A proof assistant for higher-order logic. Lecture Notes in Computer Science, volume 2283 of LNCS. Springer, (2002).

[2] Cruz J. Constraint Reasoning for Differential Models. Amsterdam: The IOS Press, (2005).

[3] Clarke M, Grumberg O, Peled D. ModelChecking. Massachusetts: The MIT Press, (1999).

[4] Flanagan C, Leino K, Lillibridge M, Nelson G, Saxe JB, Stata R. Extended static checking for Java/Proceedings of the 23rd International Conference on Programming language design and implementation(PLDI 2002). New York, USA, 2002: 234−245.

DOI: 10.1145/512529.512558

[5] Ball T, Rajamani S. Automatically validating temporal safety properties of interfaces/ Proceedings of the 8th International SPIN workshop on Model Checking of Software (SPIN 2001). Toronto, Canada, 2001: 102−122.

DOI: 10.1007/3-540-45139-0_7

[6] Henzinger T, Jhala R, Majumdar R, Sutre G. Software Verification with BLAST/Proceedings of the 10th International SPIN Workshop on Model Checking of Software (SPIN 2003). Portland, USA, 2003: 235−239.

DOI: 10.1007/3-540-44829-2_17

[7] Engler D, Chelf B, Chou A, Hallem S. Checking system rules using system-specific, programmer-written compiler extensions/Proceedings of the 4th symposium on Operating System Design and Implementation(OSDI 2000). New York, USA, 2000. 2-11.

DOI: 10.21236/ada419626

[8] Manevich R, Sridharan M, Adams S. PSE: explaining program failures viapostmortemstaticanalysis/Proceedings of the 7th FundamentalApproaches to Software Engineering (FASE 2004). Barcelona, Spain, 2004: 63-72.

DOI: 10.1145/1041685.1029907

[9] Zhongxian G, Earl T, David J. Has the bug really been fixed/Proceedings of the 32nd Conference on International Conference on Software Engineering (ICSE 2010). Cape Town, South Africa, 2010: 55-64.