Eunomia：在符号执行 WebAssembly 二进制时支持用户指定的细粒度搜索

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