Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver

Guillaume Bury
Steven de Oliveira
  • Fonction : Auteur

Résumé

Alt-Ergo is an open source Satisfiability Modulo Theories (SMT) solver programmed in OCaml. It was designed for program verification and it's used as a back end by other software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat, the reliability of which depends on the soundness of Alt-Ergo's answers and the absence of bugs in it. Fuzzing is an efficient technique to test programs and find bugs. It works by quickly and automatically generating input data with which to test the software. American Fuzzy Lop (AFL) is one of the most well-known and most used fuzzers in both academia and the industry. It has managed to find many bugs in various programs thanks to its grey box fuzzing technique that uses genetic algorithms and program instrumentation to generate test data that maximizes code and execution path coverage in the targeted software. In this paper we present Alt-Ergo-Fuzz, a fuzzer for Alt-Ergo that we developed with the aim of finding faults and unsoundness bugs to solve and improve its reliability. By using AFL as a back end, the Crowbar OCaml library for test case generation and the CVC5 SMT solver as a reference solver of which the answers will be used to determine whether or not Alt-Ergo's answers are correct, we managed to develop Alt-Ergo-Fuzz, which even as a work in progress and in only twenty days of testing managed to find four never found before bugs in Alt-Ergo.
Fichier principal
Vignette du fichier
jfla22_paper_15.pdf (298.32 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03626861 , version 1 (31-03-2022)

Identifiants

  • HAL Id : hal-03626861 , version 1

Citer

Hichem Rami Ait El Hara, Guillaume Bury, Steven de Oliveira. Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver. 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.235-244. ⟨hal-03626861⟩

Collections

JFLA2022
182 Consultations
282 Téléchargements

Partager

Gmail Facebook X LinkedIn More