This repository is for my (Alex Wendland) undergraduate thesis for Honors in Computer Science at Harvard submitted on April 10th, 2020. My advisor was Professor Nada Amin, and my readers were James Mickens, Stephen Chong, and Eddie Kohler.
If you're looking for an extension of WebAssembly with support for abstract types, see awendland/webassembly-spec-abstypes.
This project was mostly new territory for me, because it was focused on programming languages (eg. interpreter implementation, formal semantics, secure compilation, full abstraction) which I hadn't directly taken a course in yet. It was a fun challenge and I really appreciated the support of my mentors and peers.
Originally motivated by the goal of treating "languages and libraries orthgonally" (ie. being able to pick a language regardless of the libraries written for it, since you could use any library with any language), I began looking into secure compilation which is the ability to maintain the integrity of source-level abstractions from target-level attackers (I try to explain this more at the end of Chapter 1 of my thesis, and I also found Patrignani et al.'s 2019 survey paper quite approachable). These guarantees of integrity are also important when interoperating multiple languages, since you don't want a Rust program to call into a C function and have the C function violate the ownership guarantees of any Rust values you pass to it. During this, I discovered the importance of target language's feature set in maintaining these source-leve abstractions; without the right feature set it isn't possible to maintain. For example, you're unable to maintain unforgeable object references in x86 Assembly (see the Patrignani paper or, hopefully it's intelligble, Chapter 1 of my thesis if that previous sentence didn't make sense).
This lead me to look at WebAssembly as a target language for modular secure compilation, hence my thesis title, WebAssembly as a Multi-Language Platform. I argue for the introduction of abstract types into the core WebAssembly specification in order to support source-level abstractions like object references, unforgeable handles, and referential invariants. Combined with WebAssembly's already powerful featureset—like typed function calls and constrained control flow—WebAssembly makes a compelling candidate for use as a secure multi-language platform.
This repo contains several exploratory and supporting pieces of work, with the bulk of the WebAssembly abstract type extension being implemented in another repo (awendland/webassembly-spec-abstypes).
paper/thesis-harvard-2020.pdf- PDF of the thesis which I submitted on April 10th to the CS Department of SEAS.thesis-harvard-2020-overleaf.zip- The latex source exported from Overleaf after final submission of my thesis to the department. This document was based on the wonderful Dissertate template by Jordan Suchow.
exploration/- mini-projects where I messed around with WebAssembly and different {Rust,Zig,C++}-to-WebAssembly compilers. See [exploration/README.md] for more information.samples/- Runnable examples used in the thesis, primarily Chapter 3: Maintaining the Integrity of Source Level Abstractions.sample-X.Y.watwould refer to a sample in Chapter X Section Y.sample-X.Y-abstypes.watindicates that the code requires a WebAssembly interpreter with support for the abstract types defined in this thesis. See Reference implementation.samples.ipynb- Jupyter notebook populated with the*.watsamples; runnable in environments with the wasm-spec-kernel.
I added support for abstract types (similar to OCaml's abstract types) to the reference interpreter for WebAssembly. My extended interpreter can be found at awendland/webassembly-spec-abstypes. Discussion about this feature can be found in Chapter 2: Extending WebAssembly with Abstract Types in the thesis.
To make trying out this implementation easier, I've implemented a generic Jupyter kernel for WebAssembly reference interpreters. It's available on PyPI as wasm-spec-kernel and on GitHub.
I've configured this repository to be runnable via Binder, so that you can jump right into a web-based Jupyter notebook with the webassembly-spec-abstypes interpreter already available and the code in samples/ all runnable. Try it out with:
