ESEC/FSE 2020 (series) / Research Papers /
Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing
Tue 10 Nov 2020 08:05 - 08:06 at Virtual room 1 - Fuzzing
Formal methods use SMT solvers extensively for deciding formula
satisfiability, for instance, in software verification, systematic
test generation, and program synthesis. However, due to their complex
implementations, solvers may contain critical bugs that lead to
unsound results. Given the wide applicability of solvers in software
reliability, relying on such unsound results may have detrimental
consequences.
In this paper, we present \textsf{STORM}\xspace, a novel blackbox mutational fuzzing
technique for detecting critical bugs in SMT solvers. We run our
fuzzer on seven mature solvers and find 29 previously unknown
critical bugs. \textsf{STORM}{} is already being used in testing new features of
popular solvers before deployment.
Tue 10 Nov Times are displayed in time zone: (UTC) Coordinated Universal Time change
Tue 10 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change
| 08:00 - 08:02 Talk | Boosting Fuzzer Efficiency: An Information Theoretic PerspectiveACM SIGSOFT Distinguished Paper Award Research Papers Marcel BöhmeMonash University, Australia, Valentin ManèsKAIST, South Korea, Sang Kil ChaKAIST, South Korea DOI | ||
| 08:03 - 08:04 Talk | CrFuzz: Fuzzing Multi-purpose Programs through Input Validation Research Papers Suhwan SongSeoul National University, South Korea, Chengyu SongUniversity of California at Riverside, USA, Yeongjin JangOregon State University, USA, Byoungyoung LeeSeoul National University, South Korea DOI | ||
| 08:05 - 08:06 Talk | Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing Research Papers Muhammad Numair MansurMPI-SWS, Germany, Maria ChristakisMPI-SWS, Valentin WüstholzConsenSys, Fuyuan ZhangMPI-SWS, Germany DOI Pre-print | ||
| 08:07 - 08:08 Talk | Fuzzing: On the Exponential Cost of Vulnerability Discovery Research Papers DOI | ||
| 08:09 - 08:10 Talk | Harvey: A Greybox Fuzzer for Smart Contracts Industry Papers DOI Pre-print | ||
| 08:11 - 08:12 Talk | Intelligent REST API Data Fuzzing Research Papers Patrice GodefroidMicrosoft Research, USA, Bo-Yuan HuangPrinceton University, USA, Marina PolishchukMicrosoft Research, USA DOI | ||
| 08:13 - 08:14 Talk | MTFuzz: Fuzzing with a Multi-task Neural Network Research Papers Dongdong SheColumbia University, USA, Rahul KrishnaColumbia University, USA, Lu YanShanghai Jiao Tong University, China, Suman JanaColumbia University, USA, Baishakhi RayColumbia University, USA DOI Pre-print | ||
| 08:15 - 08:30 Talk | Conversations on Fuzzing Research Papers Dongdong SheColumbia University, USA, Muhammad Numair MansurMPI-SWS, Germany, Marcel BöhmeMonash University, Australia, Suhwan SongSeoul National University, South Korea, Valentin WüstholzConsenSys, M: Mike PapadakisUniversity of Luxembourg, Luxembourg | ||