Top

Published in:

2020 | OriginalPaper | Chapter

BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers

Authors : Joseph Scott, Federico Mora, Vijay Ganesh

Published in: Software Verification

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Satisfiability Modulo Theories (SMT) solvers are fundamental tools that are used widely in software engineering, verification, and security research. Precisely because of their widespread use, it is imperative we develop efficient and systematic methods to test them. To this end, we present a reinforcement-learning based fuzzing system, BanditFuzz, that learns grammatical constructs of well-formed inputs that may cause performance slowdown in SMT solvers. To the best of our knowledge, BanditFuzz is the first machine-learning based performance fuzzer for SMT solvers.

BanditFuzz takes the following as input: a grammar G describing well-formed inputs to a set of distinct solvers (say, a target solver T and a reference solver R) that implement the same specification, and a fuzzing objective (e.g., aim to maximize the relative performance difference between T and R). BanditFuzz outputs a list of grammatical constructs that are ranked in descending order by how likely they are to increase the performance difference between solvers T and R. Using BanditFuzz, we constructed two benchmark suites (with 400 floating-point and 300 string instances) that expose performance issues in all considered solvers, namely, Z3, CVC4, Colibri, MathSAT, Z3seq, and Z3str3. We also performed a comparison of BanditFuzz against random, mutation, and evolutionary fuzzing methods and observed up to a 81% improvement based on PAR-2 scores used in SAT competitions. That is, relative to other fuzzing methods considered, BanditFuzz was found to be more efficient at constructing inputs with wider performance margin between a target and a set of reference solvers.

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 Automatic Detection and Repair of Transition- Based Leakage in Software Binaries

next chapter Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison

We use the terms “relative performance fuzzing” and “performance fuzzing” interchangeably in this paper.

The term bandit comes from gambling: the arm of a slot machine is referred to as a one-armed bandit, and multi-arm bandits referred to several slot machines. The goal of the MAB agent is to maximize its reward by playing a sequence of actions (e.g., slot machines).

We use the terms “instance” and “input” interchangeably through this paper.

This is assuming only the RNE rounding mode is allowed, otherwise each of the below expressions could have any valid rounding mode resulting in 20 possible outputs.

Integer/Boolean constants are added for the theory of strings when appropriate (default behaviour of StringFuzz).

Cactus plots for Z3str3 and CVC4 solvers can be found on the BanditFuzz webpage.

Appelt, D., Nguyen, C.D., Panichella, A., Briand, L.C.: A machine-learning-driven evolutionary approach for testing web application firewalls. IEEE Trans. Reliab. 67(3), 733–757 (2018)CrossRef

Artho, C.: Iterative delta debugging. Int. J. Softw. Tools Technol. Transf. 13(3), 223–246 (2011)CrossRef

Baldwin, S.: Compute Canada: advancing computational research. J. Phys. Conf. Ser. 341, 012001 (2012). IOP PublishingCrossRef

Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14. http://www.cs.stanford.edu/barrett/pubs/BCD+11.pdfCrossRef

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)

Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 55–59. IEEE (2017)

Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: a fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 45–51. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_6CrossRef

Bobot-CEA, F., Chihani-CEA, Z., Iguernlala-OCamlPro, M., Marre-CEA, B.: FPA solver

Böttinger, K., Godefroid, P., Singh, R.: Deep reinforcement fuzzing. arXiv preprint arXiv:1801.04589 (2018)

10.

Brain, M., Tinelli, C., Rümmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: 2015 IEEE 22nd Symposium on Computer Arithmetic (ARITH), pp. 160–167. IEEE (2015)

11.

Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, pp. 1–5. ACM (2009)

12.

Bugariu, A., Müller, P.: Automatically testing string solvers. In: International Conference on Software Engineering (ICSE), 2020. ETH Zurich (2020)

13.

Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. (TISSEC) 12(2), 10 (2008)CrossRef

14.

Tinelli, C., Barrett, C., Fontaine, P.: Theory of unicode strings (draft) (2019). http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

15.

Cha, S.K., Woo, M., Brumley, D.: Program-adaptive mutational fuzzing. In: 2015 IEEE Symposium on Security and Privacy, pp. 725–741. IEEE (2015)

16.

Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7CrossRefMATH

17.

Committee, I.S., et al.: 754–2008 IEEE standard for floating-point arithmetic. IEEE Computer Society Std 2008, 517 (2008)

18.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

19.

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

20.

Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. ACM SIGPLAN Not. 43(6), 281–292 (2008)CrossRef

21.

Gupta, A.K., Nadarajah, S.: Handbook of Beta Distribution and Its Applications. CRC Press, Boca Raton (2004)CrossRef

22.

Karamcheti, S., Mann, G., Rosenberg, D.: Adaptive grey-box fuzz-testing with Thompson sampling. In: Proceedings of the 11th ACM Workshop on Artificial Intelligence and Security, pp. 37–47. ACM (2018)

23.

Koza, J.R.: Genetic programming (1997)

24.

Le Goues, C., Leino, K.R.M., Moskal, M.: The Boogie verification debugger (tool paper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 407–414. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_28CrossRef

25.

Lemieux, C., Padhye, R., Sen, K., Song, D.: PerfFuzz: automatically generating pathological inputs. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 254–265 (2018)

26.

Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M.: An efficient SMT solver for string constraints. Form. Methods Syst. Des. 48(3), 206–234 (2016)CrossRef

27.

Manes, V.J., et al.: Fuzzing: art, science, and engineering. arXiv preprint arXiv:1812.00140 (2018)

28.

Mansur, M.N., Christakis, M., Wüstholz, V., Zhang, F.: Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. arXiv preprint arXiv:2004.05934 (2020)

29.

Heule, M., Järvisalo, M., Suda, M.: SAT race 2019 (2019). http://sat-race-2019.ciirc.cvut.cz/

30.

Marre, B., Bobot, F., Chihani, Z.: Real behavior of floating point numbers. In: 15th International Workshop on Satisfiability Modulo Theories (2017)

31.

Miller, C., Peterson, Z.N., et al.: Analysis of mutation and generation-based fuzzing. Technical report, Independent Security Evaluators (2007)

32.

Misherghi, G., Su, Z.: HDD: hierarchical delta debugging. In: Proceedings of the 28th International Conference on Software Engineering, pp. 142–151. ACM (2006)

33.

Niemetz, A., Biere, A.: ddSMT: a delta debugger for the SMT-LIB v2 format. In: Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, SMT 2013), affiliated with the 16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013, Helsinki, Finland, 8–9 July 2013, pp. 36–45 (2013)

34.

Niemetz, A., Preiner, M., Biere, A.: Model-based API testing for SMT solvers. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017, affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, 24–28 July 2017, 10 pages (2017)

35.

Patil, K., Kanade, A.: Greybox fuzzing as a contextual bandits problem. arXiv preprint arXiv:1806.03806 (2018)

36.

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

37.

Rebert, A., et al.: Optimizing seed selection for fuzzing. In: USENIX Security Symposium, pp. 861–875 (2014)

38.

Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT), p. 151 (2010)

39.

Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Pearson Education Limited, Malaysia (2016)MATH

40.

Russo, D.J., Van Roy, B., Kazerouni, A., Osband, I., Wen, Z., et al.: A tutorial on Thompson sampling. Found. Trends® Mach. Learn. 11(1), 1–96 (2018)CrossRef

41.

Seagle Jr., R.L.: A framework for file format fuzzing with genetic algorithms (2012)

42.

Sigaud, O., Buffet, O.: Markov Decision Processes in Artificial Intelligence. Wiley, New York (2013)CrossRef

43.

Sutton, M., Greene, A., Amini, P.: Fuzzing: Brute Force Vulnerability Discovery. Pearson Education, Upper Saddle River (2007)

44.

Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (2018)MATH

45.

Sutton, R.S., Barto, A.G., et al.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (1998)MATH

46.

Szepesvári, C.: Algorithms for reinforcement learning. Synt. Lect. Artif. Intell. Mach. Learn. 4(1), 1–103 (2010)MATH

47.

Takanen, A., Demott, J.D., Miller, C.: Fuzzing for Software Security Testing and Quality Assurance. Artech House, Norwood (2008)MATH

48.

Woo, M., Cha, S.K., Gottlieb, S., Brumley, D.: Scheduling black-box mutational fuzzing. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, pp. 511–522. ACM (2013)

49.

Zalewski, M.: American fuzzy lop (2015)

50.

Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183–200 (2002)CrossRef

Title: BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers
Authors: Joseph Scott
Federico Mora
Vijay Ganesh
Publisher: Springer International Publishing
Book: Software Verification
Print ISBN: 978-3-030-63617-3

Electronic ISBN: 978-3-030-63618-0

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-63618-0_5

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