Advertisement

Concolic Testing Heap-Manipulating Programs

  • Long H. PhamEmail author
  • Quang Loc Le
  • Quoc-Sang Phan
  • Jun Sun
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on numeric programs. Heap-manipulating programs make extensive use of complex heap objects like trees and lists. Testing such programs is challenging due to multiple reasons. Firstly, test inputs for such programs are required to satisfy non-trivial constraints which must be specified precisely. Secondly, precisely encoding and solving path conditions in such programs are challenging and often expensive. In this work, we propose the first concolic testing engine called CSF for heap-manipulating programs based on separation logic. CSF effectively combines specification-based testing and concolic execution for test input generation. It is evaluated on a set of challenging heap-manipulating programs. The results show that CSF generates valid test inputs with high coverage efficiently. Furthermore, we show that CSF can be potentially used in combination with precondition inference tools to reduce the user effort.

Notes

Acknowledgments

This research is supported by MOE research grant MOE2016-T2-2-123.

References

  1. 1.
  2. 2.
    Facebook Infer. https://fbinfer.com/
  3. 3.
  4. 4.
  5. 5.
  6. 6.
  7. 7.
  8. 8.
  9. 9.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: Frankl, P.G. (ed.) ISSTA 2002, pp. 123–133. ACM (2002).  https://doi.org/10.1145/566172.566191
  10. 10.
    Braione, P., Denaro, G., Mattavelli, A., Pezzè, M.: Combining symbolic execution and search-based testing for programs with complex heap inputs. In: Bultan, T., Sen, K. (eds.) ISSTA 2017, pp. 90–101. ACM (2017).  https://doi.org/10.1145/3092703.3092715
  11. 11.
    Braione, P., Denaro, G., Pezzè, M.: Symbolic execution of programs with heap inputs. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) FSE 2015, pp. 602–613. ACM (2015).  https://doi.org/10.1145/2786805.2786842
  12. 12.
    Braione, P., Denaro, G., Pezzè, M.: JBSE: A symbolic executor for Java programs with complex heap inputs. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) FSE 2016, pp. 1018–1022. ACM (2016).  https://doi.org/10.1145/2950290.2983940
  13. 13.
    Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. JACM 58(6), 26:1–26:66 (2011).  https://doi.org/10.1145/2049697.2049700CrossRefMathSciNetzbMATHGoogle Scholar
  14. 14.
    Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006–1036 (2012).  https://doi.org/10.1016/j.scico.2010.07.004CrossRefzbMATHGoogle Scholar
  15. 15.
    Deng, X., Lee, J., Robby: Bogor/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE 2006, pp. 157–166. IEEE Computer Society (2006).  https://doi.org/10.1109/ASE.2006.26
  16. 16.
    Deng, X., Robby, Hatcliff, J.: Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In: SEFM 2007. IEEE Computer Society (2007).  https://doi.org/10.1109/SEFM.2007.43
  17. 17.
    Dennis, G.D.: TSAFE : building a trusted computing base for air traffic control software. Master’s thesis, Massachusetts Institute of Technology, USA (2003)Google Scholar
  18. 18.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) PLDI 2005, pp. 213–223. ACM (2005).  https://doi.org/10.1145/1065010.1065036
  19. 19.
    Godefroid, P., Levin, M.Y., Molnar, D.: SAGE: whitebox fuzzing for security testing. Queue 10(1), 20:20–20:27 (2012).  https://doi.org/10.1145/2090147.2094081CrossRefGoogle Scholar
  20. 20.
    Heimdahl, M.P.E., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J.: Auto-generating test sequences using model checkers: a case study. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 42–59. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24617-6_4CrossRefGoogle Scholar
  21. 21.
    Hillery, B., Mercer, E., Rungta, N., Person, S.: Exact heap summaries for symbolic execution. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 206–225. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49122-5_10CrossRefGoogle Scholar
  22. 22.
    Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 327–341. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-46002-0_23CrossRefzbMATHGoogle Scholar
  23. 23.
    Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Hankin, C., Schmidt, D. (eds.) POPL 2001, pp. 14–26. ACM (2001).  https://doi.org/10.1145/360204.375719
  24. 24.
    Jayaraman, K., Harvison, D., Ganesh, V., Kiezun, A.: jFuzz: a concolic whitebox fuzzer for Java. In: Denney, E., Giannakopoulou, D., Pasareanu, C.S. (eds.) NFM 2009, pp. 121–125 (2009)Google Scholar
  25. 25.
    Khurshid, S., Pǎsǎreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36577-X_40CrossRefzbMATHGoogle Scholar
  26. 26.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976).  https://doi.org/10.1145/360248.360252CrossRefMathSciNetzbMATHGoogle Scholar
  27. 27.
    Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52–68. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_4CrossRefGoogle Scholar
  28. 28.
    Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382–404. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41528-4_21CrossRefGoogle Scholar
  29. 29.
    Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 41–60. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89960-2_3CrossRefGoogle Scholar
  30. 30.
    Le, Q.L., Tatsuta, M., Sun, J., Chin, W.-N.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 495–517. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_26CrossRefGoogle Scholar
  31. 31.
    Le, X.D., Le, Q.L., Lo, D., Le Goues, C.: Enhancing automated program repair with deductive verification. In: ICSME 2016, pp. 428–432. IEEE Computer Society (2016).  https://doi.org/10.1109/ICSME.2016.66
  32. 32.
    Luckow, K., et al.: JDart: a dynamic symbolic analysis framework. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 442–459. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_26CrossRefGoogle Scholar
  33. 33.
    Marinescu, P.D., Cadar, C.: Make test-zesti: a symbolic execution solution for improving regression testing. In: Glinz, M., Murphy, G.C., Pezzè, M. (eds.) ICSE 2012, pp. 716–726. IEEE Computer Society (2012).  https://doi.org/10.1109/ICSE.2012.6227146
  34. 34.
    Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE 2001, pp. 22–31. IEEE Computer Society (2001).  https://doi.org/10.1109/ASE.2001.989787
  35. 35.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Enhancing symbolic execution of heap-based programs with separation logic for test input generation. In: ATVA 2019. To appearGoogle Scholar
  36. 36.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Testing heap-based programs with Java StarFinder. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) ICSE 2018, pp. 268–269. ACM (2018).  https://doi.org/10.1145/3183440.3194964
  37. 37.
    Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773–789. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_54CrossRefGoogle Scholar
  38. 38.
    Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE Computer Society (2002).  https://doi.org/10.1109/LICS.2002.1029817
  39. 39.
    Santos, J.F., Maksimović, P., Sampaio, G., Gardner, P.: JaVerT 2.0: compositional symbolic execution for JavaScript. PACMPL 3(POPL), 66:1–66:31 (2019).  https://doi.org/10.1145/3290379CrossRefGoogle Scholar
  40. 40.
    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H.C. (eds.) FSE 2005, pp. 263–272. ACM (2005).  https://doi.org/10.1145/1081706.1081750
  41. 41.
    Stephens, N., et al.: Driller: augmenting fuzzing through selective symbolic execution. In: NDSS 2016. The Internet Society (2016)Google Scholar
  42. 42.
    Tanno, H., Zhang, X., Hoshino, T., Sen, K.: TesMa and CATG: automated test generation tools for models of enterprise applications. In: Bertolino, A., Canfora, G., Elbaum, S.G. (eds.) ICSE 2015, pp. 717–720. IEEE Computer Society (2015).  https://doi.org/10.1109/ICSE.2015.231
  43. 43.
    Tillmann, N., de Halleux, J.: Pex–white box test generation for.NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-79124-9_10CrossRefGoogle Scholar
  44. 44.
    Vanoverberghe, D., Tillmann, N., Piessens, F.: Test input generation for programs with pointers. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 277–291. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00768-2_25CrossRefGoogle Scholar
  45. 45.
    Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test input generation with java PathFinder. In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA 2004, pp. 97–107. ACM (2004).  https://doi.org/10.1145/1007512.1007526
  46. 46.
    Wang, X., Sun, J., Chen, Z., Zhang, P., Wang, J., Lin, Y.: Towards optimal concolic testing. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) ICSE 2018, pp. 291–302 (2018).  https://doi.org/10.1145/3180155.3180177
  47. 47.
    Yun, I., Lee, S., Xu, M., Jang, Y., Kim, T.: QSYM : a practical concolic execution engine tailored for hybrid fuzzing. In: Enck, W., Felt, A.P. (eds.) USENIX Security 2018, pp. 745–761. USENIX Association (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Long H. Pham
    • 1
    Email author
  • Quang Loc Le
    • 2
  • Quoc-Sang Phan
    • 3
  • Jun Sun
    • 4
  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.School of Computing & Digital TechnologiesTeesside UniversityMiddlesbroughUK
  3. 3.Synopsys, Inc.Mountain ViewUSA
  4. 4.Singapore Management UniversitySingaporeSingapore

Personalised recommendations