🐌 Owi

Owi is a toolchain to work with WebAssembly. It is written in OCaml. It provides a binary with many subcommands:

• owi c: a bug finding tool for C code that performs symbolic execution by compiling to Wasm and using our symbolic Wasm interpreter;
• owi conc: a concolic Wasm interpreter;
• owi fmt: a formatter for Wasm;
• owi opt: an optimizer for Wasm;
• owi run: a concrete Wasm interpreter;
• owi script: an interpreter for Wasm scripts;
• owi sym: a symbolic Wasm interpreter;
• owi validate: a validator for Wasm modules;
• owi wasm2wat: a Wasm binary to text format translater;
• owi wat2wasm: a Wasm text to binary format translater.

It also provides an OCaml library which allows for instance to import OCaml functions in a Wasm module in a type-safe way!

We also have a fuzzer that is able to generate random valid Wasm programs. For now it has not been made available as a subcommand so you'll have to hack the code a little bit to play with it.

⚠️ For now, the optimizer and the formatter are quite experimental. The optimizer is well tested but only performs basic optimizations in an inefficient way. The formatter is mainly used for debugging purpose and is probably incorrect on some cases.

🧑‍🎓 We are looking for interns, have a look at the internship labeled issues.

Installation

owi can be installed with opam:

$ opam install owi
# if you intend to use symbolic execution you must install one solver
# you can choose any solver supported by smtml
# z3, colibri2, bitwuzla-cxx or cvc5 for instance
$ opam install z3

If you don't have opam, you can install it following the how to install opam guide.

If you can't or don't want to use opam, you can build the package with dune build -p owi @install but you'll first have to install the dependencies by yourself. You can find the list of dependencies in the dune-project file.

Development version

To get the development version:

$ git clone [email protected]:OCamlPro/owi.git
$ cd owi
$ opam install . --deps-only
$ dune build -p owi @install
$ dune install

Development setup

To get a proper development setup:

$ git clone [email protected]:OCamlPro/owi.git
$ cd owi
$ opam install . --deps-only --with-test --with-doc --with-dev-setup
$ dune build @all

Supported proposals

The 🐌 status means the proposal is not applicable to Owi.

Adopted proposals

Proposal	Status
Import/Export of Mutable Globals	✔️
Non-trapping float-to-int conversions	✔️
Sign-extension operators	✔️
Multi-value	✔️
Reference Types	✔️
Bulk memory operations	✔️
Fixed-width SIMD	❌
JavaScript BigInt to WebAssembly i64 integration	🐌

Current proposals

We only list proposals that reached phase 3 at least.

Proposal	Status
Tail call	✔️
Typed Function References	✔️
Extended Constant Expressions	✔️
Garbage collection	Ongoing
Custom Annotation Syntax in the Text Format	Ongoing
Multiple memories	❌
Memory64	❌
Exception handling	❌
Branch Hinting	❌
Relaxed SIMD	❌
Threads	❌
Web Content Security Policy	🐌
JS Promise Integration	🐌
Type Reflection for WebAssembly JavaScript API	🐌

About

Publications and Talks

Publications

• Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly, 2024

Talks

• september 2023: ICFP OCaml track
• october 2023: Wasm Research Day organized by the WebAssembly Research Center and hosted in Google Munich
• april 2024: OUPS (OCaml UserS in Paris)

Spelling and pronunciation

Although the name Owi comes from an acronym (OCaml WebAssembly Interpreter), it must be written as a proper noun and only the first letter must be capitalized. It is possible to write the name in full lowercase when referring to the opam package or to the name of the binary.

The reason we chose this spelling rather than the fully capitalized version is that in French, Owi is pronounced [o’wi(ʃ)] which sounds like "Oh oui !" which means "Oh yes!". Thus it should be pronounced this way and not by spelling the three letters it is made of.

Changelog

See CHANGELOG.

License

Owi
Copyright (C) 2021-2024 OCamlPro

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU Affero General Public License for more details.

You should have received a copy of the GNU Affero General Public License
along with this program.  If not, see <http://www.gnu.org/licenses/>.

See LICENSE.

A few files have been taken from the WebAssembly reference interpreter. They are licensed under the Apache License 2.0 and have a different copyright which is stated in the header of the files.

Some code has been taken from the base library from Jane Street. It is licensed under the MIT License and have a different copyright which is stated in the header of the files.

Some code has been taken from the E-ACSL plugin of Frama-C. It is licensed under the GNU Lesser General Public License 2.1 and have a different copyright which is stated in the header of the files.

Fundings

This project was funded through the NGI0 Core Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme. See Owi project on NLnet.