模糊符号表达式
Fuzzing Symbolic Expressions
摘要：
近年来，软件测试取得了广泛的成果，探索了不同的方法和方法，从模糊器到符号引擎，以及介于两者之间的各种实例，如concolic执行和混合模糊。其中许多工具的一个关键组成部分是可满足性模理论（SMT）求解器，用于对分析期间收集的符号表达式进行推理。在本文中，我们研究是否可以借用模糊域的技术来检查是否符号公式是可满足的concolic和混合模糊引擎的背景下，提供了一个可行的替代经典SMT解决技术。我们设计了一个新的近似求解器，FUZZY-SAT，并表明它是竞争和互补的最先进的求解器，如Z3处理混合模糊器产生的查询。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
