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，使用户能够精确定位目标程序不同部分的局部搜索策略。为进一步优化局部搜索策略，我们设计了基于区间的算法，该算法可自动隔离不同局部搜索策略的变量上下文，避免同一变量上的局部搜索策略冲突。我们以WebAssembly为目标平台实现了Eunomia符号执行框架，使其能够分析用多种语言（如C和Go）编写但可编译为WebAssembly的应用程序。据我们所知，Eunomia是首个支持WebAssembly运行时全部特性的符号执行引擎。我们使用专用符号执行微基准测试套件和六个真实应用程序对Eunomia进行评估。评估表明，Eunomia将真实应用程序的漏洞检测速度提升高达三个数量级。综合用户研究结果显示，用户通过编写简单直观的Aes脚本即可显著提升符号执行的效率与效果。除验证六个已知真实世界漏洞外，Eunomia还在流行开源项目Collections-C中检测到两个零日漏洞。