Symbolic verification of regular properties

ABSTRACT

Verifying the regular properties of programs has been a significant challenge. This paper tackles this challenge by presenting symbolic regular verification (SRV) that offers significant speedups over the state-of-the-art. SRV is based on dynamic symbolic execution (DSE) and enabled by novel techniques for mitigating path explosion: (1) a regular property-oriented path slicing algorithm, and (2) a synergistic combination of property-oriented path slicing and guiding. Slicing prunes redundant paths, while guiding boosts the search for counterexamples. We have implemented SRV for Java and evaluated it on 15 real-world open-source Java programs (totaling 259K lines of code). Our evaluation results demonstrate the effectiveness and efficiency of SRV. Compared with the state-of-the-art --- pure DSE, pure guiding, and pure path slicing --- SRV achieves average speedups of more than 8.4X, 8.6X, and 7X, respectively, making symbolic regular property verification significantly more practical.

References

1. A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools Addison-Wesley, 1986.
2. C. Allan, P. Avgustinov, A. S. Christensen, L. J. Hendren, S. Kuzins, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. Adding trace matching with free variables to AspectJ. In OOPSLA, pages 345--364, 2005.
3. D. Babić, L. Martignoni, S. McCamant, and D. Song. Statically-directed dynamic automated test generation. In ISSTA, pages 12--22. ACM, 2011.
4. T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3, 2002.
5. T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI, pages 203--213, 2001.
6. S. M. Blackburn, R. Garner, C. Hoffmann, A. M. Khang, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, et al. The DaCapo benchmarks: Java benchmarking development and analysis. In OOPSLA, pages 169--190, 2006.
7. E. Bodden. Efficient hybrid typestate analysis by determining continuation-equivalent states. In ICSE, pages 5--14, 2010.
8. P. Boonstoppel, C. Cadar, and D. Engler. RWset: Attacking path explosion in constraint-based test generation. In TACAS, pages 351--366, 2008.
9. J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In AŞE pages 443--446, 2008.
10. C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209--224, 2008.
11. S. Chandra, S. J. Fink, and M. Sridharan. Snugglebug: a powerful approach to weakest preconditions. In PLDI, pages 363--374, 2009.
12. F. Chen and G. Rosu. MOP: an efficient and generic runtime verification framework. In OOPSLA, pages 569--588, 2007.
13. M. Christakis, P. Müller, and V. Wüstholz. Guiding dynamic symbolic execution toward unverified program executions. In ICSE, pages 144--155, 2016.
14. E. M. Clarke, O. Grumberg, and D. Peled. Model checking. MIT press, 1999.
15. Clemens Hammacher, Martin Burger, and Valentin Dallmeier. JavaSlicer. https://www.st.cs.uni-saarland.de/javaslicer/, 2008.
16. H. Cui, G. Hu, J. Wu, and J. Yang. Verifying systems rules using rule-directed symbolic execution. In ASPLOS, pages 329--342, 2013.
17. M. Das, S. Lerner, and M. Seigle. ESP: path-sensitive program verification in polynomial time. In PLDI, pages 57--68, 2002.
18. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In ICSE, pages 411--420, 1999.
19. D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as deviant behavior: A general approach to inferring errors in systems code. In SOSP, pages 57--72, 2001.
20. D. R. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI, pages 1--16, 2000.
21. S. J. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. In ISSTA, pages 133--144, 2006.
22. A. Gill et al. Introduction to the theory of finite-state machines. 1962.
23. P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In PLDI, pages 213--223, 2005.
24. IBM. T.J. Watson Libraries for Analysis (WALA). http://wala.sf.net/.
25. J. Jaffar, V. Murali, and J. A. Navas. Boosting concolic testing via interpolation. In FSE, pages 48--58, 2013.
26. K. Jayaraman, D. Harvison, V. Ganesh, and A. Kiezun. jFuzz: A concolic whitebox fuzzer for Java. In NASA Formal Methods, pages 121--125, 2009.
27. R. Jhala and R. Majumdar. Path slicing. In PLDI, pages 38--47, 2005.
28. R. Just, D. Jalali, L. Inozemtseva, M. D. Ernst, R. Holmes, and G. Fraser. Are mutants a valid substitute for real faults in software testing? In FSE, pages 654--665, 2014.
29. U. P. Khedker, A. Sanyal, and B. Sathe. Data Flow Analysis - Theory and Practice. CRC Press, 2009.
30. J. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.
31. M. Leucker and C. Schallhart. A brief account of runtime verification. J. Log. Algebr. Program., 78(5):293--303, 2009.
32. Y. Li, Z. Su, L. Wang, and X. Li. Steering symbolic execution to less traveled paths. In OOPSLA, pages 19--32, 2013.
33. Y. Liu, C. Xu, and S.-C. Cheung. Characterizing and detecting performance bugs for smartphone applications. In ICSE, pages 1013--1024, 2014.
34. K.-K. Ma, K. Y. Phang, J. S. Foster, and M. Hicks. Directed symbolic execution. In SAS, pages 95--111, 2011.
35. P. D. Marinescu and C. Cadar. make test-zesti: A symbolic execution solution for improving regression testing. In ICSE, pages 716--726, 2012.
36. G. J. Myers, C. Sandler, and T. Badgett. The art of software testing. John Wiley & Sons, 2011.
37. F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 2015.
38. A. V. Nori, S. K. Rajamani, S. Tetali, and A. V. Thakur. The YOGI project: Software property checking via static analysis and testing. In TACAS, pages 178--181, 2009.
39. S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. In PLDI, pages 504--515, 2011.
40. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49--61, 1995.
41. K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In FSE, pages 263--272, 2005.
42. H. Seo and S. Kim. How we get there: a context-guided search strategy in concolic testing. In FSE, pages 413--424, 2014.
43. R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE TSE, (1):157--171, 1986.
44. N. Tillmann and J. De Halleux. Pex - white box test generation for .NET. In TAP, pages 134--153, 2008.
45. F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 1995.
46. T. Xie, N. Tillmann, J. de Halleux, and W. Schulte. Fitness-guided path exploration in dynamic symbolic execution. In DSN, pages 359--368, 2009.
47. H. Yu, Z. Chen, Y. Zhang, J. Wang, and W. Dong. RGSE: a regular property guided symbolic executor for java. In FSE, pages 954--958, 2017.
48. C. Zamfir and G. Candea. Execution synthesis: a technique for automated software debugging. In EuroSys, pages 321--334, 2010.
49. Y. Zhang, Z. Chen, J. Wang, W. Dong, and Z. Liu. Regular property guided dynamic symbolic execution. In ICSE, pages 643--653, 2015.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation