workshop-ocaml-2023-owi/owi.tex

\documentclass{article}

\usepackage[english]{babel}

\usepackage{fontspec} % encoding
\usepackage{hyperref}                                 % internal and external links (e.g. mail, www)
\usepackage{authblk} % author affiliation handling
\renewcommand\Affilfont{\itshape\small}
\usepackage{bbding}
\setmainfont{Linux Libertine O}
\setsansfont{Linux Biolinum O}
%\setsansfont{TeX Gyre Heros}
\setmonofont[Scale=MatchLowercase]{RobotoMono Nerd Font}

\title{Owi: an interpreter and a toolkit for WebAssembly written in OCaml}

\author[1,2]{Léo Andrès}
\author[1]{Pierre Chambart}
\author[1]{Eric Patrizio}
\author[1]{Dario Pinto}

\affil[1]{OCamlPro SAS, 21 rue de Châtillon, 75014 Paris, France}
\affil[2]{Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190 Gif-sur-Yvette, France}

\begin{document}

  \maketitle

  \begin{abstract}
    This presentation introduces Owi, an OCaml-based interpreter and toolkit for WebAssembly (Wasm). Owi aims to provide a fast and easily maintainable solution for Wasm code execution. Unlike competing interpreters, Owi focuses on facilitating experimentation, research, and symbolic manipulations of Wasm. We describe the different passes and intermediate representations of Owi. Additionally, we discuss the linker, the interpreter and its support for various Wasm-specific extensions. Owi's API leverages Generalized Algebraic Data Types (GADTs) for improved error detection at link-time. We also describe the testing methods used, including a Crowbar-based fuzzer. Future work includes incorporating missing Wasm extensions, implementing advanced optimization passes, and potentially porting the WASP execution engine to perform concolic execution.
  \end{abstract}

WebAssembly (Wasm) was developped to lever the limitations of Javascript for the Web but its current usages have expanded way beyond it. It is now used to execute code in isolated contexts such as in the cloud, or as a means to distribute portable binaries. Consequentially, numerous interpreters, optimisers and toolkits have been created such as: V8, SpiderMonkey, Binaryen, Wabt, Wasm3, Wasmer and Wasmtime. However most of these tool have been written in languages such as C, C++ or Rust, which makes them hard to expand and maintain even if they do offer excellent performances.

Two of which are written in OCaml, firstly: the reference interpreter. Only, its code is specifically tailored to adhere to the operationnal semantics of the language which makes it relatively slow and not easily modified (e.g. a substantial number of simplifications are done at parsing time, making it hard ot understand). Furthermore, it is solely comprised of what appears in the specification and does not perform any optimisation or allow for it to be used as a library in order to facilitate interfacing with functions written in the host language (OCaml).
The second is developped for the Tezos blockchain. It is a fork of the first but modified so that it may produce a trace to build a Merkle Tree at each step of the execution. It suffers from the same flaws as the first while being even slower.

In this talk, we will present Owi, an interpreter and toolkit developped in OCaml, which are at the same time easy to maintain, to expand and relatively fast. The goal of Owi, is not to compete with the fastest interpreters but rather to produce a tool that allows easy experimentation, means of research and perform symbolic manipulations of Wasm.

We start by describing the parser, which manages the entirety of the Wasm syntax allowing to use both S-expressions and sequential instructions wherever in the file, which is not supported by most tools. Then, we first demonstrate the functorized representation of the AST, which allows to factorise textual and binary modules, and second, the passes which validate and simplify modules.

We will then touch upon the linker and the Wasm interpreter itself, as well as our managing of the Wasm-specific extensions, some of which are not yet fully standardised, like:

\begin{itemize}
  \item  Import/Export of Mutable Globals
  \item  Non-trapping float-to-int conversions
  \item  Sign-extension operators
  \item  Multi-value
  \item  Reference Types
  \item  Bulk memory operations
  \item  Tail call
  \item  Typed Function References
  \item  Garbage collection
\end{itemize}

One of the peculiarities of Owi resides in its API which uses GADTs (Generalized Algebraic Data Types) to define functions in the host language (OCaml) and import them in Wasm modules. This allows, especially in the case of errors, to detect problems at link-time rather than at run-time.

We then describe the different methods used to test Owi, namely the reproduction of the script language used for Wasm in the reference test-suite as well as the development of a fuzzer that uses Crowbar.

Eventually, we mention the future works for Owi, namely:

\begin{itemize}
  \item the addition of missing Wasm extensions: Fixed-width SIMD, Extended Constant Expressions, Multiple memories, Custom Annotation Syntax in the Text Format, Memory64, Exception handling, Branch Hinting, Relaxed SIMD, Threads ;
  \item the addition of a more advanced optimisation pass than the one currently implemented by using static analysis techniques by taking part of the interpreter integrated in Owi ;
  \item Porting WASP, a concolic execution engine for WebAssembly that allows to test programs in C. Currently, WASP uses the reference interpreter but we hope to improve the performances by porting it to Owi.
\end{itemize}

\end{document}