nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs

verfasst von : Amirfarhad Nilizadeh, Gary T. Leavens, Corina S. Păsăreanu

Erschienen in: Tests and Proofs

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Software is widely used in critical systems. Thus, it is important that developers can quickly find semantic bugs with testing; however, semantic bugs can only be revealed by tests that use valid inputs. Guided fuzzers can create input tests that cover all branches; however, they may not necessarily cover all branches with valid inputs. Therefore, the problem is how to guide a fuzzer to cover all branches in a program with only valid inputs. We perform a study of an idea that guarantees that all inputs generated by a guided fuzzer that reach the program under test are valid using formal specifications and runtime assertion checking. Our results show that this idea improves the feedback given to a guided fuzzer.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Generating Timed UI Tests from Counterexamples

Nächstes Kapitel FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs

An assertion is trivial if it is always true.

Our study used an Intel i7-3770 CPU @ 3.40 GHz with 15 GB of RAM.

Ahrendt, W., Gladisch, C., Herda, M.: Proof-based test case generation. Deductive Software Verification – The KeY Book. LNCS, vol. 10001, pp. 415–451. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6_12CrossRef

Artho, C., et al.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2–3), 209–234 (2005)MathSciNetCrossRef

Banks, G., Cova, M., Felmetsger, V., Almeroth, K., Kemmerer, R., Vigna, G.: SNOOZE: toward a Stateful NetwOrk prOtocol fuzZEr. In: Katsikas, S.K., López, J., Backes, M., Gritzalis, S., Preneel, B. (eds.) ISC 2006. LNCS, vol. 4176, pp. 343–358. Springer, Heidelberg (2006). https://doi.org/10.1007/11836810_25CrossRef

Bardin, S., Kosmatov, N., Marre, B., Mentré, D., Williams, N.: Test case generation with PathCrawler/LTest: how to automate an industrial testing process. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 104–120. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03427-6_12CrossRef

Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. ACM SIGSOFT Softw. Eng. Notes 27(4), 123–133 (2002)CrossRef

Brucker, A.D., Wolff, B.: Symbolic test case generation for primitive recursive functions. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 16–32. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31848-4_2CrossRef

BuggyJavaJML. https://github.com/Amirfarhad-Nilizadeh/BuggyJavaJML. Accessed 05 May 2021

Bürdek, J., et al.: Facilitating reuse in multi-goal test-suite generation for software product lines. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 84–99. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46675-9_6CrossRef

Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transfer 7(3), 212–232 (2005). https://doi.org/10.1007/s10009-004-0167-4CrossRef

10.

Cadar, C., et al.: Symbolic execution for software testing in practice: preliminary assessment. In: 2011 33rd International Conference on Software Engineering (ICSE), pp. 1066–1071. IEEE (2011)

11.

Cha, S.K., Avgerinos, T., Rebert, A., Brumley, D.: Unleashing mayhem on binary code. In: 2012 IEEE Symposium on Security and Privacy, pp. 380–394. IEEE (2012)

12.

Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_16CrossRef

13.

Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: the JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 231–255. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47993-7_10CrossRef

14.

Cheon, Y., Leavens, G.T.: The JML and JUnit way of unit testing and its implementation. Technical report TR# 04–02a, Department of Computer Science (2004)

15.

Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006)CrossRef

16.

Cok, D.R.: Improved usability and performance of SMT solvers for debugging specifications. Int. J. Softw. Tools Technol. Transfer 12(6), 467–481 (2010). https://doi.org/10.1007/s10009-010-0138-xCrossRef

17.

Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35CrossRef

18.

Corina, J., et al.: DIFUZE: interface aware fuzzing for kernel drivers. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 2123–2138 (2017)

19.

Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)MathSciNetCrossRef

20.

Fraser, G., Arcuri, A.: EvoSuite: automatic test suite generation for object-oriented software. In: Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, pp. 416–419 (2011)

21.

Fraser, G., Arcuri, A.: EvoSuite: on the challenges of test case generation in the real world. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, pp. 362–369. IEEE (2013)

22.

Fraser, G., Arcuri, A.: A large-scale evaluation of automated unit test generation using evosuite. ACM Trans. Softw. Eng. Methodol. (TOSEM) 24(2), 1–42 (2014)CrossRef

23.

Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, vol. 1, pp. 225–234 (2010)

24.

Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 213–223 (2005)

25.

Godefroid, P., Peleg, H., Singh, R.: Learn&Fuzz: machine learning for input fuzzing. In: 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 50–59. IEEE (2017)

26.

Groce, A., Pinto, J.: A little language for testing. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 204–218. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_15CrossRef

27.

Groce, A., Pinto, J., Azimi, P., Mittal, P.: TSTL: a language and tool for testing. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, pp. 414–417 (2015)

28.

Hoffmann, M.R., Mandrikov, E., Friedenhagen, M.: Java Code Coverage for Eclipse. https://www.eclemma.org/jacoco/. Accessed 05 May 2021

29.

Holmes, J., et al.: TSTL: the template scripting testing language. Int. J. Softw. Tools Technol. Transfer 20(1), 57–78 (2016). https://doi.org/10.1007/s10009-016-0445-yCrossRef

30.

Google Inc., et al.: Google/syzkaller. https://github.com/google/syzkaller. Accessed 05 May 2021

31.

Java-JML. https://github.com/Amirfarhad-Nilizadeh/Java-JML. Accessed 05 May 2021

32.

Johansson, W., Svensson, M., Larson, U.E., Almgren, M., Gulisano, V.: T-Fuzz: model-based fuzzing for robustness testing of telecommunication protocols. In: 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation, pp. 323–332. IEEE (2014)

33.

Kersten, R., Luckow, K., Păsăreanu, C.S.: POSTER: AFL-based fuzzing for Java with Kelinci. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 2511–2513 (2017)

34.

Kosmatov, N., Maurica, F., Signoles, J.: Efficient runtime assertion checking for properties over mathematical numbers. In: Deshmukh, J., Ničković, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 310–322. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-60508-7_17CrossRef

35.

Kwong, G., Ruderman, J., Carette, A.: MozillaSecurity/funfuzz. https://github.com/MozillaSecurity/funfuzz. Accessed 05 May 2021

36.

Le, X.B.D., Pasareanu, C., Padhye, R., Lo, D., Visser, W., Sen, K.: SAFFRON: adaptive grammar-based fuzzing for worst-case analysis. ACM SIGSOFT Softw. Eng. Notes 44(4), 14–14 (2019)CrossRef

37.

Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. SECS, vol. 523, pp. 175–188. Springer, Boston (1999). https://doi.org/10.1007/978-1-4615-5229-1_12CrossRef

38.

Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)CrossRef

39.

Leavens, G.T., Cheon, Y.: Design by contract with JML (2006). https://www.cs.ucf.edu/~leavens/JML//jmldbc.pdf

40.

Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1–3), 185–208 (2005)MathSciNetCrossRef

41.

Leavens, G.T., Ruby, C., Leino, K.R.M., Poll, E., Jacobs, B.: JML (poster session) notations and tools supporting detailed design in JAVA. In: Addendum to the 2000 Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (Addendum), pp. 105–106 (2000)

42.

Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 78(5), 293–303 (2009)CrossRef

43.

Li, J., Zhao, B., Zhang, C.: Fuzzing: a survey. Cybersecurity 1(1) (2018). Article number: 6. https://doi.org/10.1186/s42400-018-0002-y

44.

Liang, H., Pei, X., Jia, X., Shen, W., Zhang, J.: Fuzzing: state of the art. IEEE Trans. Reliab. 67(3), 1199–1218 (2018)CrossRef

45.

Ly, D., Kosmatov, N., Loulergue, F., Signoles, J.: Verified runtime assertion checking for memory properties. In: Ahrendt, W., Wehrheim, H. (eds.) TAP 2020. LNCS, vol. 12165, pp. 100–121. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50995-8_6CrossRef

46.

Meinke, K., Sindhu, M.A.: LBTest: a learning-based testing tool for reactive systems. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, pp. 447–454. IEEE (2013)

47.

Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: a tool for generating structurally complex test inputs. In: 29th International Conference on Software Engineering (ICSE 2007), pp. 771–774. IEEE (2007)

48.

Nagy, S., Hicks, M.: Full-speed fuzzing: reducing fuzzing overhead through coverage-guided tracing. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 787–802. IEEE (2019)

49.

Nguyen, H.A., Dyer, R., Nguyen, T.N., Rajan, H.: Mining preconditions of APIs in large-scale code corpus. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 166–177 (2014)

50.

Nilizadeh, A.: JMLKelinci. http://github.com/Amirfarhad-Nilizadeh/JMLKelinci. Accessed 05 May 2021

51.

Nilizadeh, A., Leavens, G., Le, X.B., Pasareanu, C., Cok, D.: Exploring true test overfitting in dynamic automated program repair using formal methods. In: 2021 14th IEEE Conference on Software Testing, Validation and Verification (ICST). IEEE (2021)

52.

Nilizadeh, S., Noller, Y., Pasareanu, C.S.: DifFuzz: differential fuzzing for side-channel analysis. In: 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE), pp. 176–187. IEEE (2019)

53.

Noller, Y., Kersten, R., Păsăreanu, C.S.: Badger: complexity analysis with fuzzing and symbolic execution. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 322–332 (2018)

54.

Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for Java. In: Companion to the 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications Companion, pp. 815–816 (2007)

55.

Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: 29th International Conference on Software Engineering (ICSE 2007), pp. 75–84. IEEE (2007)

56.

Peters, D., Parnas, D.L.: Generating a test oracle from program documentation: work in progress. In: Proceedings of the 1994 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 58–65 (1994)

57.

Rajpal, M., Blum, W., Singh, R.: Not all bytes are equal: neural byte sieve for fuzzing. arXiv preprint arXiv:1711.04596 (2017)

58.

Rawat, S., Jain, V., Kumar, A., Cojocar, L., Giuffrida, C., Bos, H.: VUzzer: application-aware evolutionary fuzzing. In: NDSS, vol. 17, pp. 1–14 (2017)

59.

Stephens, N., et al.: Driller: augmenting fuzzing through selective symbolic execution. In: NDSS, vol. 16, pp. 1–16 (2016)

60.

Visser, W., Geldenhuys, J.: COASTAL: combining concolic and fuzzing for Java (competition contribution). In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12079, pp. 373–377. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_23CrossRef

61.

Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test input generation with Java pathfinder. In: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 97–107 (2004)

62.

Wang, T., Wei, T., Gu, G., Zou, W.: TaintScope: a checksum-aware directed fuzzing tool for automatic software vulnerability detection. In: 2010 IEEE Symposium on Security and Privacy, pp. 497–512. IEEE (2010)

63.

Wang, X., Hu, C., Ma, R., Li, B., Wang, X.: LAFuzz: neural network for efficient fuzzing. In: 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI), pp. 603–611. IEEE (2020)

64.

Xu, G., Yang, Z.: JMLAutoTest: a novel automated testing framework based on JML and JUnit. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 70–85. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24617-6_6CrossRef

65.

Yue, T., Tang, Y., Yu, B., Wang, P., Wang, E.: LearnAFL: greybox fuzzing with knowledge enhancement. IEEE Access 7, 117029–117043 (2019)CrossRef

66.

Zalewski, M.: Technical “whitepaper” for afl-fuzz (2014). http://lcamtuf.coredump.cx/afl/technical_details.txt

67.

Zimmerman, D.M., Nagmoti, R.: JMLUnit: the next generation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 183–197. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18070-5_13CrossRef

Titel: Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs
verfasst von: Amirfarhad Nilizadeh
Gary T. Leavens
Corina S. Păsăreanu
Verlag: Springer International Publishing
Buch: Tests and Proofs
Print ISBN: 978-3-030-79378-4

Electronic ISBN: 978-3-030-79379-1

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-79379-1_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner