01whole.pdf (1.36 MB)
Download file

Verification of WebAssembly programs

Download (1.36 MB)
thesis
posted on 29.03.2022, 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.

History

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.

Notes

Theoretical thesis. Bibliography: pages 51-53

Awarding Institution

Macquarie University

Degree Type

Thesis MRes

Degree

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

Department, Centre or School

Department of Computing

Year of Award

2019

Principal Supervisor

Anthony Sloane

Additional Supervisor 1

Franck Cassez

Rights

Copyright Diego Ignacio Ocampo Herrera 2019. Copyright disclaimer: http://mq.edu.au/library/copyright

Language

English

Extent

1 online resource (xviii, 71 pages)

Former Identifiers

mq:71163 http://hdl.handle.net/1959.14/1271507