Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, FUZZY-SAT, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers.
翻译:近年来,在软件测试方面取得了广泛的结果,探索了从模糊器到象征性引擎的不同方法与方法,在诸如硬化执行和混合模糊学等一系列实例中都有各种各样的实例。这些工具中有许多关键成分是可满足的莫杜洛理论解答器,用来解释分析过程中收集的符号表达法。在本文中,我们研究从模糊学域借用的技术是否可以用于检查在调和和混合模糊学引擎中象征性公式是否可被引用,为经典的SMT解答技术提供可行的替代方法。我们设计了一个新的近似解答器,即FUZY-SAT,并表明它与Z3等最新解答器具有竞争力,并且与Z3等最新解答器在处理混合模糊学问时具有互补性。