ICSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
Thu 18 Apr 2024 11:15 - 11:30 at Fernando Pessoa - Fuzzing 1 Chair(s): Marcel Böhme

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 Apr

Displayed time zone: Lisbon change

11:00 - 12:30
11:00
15m
Talk
Crossover in Parametric Fuzzing
Research Track
Katherine Hough Northeastern University, Jonathan Bell Northeastern University
Pre-print Media Attached
11:15
15m
Talk
SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions
Research Track
Luiz Carvalho University of Luxembourg, Renzo Degiovanni Luxembourg Institute of Science and Technology, 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
15m
Talk
EDEFuzz: A Web API Fuzzer for Excessive Data ExposuresACM SIGSOFT Distinguished Paper Award
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
15m
Talk
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
15m
Talk
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
7m
Talk
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
7m
Talk
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