Macquarie University
01whole.pdf (1.36 MB)
Download file

Verification of WebAssembly programs

Download (1.36 MB)
posted on 2022-03-29, 03:28 authored by Diego Ignacio Ocampo Herrera
WebAssembly is a new low-level language and compilation target mainly for the web that is already shipped in all major browsers in its minimum viable product version. The current version does not support exception handling, and therefore runtime errors cannot be handled inside the WebAssembly code. Our main contribution of this research is the development of an approach that can detect runtime errors (traps) statically using Skink, a static analysis tool. To detect the possible traps, we: 1. translate WebAssembly (stack machine) into LLVM-IR (register machine), and 2. instrument the resulting code to reduce the problem of detecting traps to a reachability problem. To test our solution, we use C/C++ benchmarks files from SV-COMP compiled into WebAssembly by Emscripten and compare the results against the standard verification process of C/C++ files by Skink. After successfully testing our approach, we apply our tool to verify programs that could abort execution due to runtime errors, detecting the conditions under which the error would occur. Internet browsers could benefit from this approach in the future, as they will execute WebAssembly modules that originate from untrusted sources and possibly with malicious intentions. Our approach would then aid in the early detection of runtime errors of these WebAssembly modules -- abstract.


Table of Contents

1. Introduction -- 2. Literature review -- 3. Methods -- 4. Translating WebAssembly into LLVM -- 5. Validating the translation -- 6. Verifying WebAssembly -- 7. Conclusions -- References.


Theoretical thesis. Bibliography: pages 51-53

Awarding Institution

Macquarie University

Degree Type

Thesis MRes


MRes, Macquarie University, Faculty of Science and Engineering, Department of Computing

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Anthony Sloane

Additional Supervisor 1

Franck Cassez


Copyright Diego Ignacio Ocampo Herrera 2019. Copyright disclaimer:




1 online resource (xviii, 71 pages)

Former Identifiers