Owi: Seamless program analysis for C, C++, Go, Haskell, LLVM, Rust, Wasm and Zig

Owi provides seamless program analysis for C, C++, Go, Haskell, LLVM, Rust, Wasm and Zig.

Owi operates at the Wasm level. It provides built-in support for compiling programs written in higher-level languages to Wasm and analyzing the resulting code. This also makes it possible to analyze cross-language programs. For example, you can use Owi on a Rust program calling into a C library.

Owi's main capability is automatic bug-finding, powered by its multicore symbolic execution engine. Owi also includes a basic fuzzer. We are currently working on improving the fuzzer, and in particular, on combining fuzzing with symbolic execution to discover some bugs earlier and explore programs more efficiently.

The same bug-finding infrastructure can be used for other purposes, including automated test-case generation for advanced code-coverage criteria, and solver-aided programming.

A more recent direction is the exploration of automatic program verification with Owi. This work is still experimental but actively developed. In particular, we have a prototype abstract interpreter that can generate invariants statically and prove some properties of Wasm programs.

The abstract interpreter is also being used as the basis for a Wasm-to-Wasm optimizer, currently under development. We are also exploring how to reuse generated invariants in the symbolic execution engine to eliminate many SMT checks.

Because Owi works at the Wasm level, it also serves as a Wasm Swiss Army knife. It includes a formatter, interpreter, validator, and tools for converting between .wasm and .wat formats.

Owi also includes a Wasm fuzzer that generates well-typed Wasm programs. This is distinct from the program fuzzer described above: the Wasm fuzzer generates Wasm programs, while the program fuzzer is intended to find bugs in programs compiled to Wasm.

Since Owi is written in OCaml, it can also be used as an OCaml library. This makes its analysis and Wasm-related capabilities available for integration into other tools and workflows.

For instance, we are currently working on a Wasm-to-OCaml compiler. Our goal is to build unikernels from any program that can be compiled to Wasm. This compiler could also be used to efficiently embed Wasm programs into OCaml applications.

• 📘 User Manual
  • Install Owi
  • Quickstart
• 💬 Zulip community
• List of supported Wasm proposals
• Changelog
• Hacking on Owi

• Manpages
• TODO: high-level API for each language
• TODO: Wasm API
• OCaml library API

This project was partly funded through the NGI0 Core Fund and the NGI0 Commons Fund, established by NLnet with financial support from the European Commission's Next Generation Internet program :

1. First grant.
2. Second grant.
3. Third grant.
4. Fourth grant.

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.

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 Wasm 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.