LTL solvers check the satisfiability of Linear-time Temporal Logic (LTL) formulas and are widely used for verifying and testing critical software systems. Thus, potential bugs in the solvers’ implementation can have a significant impact. To deal with this problem, we present SpecBCFuzz, a fuzzing method for LTL solvers that is guided by boundary conditions (BCs), corner cases whose (un)satisfiability depends on rare traces. SpecBCFuzz implements a search-based algorithm that fuzzes LTL formulas in a way that the BCs remain relevant. To achieve this, SpecBCFuzz integrates syntactic and semantic similarity metrics to explore the vicinity of the seeded formulas with BCs. We evaluate SpecBCFuzz with 21 different configurations (including the latest and past releases) of four mature and state-of-the-art LTL solvers (NuSMV, Black, Aalta and PLTL) that implement a diverse set of algorithms (BDD, BMC, Tableau, etc). SpecBCFuzz produces 368,716 bug-triggering formulas, detecting bugs in 18 out of the 21 solvers’ configurations we study. Specifically, SpecBCFuzz reveals: soundness issues (wrong answers given by a solver) in Aalta and PLTL; crashes, e.g., segmentation faults, in NuSMV, Black and Aalta; flaky behavior (different responses across re-runs of the solver on the same formula) in NuSMV and Aalta; performance bugs (large performance degradations between successive versions of the solver on the same formula) in Black, Aalta and PLTL; and no bug in NuSMV BDD (all versions), suggesting that the latter is currently the most robust solver.
Thu 18 AprDisplayed time zone: Lisbon change
11:00 - 12:30 | Fuzzing 1Software Engineering in Practice / Journal-first Papers / Research Track at Fernando Pessoa Chair(s): Marcel Böhme MPI-SP, Bochum | ||
11:00 15mTalk | Crossover in Parametric Fuzzing Research Track Pre-print Media Attached | ||
11:15 15mTalk | SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions Research Track Luiz Carvalho University of Luxembourg, Renzo Degiovanni SnT, University of Luxembourg, Maxime Cordy University of Luxembourg, Luxembourg, Nazareno Aguirre University of Rio Cuarto and CONICET, Yves Le Traon University of Luxembourg, Luxembourg, Mike Papadakis University of Luxembourg | ||
11:30 15mTalk | EDEFuzz: A Web API Fuzzer for Excessive Data Exposures Research Track Lianglu Pan University of Melbourne, Shaanan Cohney University of Melbourne, Toby Murray University of Melbourne, Thuan Pham The University of Melbourne | ||
11:45 15mTalk | ECFuzz: Effective Configuration Fuzzing for Large-Scale Systems Research Track Junqiang Li University of Electronic Science and Technology of China, Senyi Li University of Electronic Science and Technology of China, Keyao Li University of Electronic Science and Technology of China, Falin Luo University of Electronic Science and Technology of China, Hongfang Yu University of Electronic Science and Technology of China, Shanshan Li National University of Defense Technology, Xiang Li Academy of Military Sciences DOI Media Attached File Attached | ||
12:00 15mTalk | Mind the Gap: What Working With Developers on Fuzz Tests Taught Us About Coverage Gaps Software Engineering in Practice Carolin Brandt Delft University of Technology, Marco Castelluccio Mozilla, Christian Holler Mozilla Corporation, Jason Kratzer Mozilla Corporation, Andy Zaidman Delft University of Technology, Alberto Bacchelli University of Zurich DOI Pre-print | ||
12:15 7mTalk | CLFuzz: Vulnerability Detection of Cryptographic Algorithm Implementation via Semantic-Aware Fuzzing Journal-first Papers Yuanhang Zhou Tsinghua University, Fuchen Ma Tsinghua University, Yuanliang Chen Tsinghua University, Meng Ren Tsinghua University, Yu Jiang Tsinghua University | ||
12:22 7mTalk | FormatFuzzer: Effective Fuzzing of Binary File Formats Journal-first Papers Rafael Dutra CISPA Helmholtz Center for Information Security, Rahul Gopinath University of Sydney, Andreas Zeller CISPA Helmholtz Center for Information Security | ||