posted on 2022-03-29, 03:28authored byDiego 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