1 Introduction
2 Our Approach
3 Tool Architecture and Flow
witness generation
(\(P_w\)) and initial test-input generation modules. In the next step, the program is analysed to determine input ranges. These input ranges are used to formulate the fuzzing engine parameters \(F_i\). Subsequently, initial test-input population \(T_i\) is generated using the initial input generation module. The fuzz engine is then invoked with \(P_i\), \(F_i\), and \(T_i\) as inputs.__VERIFIER_*
functions are compiled together using gcc
to generate the executable program \(P_e\). The core fuzzer begins with \(T_i\) as its initial population, executes \(P_e\), and measures the coverage. A test-input from the population is selected and mutated several times to generate newer test-inputs \(T_g\). The program \(P_e\) is repeatedly executed with each test-input \(t_g \in T_g\) and coverage is measured. The fitness check step compares the code coverage due run on each \(t_g\) with the historical code coverage and determines whether \(t_g\) should be added to the population or not. This process is repeated until the core fuzzer finds a crashing test-input \(t_c\) that causes the program run to reach the error location or the time budget is elapsed. The \(t_c\) and \(P_w\) are passed to a witness generation program to generate error-witness
.4 Strengths and Weaknesses
reachsafety FALSE
benchmarks with 67 s as mean time per verification task
. Whereas in Test-Comp, it could identify bugs
in 592 out of 636 benchmarks. VeriFuzz could generate test-inputs that can, on an average, cover 70% branches in 1720 benchmarks.5 Tool Configuration and Setup
benchexec
tool-info module is verifuzz.py and the benchmark description file is verifuzz.xml. To install and run the tool, follow the instructions provided in README.txt with the tool. A sample run command is as follows:./scripts/verifuzz.py --propertyFile unreach-call.prp example.c