一句话：提出高效全功能的 WebAssembly 二进制符号执行引擎 SeeWasm，无需人工干预且提速 2 至 6 倍。
WebAssembly 可由 40 多种高级语言编译生成，但其二进制漏洞可能导致敏感数据泄露并威胁宿主环境。符号执行因具备可靠性与自动生成利用的能力而被广泛采用，但现有 Wasm 符号执行器通常与特定平台绑定，无法支持全部 Wasm 特性，且需大量人工干预、效率较低。为此，本文提出高效且全功能的符号执行引擎 SeeWasm。评估表明，SeeWasm 无需额外人工干预即可支持全特性 Wasm 二进制，并将分析速度提升 2 至 6 倍；已有工作使用它，在将知名 C、Go 和 SGX 应用编译为 Wasm 后，识别出 30 多个 0-day 漏洞或安全问题。
WebAssembly (Wasm), as a compact, fast, and isolation-guaranteed binary format, can be compiled from more than 40 high-level programming languages. However, vulnerabilities in Wasm binaries could lead to sensitive data leakage and even threaten their hosting environments. To identify them, symbolic execution is widely adopted due to its soundness and the ability to automatically generate exploitations. However, existing symbolic executors for Wasm binaries are typically platform-specific, which means that they cannot support all Wasm features. They may also require significant manual interventions to complete the analysis and suffer from efficiency issues as well. In this paper, we propose an efficient and fully-functional symbolic execution engine, named SeeWasm. Compared with existing tools, we demonstrate that SeeWasm supports full-featured Wasm binaries without further manual intervention, while accelerating the analysis by 2 to 6 times. SeeWasm has been adopted by existing works to identify more than 30 0-day vulnerabilities or security issues in well-known C, Go, and SGX applications after compiling them to Wasm binaries.
DOI 原文 ·
@inproceedings{paperbot8477,
title = {SeeWasm: An Efficient and Fully-Functional Symbolic Execution Engine for WebAssembly Binaries},
author = {Ningyu He and Zhehao Zhao and Hanqin Guan and Jikai Wang and Shuo Peng and Ding Li and Haoyu Wang and Xiangqun Chen and Yao Guo},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3685300}
}