Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FuSeBMC v4: Improving code coverage with smart seeds via BMC, fuzzing and static analysis

Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat, Lucas C. Cordeiro

TL;DR

FuSeBMC v4 tackles coverage gaps in software testing by integrating bounded model checking, greybox fuzzing, and static analysis into a two-stage workflow that generates and then exploits smart seeds. It injects goal labels into C code, ranks and selects high-impact goals, and uses a Tracer to coordinate seeds and coverage across engines. The framework combines a modified AFL fuzzer with ESBMC and a selective fuzzer, while static analysis identifies input ranges and loop unwind bounds to speed up exploration. Empirical results on Test-Comp 2022 show FuSeBMC v4 achieving first place in Cover-Branches, Cover-Error, and overall, outperforming FuSeBMC v3 and multiple state-of-the-art tools, demonstrating substantial gains in code coverage and vulnerability detection for C programs.

Abstract

Bounded model checking (BMC) and fuzzing techniques are among the most effective methods for detecting errors and security vulnerabilities in software. However, there are still shortcomings in detecting these errors due to the inability of existent methods to cover large areas in target code. We propose FuSeBMC v4, a test generator that synthesizes seeds with useful properties, that we refer to as smart seeds, to improve the performance of its hybrid fuzzer thereby achieving high C program coverage. FuSeBMC works by first analyzing and incrementally injecting goal labels into the given C program to guide BMC and Evolutionary Fuzzing engines. After that, the engines are employed for an initial period to produce the so-called smart seeds. Finally, the engines are run again, with these smart seeds as starting seeds, in an attempt to achieve maximum code coverage / find bugs. During both seed generation and normal running, coordination between the engines is aided by the Tracer subsystem. This subsystem carries out additional coverage analysis and updates a shared memory with information on goals covered so far. Furthermore, the Tracer evaluates test cases dynamically to convert cases into seeds for subsequent test fuzzing. Thus, the BMC engine can provide the seed that allows the fuzzing engine to bypass complex mathematical guards (e.g., input validation). As a result, we received three awards for participation in the fourth international competition in software testing (Test-Comp 2022), outperforming all state-of-the-art tools in every category, including the coverage category.

FuSeBMC v4: Improving code coverage with smart seeds via BMC, fuzzing and static analysis

TL;DR

FuSeBMC v4 tackles coverage gaps in software testing by integrating bounded model checking, greybox fuzzing, and static analysis into a two-stage workflow that generates and then exploits smart seeds. It injects goal labels into C code, ranks and selects high-impact goals, and uses a Tracer to coordinate seeds and coverage across engines. The framework combines a modified AFL fuzzer with ESBMC and a selective fuzzer, while static analysis identifies input ranges and loop unwind bounds to speed up exploration. Empirical results on Test-Comp 2022 show FuSeBMC v4 achieving first place in Cover-Branches, Cover-Error, and overall, outperforming FuSeBMC v3 and multiple state-of-the-art tools, demonstrating substantial gains in code coverage and vulnerability detection for C programs.

Abstract

Bounded model checking (BMC) and fuzzing techniques are among the most effective methods for detecting errors and security vulnerabilities in software. However, there are still shortcomings in detecting these errors due to the inability of existent methods to cover large areas in target code. We propose FuSeBMC v4, a test generator that synthesizes seeds with useful properties, that we refer to as smart seeds, to improve the performance of its hybrid fuzzer thereby achieving high C program coverage. FuSeBMC works by first analyzing and incrementally injecting goal labels into the given C program to guide BMC and Evolutionary Fuzzing engines. After that, the engines are employed for an initial period to produce the so-called smart seeds. Finally, the engines are run again, with these smart seeds as starting seeds, in an attempt to achieve maximum code coverage / find bugs. During both seed generation and normal running, coordination between the engines is aided by the Tracer subsystem. This subsystem carries out additional coverage analysis and updates a shared memory with information on goals covered so far. Furthermore, the Tracer evaluates test cases dynamically to convert cases into seeds for subsequent test fuzzing. Thus, the BMC engine can provide the seed that allows the fuzzing engine to bypass complex mathematical guards (e.g., input validation). As a result, we received three awards for participation in the fourth international competition in software testing (Test-Comp 2022), outperforming all state-of-the-art tools in every category, including the coverage category.
Paper Structure (29 sections, 3 figures, 7 tables, 3 algorithms)

This paper contains 29 sections, 3 figures, 7 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Fuzzing
  4. Code Coverage
  5. Bounded Model Checking
  6. Hybrid Fuzzing Techniques
  7. FuSeBMC v4 Framework
  8. Overview
  9. Code Instrumentation & Static Analysis
  10. Code Instrumentation
  11. Static Analysis
  12. Shared Memory
  13. Seed Generation
  14. Test Generation
  15. Main Fuzzer
  16. ...and 14 more sections

Figures (3)

  • Figure 1: Traditional fuzzing workflow. The fuzzing process consists of repetitive generation of inputs for the PUT, executing the PUT with these inputs and reporting any crashes as they occur.
  • Figure 2: The Framework of FuSeBMC v4. This figure illustrates the main components of FuSeBMC. Our tool starts by instrumenting and analyzing the source code, then performs coverage analysis in two stages: seed generation and test generation.
  • Figure 3: An example of a) a C program, b) the corresponding instrumented code, and c) the resulting goals tree, their depth in the code, and resulting rank values.