Exploiting the SAT Revolution for Automated Software Verification: Report from an Industrial Case Study
Resumo
In the last three decades, Boolean Satisfiability (SAT) solvers experienced a dramatic performance revolution; they are now used as the backend of various industrial verification engines. SAT solvers can now check logical formulas that contain millions of propositional variables. In Satisfiability Modulo Theories (SMT) solvers, predicates from various theories are not encoded using propositional variables as in SAT but remain in the problem formulation. Thus, SMT solvers can be used as backends for solving the generated verification conditions to cope with increasing software complexity from industrial applications. This talk will overview automated software verification techniques that rely on sophisticated SMT solvers built over efficient SAT solvers. I will discuss challenges, problems, and recent advances to ensure safety and security in open-source and embedded software applications. I will describe novel algorithms that exploit fuzzing, explicit-state, and SMT-based symbolic model checking for verifying single- and multi-threaded software. These algorithms were the first to verify multi-threaded C/Posix software based on shared-memory synchronization and communication symbolically. They are implemented in industrial-strength software verification tools, now considered state-of-the-art in the software testing and verification community, receiving 28 medals at SV-COMP and Test-COMP. This achievement enabled industrial research collaborations with Intel and Nokia. Software engineers applied these tools to find real security vulnerabilities in large-scale software systems (e.g., memory safety in firmware for Intel and arithmetic overflow in telecommunication software for Nokia, neither of which had been found before).
Referências
MITRE, “Mitre’s top 25 cwe,” 2020, https://cwe.mitre.org/top25/archive/2020/2020_cwe_top25.html.
C. Cimpanu, “Microsoft: 70 percent of all security bugs are memory safety issues,” 2019, [link].
Google, “https://www.chromium.org/home/chromium-security/memory-safety,” 2020, https://www.chromium.org/Home/chromium-security/memory-safety.
L. C. Cordeiro and B. Fischer, “Verifying multi-threaded software using smt-based context-bounded model checking,” in Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011. ACM, 2011, pp. 331–340. [Online]. Available: https://doi.org/10.1145/1985793.1985839
L. C. Cordeiro, B. Fischer, and J. Marques-Silva, “Smt-based bounded model checking for embedded ANSI-C software,” IEEE Trans. Software Eng., vol. 38, no. 4, pp. 957–974, 2012. [Online]. Available: https://doi.org/10.1109/TSE.2011.59
P. A. Pereira, H. F. Albuquerque, I. da Silva, H. Marques, F. R. Monteiro, R. Ferreira, and L. C. Cordeiro, “Smt-based context-bounded model checking for CUDA programs,” Concurr. Comput. Pract. Exp., vol. 29, no. 22, 2017. [Online]. Available: https://doi.org/10.1002/cpe.3934
F. R. Monteiro, M. R. Gadelha, and L. C. Cordeiro, “Model checking C++ programs,” Journal of Software: Testing, Verification and Reliability, vol. 31, 2021. [Online]. Available: https://onlinelibrary.wiley.com/doi/epdf/10.1002/stvr.1793.
Cordeiro L., Kesseli P., Kroening D., Schrammel P., Trtík M. (2018) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. In: Chockler H., Weissenbacher G. (eds) Computer Aided Verification. CAV 2018. Lecture Notes in Computer Science, vol 10981. Springer, Cham. https://doi.org/10.1007/978-3-319-96145-3_10
L. C. Cordeiro, D. Kroening, and P. Schrammel, “JBMC: bounded model checking for java bytecode - (competition contribution),” in Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, ser. Lecture Notes in Computer Science, vol. 11429. Springer, 2019, pp. 219–223. [Online]. Available: https://doi.org/10.1007/978-3-319-96145-3_17
