Generative type-aware mutation for testing SMT solvers
OPEN ACCESS
Loading...
Author / Producer
Date
2021-10
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
We propose Generative Type-Aware Mutation, an effective approach for testing SMT solvers. The key idea is to realize generation through the mutation of expressions rooted with parametric operators from the SMT-LIB specification. Generative Type-Aware Mutation is a hybrid of mutation-based and grammar-based fuzzing and features an infinite mutation space—overcoming a major limitation of OpFuzz, the state-of-the-art fuzzer for SMT solvers. We have realized Generative Type-Aware Mutation in a practical SMT solver bug hunting tool, TypeFuzz. During our testing period with TypeFuzz, we reported over 237 bugs in the state-of-the-art SMT solvers Z3 and CVC4. Among these, 189 bugs were confirmed and 176 bugs were fixed. Most notably, we found 18 soundness bugs in CVC4’s default mode alone. Several of them were two years latent (7/18). CVC4 has been proved to be a very stable SMT solver and has resisted several fuzzing campaigns.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
5 (OOPSLA)
Pages / Article No.
152
Publisher
Association for Computing Machinery
Event
Object-oriented Programming, Systems, Languages, and Applications Conference (OOPSLA 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
SMT solvers; Fuzz testing; Generative type-aware mutation
Organisational unit
09628 - Su, Zhendong / Su, Zhendong