SeeWasm: An Efficient and Fully-Functional Symbolic Execution Engine for WebAssembly Binaries

Fuente: arXiv
Gespeichert in:
Bibliographische Detailangaben
Hauptverfasser: He, Ningyu, Zhao, Zhehao, Guan, Hanqin, Wang, Jikai, Peng, Shuo, Li, Ding, Wang, Haoyu, Chen, Xiangqun, Guo, Yao
Format: Preprint
Veröffentlicht: 2024
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1866914913700544512
author He, Ningyu
Zhao, Zhehao
Guan, Hanqin
Wang, Jikai
Peng, Shuo
Li, Ding
Wang, Haoyu
Chen, Xiangqun
Guo, Yao
author_facet He, Ningyu
Zhao, Zhehao
Guan, Hanqin
Wang, Jikai
Peng, Shuo
Li, Ding
Wang, Haoyu
Chen, Xiangqun
Guo, Yao
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2408_08537
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle SeeWasm: An Efficient and Fully-Functional Symbolic Execution Engine for WebAssembly Binaries
He, Ningyu
Zhao, Zhehao
Guan, Hanqin
Wang, Jikai
Peng, Shuo
Li, Ding
Wang, Haoyu
Chen, Xiangqun
Guo, Yao
Cryptography and Security
Software Engineering
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.
title SeeWasm: An Efficient and Fully-Functional Symbolic Execution Engine for WebAssembly Binaries
topic Cryptography and Security
Software Engineering
url https://arxiv.org/abs/2408.08537