一句话：提出 Sādhak，将模糊测试与 SMT 求解协同用于含闭盒函数的约束求解。
论文关注含闭盒函数的 SMT 求解问题：这类函数（第三方库、内联汇编、SIMD 指令、系统调用、机器学习模型调用等）缺乏形式语义，仅有输入-输出 oracle，传统 SMT 求解器无法处理。作者提出 Sādhak，其核心是让 fuzzer 与 SMT 引擎协同工作：fuzzer 负责对闭盒函数进行推理，SMT 引擎负责求解 SMT 理论约束，两者通过交换丰富且各自可解释的接口约束逐步收敛到模型。评估与唯一能处理此类闭盒约束的现有求解器比较，Sādhak 多求解 36.45% 的基准，PAR-2 指标提升 5.72 倍；在两者都能求解的基准上平均快 14.62 倍。
Programming languages and software engineering tools routinely encounter components that are difficult to reason on via formal techniques or whose formal semantics are not even available—third-party libraries, inline assembly code, SIMD instructions, system calls, calls to machine learning models, etc. However, often access to these components is available as input-output oracles—interfaces are available to query these components on certain inputs to receive the respective outputs. We refer to such functions as closed-box functions . Regular SMT solvers are unable to handle such closed-box functions. We propose Sādhak, a solver for SMT theories modulo closed-box functions. Our core idea is to use a synergistic combination of a fuzzer to reason on closed-box functions and an SMT engine to solve the constraints pertaining to the SMT theories. The fuzz and the SMT engines attempt to converge to a model by exchanging a rich set of interface constraints that are relevant and interpretable by them. Our implementation, Sādhak, demonstrates a significant advantage over the only other solver that is capable of handling such closed-box constraints: Sādhak solves 36.45% more benchmarks than the best-performing mode of this state-of-the-art solver and has 5.72x better PAR-2 score; on the benchmarks that are solved by both tools, Sādhak is (on an average) 14.62x faster.
@article{paperbot1462,
title = {Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing},
author = {Sujit Kumar Muduli and Subhajit Roy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563332}
}