Solidifying Modern SMT Solvers
OPEN ACCESS
Author / Producer
Date
2024
Publication Type
Doctoral Thesis
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Satisfiability Modulo Theory (SMT) solvers realize one of the most powerful and mature classes of formal methods. They are foundational for many important advances in software research and industry. For example, one large-scale application is realized by AWS, which uses SMT solvers for verifying properties of cloud services. In almost all of their applications, SMT solvers are critical components solving NP-hard problems and establish trust through proof. Hence SMT solvers should be correct and performant, particularly in safety-critical and security-critical domains. Until recently, SMT solvers were widely trusted and believed to be solid. This thesis puts the existing trust in SMT solvers to the test by proposing five approaches to address the correctness and performance of SMT solvers. The first approach is Semantic Fusion, a testing methodology to validate the correctness of SMT solvers. Semantic Fusion demonstrated that SMT solvers are less reliable than previously believed by finding dozens of soundness bugs in Z3 and CVC4. Orthogonal to Semantic Fusion, we propose Type-Aware Operator Mutation, a simple but unusually effective approach which found a total of 1,254 bugs in Z3 and CVC4 including soundness bugs across almost all theories in both solvers Z3 and CVC4/cvc5. To overcome the limitations of Type-Aware Operator Mutation, we propose Generative Type-Aware Mutation, an even more powerful approach, finding another 322 bugs in Z3 and CVC4/cvc5, among them several longstanding soundness bugs in CVC4. While the first three approaches focus on correctness, Janus is a pioneering approach for finding incompleteness bugs in SMT solvers. The final approach, Grammar-based Enumeration, addresses correctness and performance. Its realization ET is not only an effective bug finder but ET can help understand the evolution of SMT solvers. Our results suggest improved correctness in recent versions of Z3 and CVC4/cvc5 but decreased performance in newer Z3 releases. This research enables one of the world’s largest academic bug-finding campaigns. In five years, we found 1,825 unique bugs in Z3 and cvc5, among which 1,333 were fixed. Strikingly, we found 483 soundness bugs among which 349 were fixed. This thesis has significantly boosted research on solidifying formal methods beyond SMT solvers.
Permanent link
Publication status
published
External links
Editor
Contributors
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH Zurich
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
COMPUTER SCIENCE; Software testing; SMT solvers
Organisational unit
09628 - Su, Zhendong / Su, Zhendong
09628 - Su, Zhendong / Su, Zhendong
03653 - Müller, Peter / Müller, Peter