Building Call Graph of WebAssembly Programs via Abstract Semantics
Mattia Paccamiccio, Franco Raimondi, Michele Loreti

TL;DR
This paper introduces a formal method using Abstract Interpretation to construct call graphs for WebAssembly programs, aiding security and behavioral verification.
Contribution
It presents a novel formal approach for building WebAssembly call graphs, addressing a key step in program analysis and verification.
Findings
Effective in predicting call graphs for benchmark programs
Outperforms existing methods in accuracy and efficiency
Facilitates security and correctness analysis of WebAssembly code
Abstract
WebAssembly is a binary format for code that is gaining popularity thanks to its focus on portability and performance. Currently, the most common use case for WebAssembly is execution in a browser. It is also being increasingly adopted as a stand-alone application due to its portability. The binary format of WebAssembly, however, makes it prone to being used as a vehicle for malicious software. For instance, one could embed a cryptocurrency miner in code executed by a browser. As a result, there is substantial interest in developing tools for WebAssembly security verification, information flow control, and, more generally, for verifying behavioral properties such as correct API usage. In this document, we address the issue of building call graphs for WebAssembly code. This is important because having or computing a call graph is a prerequisite for most inter-procedural verification…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsManufacturing Process and Optimization · Business Process Modeling and Analysis · Model-Driven Software Engineering Techniques
