Abstract
This paper presents the Cubicle Fuzzy Loop (CFL), a fuzzing-based extension for Cubicle, a model checker for parameterized systems.
To prove safety, Cubicle generates invariants, making use of forward exploration strategies like BFS or DFS on finite model instances. However, these standard algorithms are quickly faced with the state explosion problem due to Cubicle’s purely nondeterministic semantics. This causes them to struggle at discovering critical states, hindering invariant generation.
CFL replaces this approach with a powerful DFS-like algorithm inspired by fuzzing. Cubicle’s purely nondeterministic execution loop is modified to provide feedback on newly discovered states and visited transitions. This feedback is used by CFL to construct schedulers that guide the model exploration. Not only does this provide Cubicle with a bigger variety of states for generating invariants, it also quickly identifies unsafe models. As a bonus, it adds testing capabilities to Cubicle, such as the ability to detect deadlocks.
Our first experiments have yielded promising results. CFL effectively allows Cubicle to generate crucial invariants, useful to handle hierarchical systems, while also being able to trap bad states and deadlocks in hard-to-reach areas of such models.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aljaafari, F.K., Menezes, R., Manino, E., Shmarov, F., Mustafa, M.A., Cordeiro, L.C.: Combining BMC and fuzzing techniques for finding software vulnerabilities in concurrent programs. IEEE Access 10, 121365–121384 (2022)
Alshmrany, K.M., Aldughaim, M., Bhayat, A., Cordeiro, L.C.: FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing. In: FASE 2022. LNCS, vol. 13241, pp. 336–340. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99429-7_19
Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_55
Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: 2013 Formal Methods in Computer-Aided Design, pp. 61–68. IEEE (2013)
Conchon, S., Mebsout, A., Zaïdi, F.: Vérification de systèmes paramétrés avec Cubicle. In: JFLA. Aussois, France, February 2013. http://hal.inria.fr/hal-00778832
Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning. Lecture Notes in Computer Science, vol. 5195, pp. 67–82. Springer, Heidelberg (2008)
Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: IJCAR, pp. 22–29 (2010)
Godefroid, P.: Fuzzing: hack, art, and science. Commun. ACM 63(2), 70–76 (2020)
Manès, V.J., et al.: The art, science, and engineering of fuzzing: a survey. IEEE Trans. Softw. Eng. 47(11), 2312–2331 (2019)
Meng, R., Dong, Z., Li, J., Beschastnikh, I., Roychoudhury, A.: Linear-time temporal logic guided greybox fuzzing. In: Proceedings of the 44th International Conference on Software Engineering, pp. 1343–1355 (2022)
Miller, B.P., Fredriksen, L., So, B.: An empirical study of the reliability of unix utilities. Commun. ACM 33(12), 32–44 (1990)
Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Exploiting transition locality in automatic verification of finite-state concurrent systems. STTT 6(4), 320–341 (2004)
Yang, Y.: Improve model testing by integrating bounded model checking and coverage guided fuzzing. Electronics 12(7), 1573 (2023)
Zalewski, M.: American fuzzy lop-whitepaper (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Conchon, S., Korneva, A. (2023). The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker. In: Ferreira, C., Willemse, T.A.C. (eds) Software Engineering and Formal Methods. SEFM 2023. Lecture Notes in Computer Science, vol 14323. Springer, Cham. https://doi.org/10.1007/978-3-031-47115-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-47115-5_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-47114-8
Online ISBN: 978-3-031-47115-5
eBook Packages: Computer ScienceComputer Science (R0)