Although existing techniques have proposed automated approaches to alleviate the path explosion problem of symbolic execution, users still need to optimize symbolic execution by applying various searching strategies carefully. As existing approaches mainly support only coarse-grained global searching strategies, they cannot efficiently traverse through complex code structures. In this paper, we propose Eunomia, a symbolic execution technique that allows users to specify local domain knowledge to enable fine-grained search. In Eunomia, we design an expressive DSL, Aes, that lets users precisely pinpoint local searching strategies to different parts of the target program. To further optimize local searching strategies, we design an interval-based algorithm that automatically isolates the context of variables for different local searching strategies, avoiding conflicts between local searching strategies for the same variable. We implement Eunomia as a symbolic execution platform targeting WebAssembly, which enables us to analyze applications written in various languages (like C and Go) but can be compiled into WebAssembly. To the best of our knowledge, Eunomia is the first symbolic execution engine that supports the full features of the WebAssembly runtime. We evaluate Eunomia with a dedicated microbenchmark suite for symbolic execution and six real-world applications. Our evaluation shows that Eunomia accelerates bug detection in real-world applications by up to three orders of magnitude. According to the results of a comprehensive user study, users can significantly improve the efficiency and effectiveness of symbolic execution by writing a simple and intuitive Aes script. Besides verifying six known real-world bugs, Eunomia also detected two new zero-day bugs in a popular open-source project, Collections-C.

翻译：尽管现有技术提出了自动化方法来缓解符号执行的路径爆炸问题，用户仍需通过仔细应用多种搜索策略来优化符号执行。由于现有方法主要支持粗粒度的全局搜索策略，因此无法高效遍历复杂代码结构。本文提出Eunomia，一种允许用户指定局部领域知识以实现细粒度搜索的符号执行技术。在Eunomia中，我们设计了一种表达能力强的领域特定语言Aes，使用户能够精确地将局部搜索策略定位到目标程序的不同部分。为进一步优化局部搜索策略，我们设计了一种基于区间的算法，自动隔离不同局部搜索策略的变量上下文，避免同一变量的局部搜索策略间的冲突。我们将Eunomia实现为针对WebAssembly的符号执行平台，从而能够分析用多种语言（如C和Go）编写但可编译为WebAssembly的应用程序。据我们所知，Eunomia是首个支持WebAssembly运行时全部特性的符号执行引擎。我们使用专用符号执行微基准测试套件和六个真实应用对Eunomia进行评估。评估表明，Eunomia将真实应用的缺陷检测速度提升最高达三个数量级。综合用户研究结果显示，用户通过编写简单直观的Aes脚本即可显著提高符号执行的效率和有效性。除验证了六个已知的真实缺陷外，Eunomia还在流行开源项目Collections-C中检测到两个新的零日缺陷。