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 extant 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. It ranks these goal labels according to a user-defined strategy. 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.

翻译：有界模型检验（BMC）与模糊测试技术是检测软件错误和安全漏洞最有效的方法之一。然而，现有方法因难以覆盖目标代码中的大面积区域，在错误检测中仍存在不足。我们提出FuSeBMC v4——一种测试生成器，通过合成具有有用属性的种子（称为智能种子），提升其混合模糊器的性能，从而实现对C程序的高覆盖率。FuSeBMC首先分析指定C程序，并逐步注入目标标签以引导BMC与进化模糊引擎；随后根据用户定义的策略对这些目标标签排序；接着，引擎在初始阶段运行以生成所谓的智能种子；最后，引擎以这些智能种子为初始种子再次运行，力求实现最大代码覆盖率与/或发现缺陷。在种子生成与常规运行过程中，引擎间的协调由Tracer子系统辅助完成。该子系统执行额外的覆盖率分析，并更新共享内存中已覆盖目标的信息。此外，Tracer动态评估测试用例，将用例转化为后续测试模糊的种子。由此，BMC引擎可提供种子，使模糊引擎能绕过复杂的数学防护（如输入验证）。最终，我们在第四届国际软件测试竞赛（Test-Comp 2022）中获得三项奖项，在包括覆盖率类别在内的所有类别中均超越现有顶尖工具。