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.

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