一句话：提出用 DSL 指定局部搜索策略的细粒度符号执行技术 Eunomia，并实现首个全特性 WebAssembly 符号执行引擎。
针对符号执行中的路径爆炸问题，现有自动化方法多只支持粗粒度全局搜索策略，难以高效遍历复杂代码结构，用户仍需谨慎优化搜索。本文提出 Eunomia，一种支持局部领域知识的细粒度搜索符号执行技术。它设计 DSL Aes，允许用户为程序不同部分指定局部搜索策略，并隔离不同局部策略的变量上下文以避免冲突。作者面向 WebAssembly 实现 Eunomia，可分析多种语言编写的应用，并称其为首个支持 WebAssembly 全特性的符号执行引擎。在微基准和六个真实应用上的评估显示，Eunomia 将 bug 检测能力最高提升三个数量级；用户研究验证了 Aes 的收益；它验证了 Collections-C 的六个已知 bug，并发现两个新的 0-day bug。
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 supports fine-grained search with local domain knowledge. Eunomia uses Aes, a DSL that lets users specify local searching strategies for different parts of the program. Eunomia also isolates the context of variables for different local searching strategies, avoiding conflicts. We implement Eunomia for WebAssembly, which can analyze applications written in various languages. Eunomia is the first symbolic execution engine that supports the full features of WebAssembly. We evaluate Eunomia with a microbenchmark suite and six real-world applications. Our evaluation shows that Eunomia improves bug detection by up to three orders of magnitude. We also conduct a user study that shows the benefits of using Aes. Moreover, Eunomia verifies six known bugs and detects two new zero-day bugs in Collections-C.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2304-07204,
title = {Eunomia: Enabling User-Specified Fine-Grained Search in Symbolically Executing WebAssembly Binaries},
author = {Ningyu He and Zhehao Zhao and Jikai Wang and Yubin Hu and Shengjian Guo and Haoyu Wang and Guangtai Liang and Ding Li and Xiangqun Chen and Yao Guo},
booktitle = {ISSTA},
year = {2023},
doi = {10.1145/3597926.3598064}
}