Top

Published in:

2021 | OriginalPaper | Chapter

FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs

Authors : Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat, Lucas C. Cordeiro

Published in: Tests and Proofs

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We describe and evaluate a novel approach to automated test generation that exploits fuzzing and Bounded Model Checking (BMC) engines to detect security vulnerabilities in C programs. We implement this approach in a new tool FuSeBMC that explores and analyzes the target C program by injecting labels that guide the engines to produce test cases. FuSeBMC also exploits a selective fuzzer to produce test cases for the labels that fuzzing and BMC engines could not produce test cases. Lastly, we manage each engine’s execution time to improve FuSeBMC’s energy consumption. We evaluate FuSeBMC by analysing the results of its participation in Test-Comp 2021 whose two main categories evaluate a tool’s ability to provide code coverage and bug detection. The competition results show that FuSeBMC performs well compared to the state-of-the-art software testing tools. FuSeBMC achieved 3 awards in the Test-Comp 2021: first place in the Cover-Error category, second place in the Overall category, and third place in the Low Energy Consumption category.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

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

Available only for authorised users

https://gitlab.com/sosy-lab/software/test-format/.

https://github.com/kaled-alshmrany/FuSeBMC.

https://doi.org/10.5281/zenodo.4710599.

Rodriguez, M., Piattini, M., Ebert, C.: Software verification and validation technologies and tools. IEEE Softw. 36(2), 13–24 (2019)CrossRef

Airbus issues software bug alert after fatal plane crash. The Guardian, May 2015. https://tinyurl.com/xw67wtd9. Accessed Mar 2021

Liu, B., Shi, L., Cai, Z., Li, M.: Software vulnerability discovery techniques: a survey. In: 2012 Fourth International Conference on Multimedia Information Networking and Security, pp. 152–156. IEEE (2012)

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking, pp. 196–215 (2008)

Godefroid, P.: Fuzzing: hack, art, and science. Commun. ACM 63(2), 70–76 (2020)CrossRef

Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35746-6_1CrossRef

Shameng, W., Feng Chao, E.A.: Testing network protocol binary software with selective symbolic execution. In: CIS, pp. 318–322. IEEE (2016)

Beyer, D.: 3rd competition on software testing (test-comp 2021) (2021)

Miller, B.P., et al.: Fuzz revisited: a re-examination of the reliability of UNIX utilities and services. Technical report, UW-Madison (1995)

10.

King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRef

11.

Faria, J.: Inspections, revisions and other techniques of software static analysis. Software Testing and Quality, Lecture, vol. 9 (2008)

12.

Qin, S., Kim, H.S.: LIFT: a low-overhead practical information flow tracking system for detecting security attacks. In: MICRO 2006, pp. 135–148. IEEE (2006)

13.

Ognawala, S., Kilger, F., Pretschner, A.: Compositional fuzzing aided by targeted symbolic execution. arXiv preprint arXiv:1903.02981 (2019)

14.

Basak Chowdhury, A., Medicherla, R.K., Venkatesh, R.: VeriFuzz: program aware fuzzing. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 244–249. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_22CrossRef

15.

Le, H.M.: LLVM-based hybrid fuzzing with LibKluzzer (competition contribution). In: FASE, pp. 535–539 (2020)

16.

Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press (2009)

17.

Cordeiro, L.C., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Software Eng. 38(4), 957–974 (2012)CrossRef

18.

Beyer, D.: Second competition on software testing: Test-Comp 2020. In: Wehrheim, H., Cabot, J. (eds.) Fundamental Approaches to Software Engineering. FASE 2020. LNCS, vol. 12076, pp. 505–519. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_25

19.

Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209–224 (2008)

20.

Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16CrossRef

21.

Alshmrany, K.M., Menezes, R.S., Gadelha, M.R., Cordeiro, L.C.: FuSeBMC: a white-box fuzzer for finding security vulnerabilities in c programs. In: 24th International Conference on Fundamental Approaches to Software Engineering (FASE), vol. 12649, pp. 363–367 (2020)

22.

Munea, T.L., Lim, H., Shon, T.: Network protocol fuzz testing for information systems and applications: a survey and taxonomy. Multimedia Tools Appl. 75(22), 14745–14757 (2016)CrossRef

23.

Wang, J., Guo, T., Zhang, P., Xiao, Q.: A model-based behavioral fuzzing approach for network service. In: 2013 Third International Conference on IMCCC, pp. 1129–1134. IEEE (2013)

24.

Baldoni, R., Coppa, E., D’elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51, 1–39 (2018)

25.

Chipounov, V., Georgescu, V., Zamfir, C., Candea, G.: Selective symbolic execution. In: Proceedings of the 5th Workshop on HotDep (2009)

26.

Black, P.E., Bojanova, I.: Defeating buffer overflow: a trivial but dangerous bug. IT Prof. 18(6), 58–61 (2016)CrossRef

27.

Zhang, S., Zhu, J., Liu, A., Wang, W., Guo, C., Xu, J.: A novel memory leak classification for evaluating the applicability of static analysis tools. In: 2018 IEEE International Conference on Progress in Informatics and Computing (PIC), pp. 351–356. IEEE (2018)

28.

Jimenez, W., Mammar, A., Cavalli, A.: Software vulnerabilities, prevention and detection methods: a review. In: Security in Model-Driven Architecture, vol. 215995, p. 215995 (2009)

29.

Boudjema, E.H., Faure, C., Sassolas, M., Mokdad, L.: Detection of security vulnerabilities in C language applications. Secur. Priv. 1(1), e8 (2018)CrossRef

30.

US-CERT: Understanding denial-of-service attacks \(|\) CISA (2009)

31.

Cisco: Cisco IOS XE software cisco discovery protocol memory leak vulnerability (2018)

32.

Clang documentation (2015). http://clang.llvm.org/docs/index.html. Accessed Aug 2019

33.

Rocha, H.O., Barreto, R.S., Cordeiro, L.C.: Hunting memory bugs in C programs with Map2Check. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 934–937. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_64CrossRef

34.

Rocha, H., Menezes, R., Cordeiro, L.C., Barreto, R.: Map2Check: using symbolic execution and fuzzing. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. LNCS, vol. 12079, pp. 403–407. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_29

35.

Gadelha, M.R., Monteiro, F., Cordeiro, L., Nicole, D.: ESBMC v6.0: verifying C programs using k-induction and invariant inference. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 209–213. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_15CrossRef

36.

Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, pp. 888–891 (2018)

37.

Beyer, D., Lemberger, T.: TestCov: robust test-suite execution and coverage measurement. In: 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1074–1077. IEEE (2019)

38.

Lopes, B.C., Auler, R.: Getting started with LLVM core libraries. Packt Publishing Ltd. (2014)

39.

Beyer, D.: Status report on software testing: Test-Comp 2021. In: Guerra, E., Stoelinga, M. (eds.) Fundamental Approaches to Software Engineering FASE 2021. LNCS, vol. 12649, pp. 341–357. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71500-7_17

40.

Beyer, D.: Software verification: 10th comparative evaluation (SV-COMP 2021). In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. LNCS, vol. 12652, pp. 401–422. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_24

41.

Chalupa, M., Novák, J., Strejček, J.: Symbiotic 8: parallel and targeted test generation. FASE 2021. LNCS, vol. 12649, pp. 368–372. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71500-7_20CrossRef

42.

Beyer, D., Wendler, P.: CPU energy meter: a tool for energy-aware algorithms engineering. TACAS 2020. LNCS, vol. 12079, pp. 126–133. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_8CrossRef

43.

Barton, J.H., Czeck, E.W., Segall, Z.Z., Siewiorek, D.P.: Fault injection experiments using fiat. IEEE Trans. Comput. 39(4), 575–582 (1990)CrossRef

44.

Böhme, M., Pham, V.-T., Nguyen, M.-D., Roychoudhury, A.: Directed greybox fuzzing. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 2329–2344 (2017)

45.

American fuzzy lop (2021). https://lcamtuf.coredump.cx/afl/

46.

Serebryany, K.: libFuzzer-a library for coverage-guided fuzz testing. LLVM project (2015)

47.

Gorbunov, S., Rosenbloom, A.: AutoFuzz: automated network protocol fuzzing framework. IJCSNS 10(8), 239 (2010)

48.

Eddington, M.: Peach fuzzing platform. Peach Fuzzer, vol. 34 (2011)

49.

Jaffar, J., Maghareh, R., Godboley, S., Ha, X.-L.: TracerX: dynamic symbolic execution with interpolation (competition contribution). In: FASE, pp. 530–534 (2020)

50.

Song, J., Cadar, C., Pietzuch, P.: SymbexNet: testing network protocol implementations with symbolic execution and rule-based specifications. In: IEEE TSE, vol. 40, no. 7, pp. 695–709 (2014)

51.

Sasnauskas, R., Kaiser, P., Jukić, R.L., Wehrle, K.: Integration testing of protocol implementations using symbolic distributed execution. In: ICNP, pp. 1–6. IEEE (2012)

52.

Le, H.M.: LLVM-based hybrid fuzzing with LibKluzzer (competition contribution). In: Wehrheim, H., Cabot, J. (eds.) Fundamental Approaches to Software Engineering. FASE 2020. LNCS, vol. 12076, pp. 535–539. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_29

53.

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

54.

Pak, B.S.: Hybrid fuzz testing: discovering software bugs via fuzzing and symbolic execution. School of Computer Science Carnegie Mellon University (2012)

55.

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)

56.

Păsăreanu, C.S., Rungta, N.: Symbolic pathfinder: symbolic execution of Java bytecode. In: Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, pp. 179–180 (2010)

57.

Ognawala, S., Hutzelmann, T., Psallida, E., Pretschner, A.: Improving function coverage with munch: a hybrid fuzzing and directed symbolic execution approach. In: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pp. 1475–1482 (2018)

58.

Godefroid, P., Levin, M.Y., Molnar, D.: SAGE: whitebox fuzzing for security testing. Queue 10(1), 20–27 (2012)CrossRef

59.

Wang, M., et al.: SAFL: increasing and accelerating testing coverage with symbolic execution and guided fuzzing. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, pp. 61–64 (2018)

60.

He, J., Balunović, M., Ambroladze, N., Tsankov, P., Vechev, M.: Learning to fuzz from symbolic execution with application to smart contracts. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 531–548 (2019)

61.

Cordeiro, L.C.: SMT-based bounded model checking for multi-threaded software in embedded systems. In: International Conference on Software Engineering, pp. 373–376. ACM (2010)

62.

Pereira, P.A., et al.: Verifying CUDA programs using SMT-based context-bounded model checking. In: Ossowski, S. (ed.) Annual ACM Symposium on Applied Computing, pp. 1648–1653. ACM (2016)

Title: FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs
Authors: Kaled M. Alshmrany
Mohannad Aldughaim
Ahmed Bhayat
Lucas C. Cordeiro
Publisher: Springer International Publishing
Book: Tests and Proofs
Print ISBN: 978-3-030-79378-4

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner