FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs

TL;DR

FuSeBMC is a novel white-box fuzzer for C programs that combines fuzzing, symbolic execution, and Bounded Model Checking to effectively discover security vulnerabilities, achieving top results in competitive testing.

Contribution

It introduces a combined approach integrating fuzzing, symbolic execution, and BMC for improved vulnerability detection in C programs.

Findings

Achieved first place in Cover-Error at Test-Comp'21

Secured second place overall at Test-Comp'21

Demonstrated effectiveness in finding security vulnerabilities

Abstract

We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. FuSeBMC explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. FuSeBMC successfully participates in Test-Comp'21 and achieves first place in the Cover-Error category and second place in the Overall category.