ocamlpro / owi

WebAssembly Swissknife & cross-language bugfinder

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

owi's Issues

improve perfs after the `return_call` support

As expected, performances suffered a bit from #1. @chambart had some idea on how to make them great again.

add a `owi fmt` command

should keep comments at some point

add some Wasm to Wasm optimisations

There is a proper internship offed (in french).

A minimal version of owi opt has been implemented in #23.

Some easy ideas to start with:

• remove unused functions;
• remove unused globals;
• remove unused parameters (a little bit harder as it requires to update call sites);
• remove pure functions with empty return type.

Stack-based optimisations:

• Local optimization in a compiler for a stack-based Lisp machine;
• Optimisation Techniques for Stack Based Architectures;
• Stack-based typed assembly language.

Representations for optimisation:

• That’s a Tough Call : Studying the Challenges of
  Call Graph Construction for WebAssembly;
• Improving the Precision of Call Graph Construction for Webassembly with Symbolic Execution and Slicing;
• Global value numbers and redundant computations;
• An efficient method of computing static single assignment form;
• Combining analyses, combining optimizations;
• Compiling with Continuations, Continued.

Have a look at existing Wasm optimizers:

• binaryen;
• Low-Level Code Synthesis Using Constraint Programming;
• Ahead-of-time compilation in a language-independent environment.

allow to convert to reference interpreter AST

was started in c38c8ac

add exception support

see the exception proposal

data string init : error message

(module $m
  (data $d0 (memory $m0) (offset i32.const 0) "%]\"\148\020\182x\132\185F\235I\133o\190_Ar\150M\186\182\175>\132\1686\"\029C(\129\006\166\b<\138\160\176\0028U\218\217v+\012\159V,\127\177U\2510\192\253V\182;\148\018\191\248")
  (memory $m0 1)
  (start 0)
  (func $start   
  )
)

Memory initialization string from (data ...) instruction is not correct.
The official wasm interpreter launches this error message : syntax error: illegal escape
Owi launches this error message : Lexing error int_of_string
Is it possible to improve the Owi error message?

Bug optimize module

(module $m
  (start 0)
  (func $start   
    call $f
  )
  (func $f (local i32) (local i32) (local i32) (local i32)
    i32.const 0
    local.set 3
  )
)

This module is correct, but its interpretation after optimization launches this error :
owi: internal error, uncaught exception: Invalid_argument("index out of bounds")
Owi stack trace (debug mode) displays : local.set 1 instead of local.set 0
Only locale id:3 is used, so it must become id:0 after optimization.

crash instead of proper error on unknown label

(module
  (func $f

    (loop
      br 0
      br 1
      br 2
      (loop
        br 0
        br 1
        br 2
        br 3
        br 4
      )
    )
  ))

$ owi f.wast
owi: internal error, uncaught exception:
     Failure("nth")

Type checking error with drop

(module $m
  (memory $m0 6)
  (func $start
    (block $b0  (result i32)
      i32.const 42
      br $b0
      i32.eqz
      memory.size
      (if
        (then
          i64.const 0
          drop
        )
      )
      memory.grow
      drop
      drop
      i32.const 0
    )
    drop
  )
)

bring back boolify

try to bring back boolify which was removed in 35c3527 cc @chambart

add call_ref and return_call_ref

allow to have a function of type unit to unit in the host

which would have the empty type in wasm side

this requires to update the GADTs definition in value.ml

support binary format

we should be able to parse and print the binary format

add a --with-no-exhaustion flag

it would make sense only when --script is used, and would ignore all exhaustion tests from Wasm scripts, it's useful when debugging

Fix the conflicts that were introduced recently in the menhir grammar

Type checking error

(module $m
  (func $f0 (result f32)
    f32.const 0
    f64.const 0
    i32.const 0
    (if
      (then
      )
    )
    f32.demote_f64
    drop
  )
)

Owi launches this error : type mismatch (pop) requires [f64] but stack has [f32 f64]
while everything is ok with the official interpreter

Typing error

(module $m
  (start 0)
  (func $start
    ;; 1. OK Owi / KO! Official interpreter
    i32.const 1
    i64.const 2
    ;; 2. KO! Owi / OK Official interpreter
    ;; i64.const 2
    ;; i32.const 1
    (if  (param  i64) (param  i32)
      (then
        drop
        drop
      )
      (else
        drop
        drop
      )
    )
  )
)

This module seems to be correct in Owi but this error is launched with official wasm interpreter :
type mismatch: instruction requires [i64 i32 i32] but stack has [i32 i64 i32]
The behavior is reversed in case 2 (see comment 2).

data_mode pretty printer

(data ...) initialization instruction (in active mode) should be

(module $m
  (data $d0 (memory $m0) (offset i32.const 42) "string init")
  (memory $m0 1)
  [...]
)

instead of

(module $m
  (data $d0 ($m0 i32.const 42) "string init")
  (memory $m0 1)
  [...]
)

split the parser

we should at least split the script and module parts, see the doc in menhir https://cambium.inria.fr/~fpottier/menhir/manual.html#sec28

memory on 32 bits architecture

We're using Bytes for the memory, this works for 64 bits architectures. For 32 bits architectures, it limits the memory to 16Mo. We should write a library providing the Bytes interface with an implementation that uses something like Bigarray on 32 bits architecture and keeps Bytes on 64 bits architecture.

add a proper step by step debug mode

on the line of what was tried in 8255e93

data string init pretty printer

Format.fprintf fmt {|(data %a %a %S)|} id_opt d.id data_mode d.mode d.init

(types.ml - line 950)
Using %S tag to display the init string of the data instruction could produce errors.
For example, %S escapes special characters : check Issue #36

Of_bool / To_bool composition

Simplification of OfBool (ToBool x) into x is not correct. It doesn't erase the top bits

owi/src/symbolic_value.ml

Lines 128 to 131 in 4445d60

	let int32 = function
	| Val (Bool b) -> if b then mk_i32 1l else mk_i32 0l
	| Cvtop (I32 ToBool, e) -> e
	| e -> Cvtop (I32 OfBool, e)

_start function removed by binaryen

data pretty printer

MData { id = Some "id"; init = "str data init"; mode = Data_passive} printing should be

(data $id "str data init")

instead of

(data "str data init")

memory.fill error

memory.fill of negative values throws errors :
out of bounds memory access (first and third i32.const ...)
internal error, uncaught exception: Invalid_argument("Char.chr") (second i32.const ...)
These errors should be catch ?

(module $m
  (memory $m 1)
  (start 0)
  (func $start   
    i32.const -1
    i32.const -1
    i32.const -1
    memory.fill
  )
)

rec type pretty printer

(module $m
  (rec 
    (type $t [...]))
  [...]
)

Recursive types are not yet implemented in the reference interpreter : syntax error: unknown operator rec.
But when there's only one type, rec isn't useful in the pretty printer.

have a look at https://github.com/WebAssembly/tool-conventions

windows compatibility

The intrinsics library does not work on Windows. Actually, it seems that the few functions we're using could work. We could either:

• ask upstream to make it available on Windows and warn that some functions may fail at runtime
• vendor the few functions we need
• write a compatibility library that uses a pure OCaml implementation on Windows

some identifiers are added too late

For instance:

(module
  (func (export "f")
      unreachable)
)

After parsing, is desugared to:

(module
  (func
      unreachable)
  (export "f" (func))
)

But it should be:

(module
  (func
      unreachable)
  (export "f" (func 0))
)

Unfortunately, we add this back only after the group/rewrite/assign operation, which removes names (and we want to keep them for owi fmt).

We should probably add a first pass that handle this.

Reported by @Swrup when working on #83.

implement multi-memory proposal

https://github.com/WebAssembly/multi-memory

cc @Swrup

global_type pretty printer

The declaration of a non-mutable global variable should be

(module $m
  [...]
  (global $g i32 i32.const 0)
  [...]
)

instead of

(module $m
  [...]
  (global $g (i32) i32.const 0)
  [...]
)

memarg align pretty printer

let memarg [...] =
  [...]
  Format.fprintf fmt "offset=%d align=%d" offset align

(types.ml - line 532)
align should be interpreted as a power of 2 (2^align)

add a `owi simplify` command

That would be as owi fmt but printing the simplified module.

Empty model generated

"There should be a model. There is not" -- Pierre C.

(module
  (type (;0;) (func (result i32)))
  (type (;1;) (func (param i32)))
  (import "symbolic" "i32_symbol" (func $i32_symbol (type 0)))
  (import "symbolic" "assert" (func $owi_assert (type 1)))
  (func $_start
    (local $x i32)
    call $i32_symbol
    local.set $x
    ( call $owi_assert (local.get $x) )
    return)
  (export "_start" (func $_start))
)

CHECK:
(bool.not (i32.to_bool symbol_1))
/CHECK KO
PATH CONDITION:
Assert failure: (i32.to_bool symbol_1)
Model:
(model
)
Reached problem!

Solver time 0.000606s
      calls 1
  mean time 0.606000ms

add a `owi validate` cmd

cc @Swrup as it should be quite similar to fmt

add GC support

GC proposal is now stabilized

typechecker error

(module
  (func
    (block $b4 (result i32) (result f64)
      i32.const 0
      f64.const 0
      i32.const 0
      br_if $b4
      br $b4
      i32.const 0
      f64.const 0
    )
    drop
    drop
  )
)

found by fuzzing

add SIMD support

SIMD proposal is now part of Wasm

Example of unsound analysis in owi_sym

The following wasm is analyzed unsoundly by owi_sym. The assert should fail because of overflow but it does with an irrelevant model.

Model:
(model
  (symbol_1 i32 (i32 1))
)

(module
  (type (;0;) (func (result i32)))
  (type (;1;) (func (param i32)))
  (type (;2;) (func (param i32) (result i32)))
  (type (;3;) (func))
  (import "symbolic" "i32_symbol" (func $i32_symbol (type 0)))
  (import "symbolic" "assert" (func $owi_assert (type 1)))
  (func $__WASP_symb_int (type 2) (param i32) (result i32)
    call $i32_symbol)
  (func $__WASP_assert (type 1) (param i32)
    local.get 0
    call $owi_assert)
  (func $_start (type 3)
    call $__original_main
    drop
    return)
  (func $__original_main (type 0) (result i32)
    (local i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32)
    global.get $__stack_pointer
    local.set 0
    i32.const 16
    local.set 1
    local.get 0
    local.get 1
    i32.sub
    local.set 2
    local.get 2
    global.set $__stack_pointer
    i32.const 0
    local.set 3
    local.get 2
    local.get 3
    i32.store offset=12
    i32.const 1024
    local.set 4
    local.get 4
    call $__WASP_symb_int
    local.set 5
    local.get 2
    local.get 5
    i32.store offset=8
    local.get 2
    i32.load offset=8
    local.set 6
    i32.const 0
    local.set 7
    local.get 6
    local.set 8
    local.get 7
    local.set 9
    local.get 8
    local.get 9
    i32.gt_s
    local.set 10
    i32.const 1
    local.set 11
    local.get 10
    local.get 11
    i32.and
    local.set 12
    block  ;; label = @1
      local.get 12
      i32.eqz
      br_if 0 (;@1;)
      local.get 2
      i32.load offset=8
      local.set 13
      i32.const 1
      local.set 14
      local.get 13
      local.get 14
      i32.add
      local.set 15
      local.get 2
      local.get 15
      i32.store offset=4
      local.get 2
      i32.load offset=4
      local.set 16
      i32.const 0
      local.set 17
      local.get 16
      local.set 18
      local.get 17
      local.set 19
      local.get 18
      local.get 19
      i32.gt_s
      local.set 20
      i32.const 1
      local.set 21
      local.get 20
      local.get 21
      i32.and
      local.set 22
      local.get 22
      call $__WASP_assert
    end
    i32.const 0
    local.set 23
    i32.const 16
    local.set 24
    local.get 2
    local.get 24
    i32.add
    local.set 25
    local.get 25
    global.set $__stack_pointer
    local.get 23
    return)
  (table (;0;) 1 1 funcref)
  (memory (;0;) 129)
  (global $__stack_pointer (mut i32) (i32.const 8389648))
  (export "memory" (memory 0))
  (export "_start" (func $_start))
  (data $.rodata (i32.const 1024) "a\00"))

derived using waspc with all optimization deactivated from the following C file (example01)

#include <wasp.h>

int main() {
  int a = __WASP_symb_int("a");
  int b;

  if (a > 0) {
    b = a + 1;
    __WASP_assert(b > 0);
  }

  return 0;

}

avoid unneeded call to the Choice monad

cc @chambart

implement extended-const proposal

https://github.com/WebAssembly/extended-const

cc @Swrup

memory.grow error

memory.grow of a negative value throws an error :
owi: internal error, uncaught exception: Invalid_argument("Bytes.create")
This error should be catch ?

(module
  (memory 0)
  (func $start
    i32.const -1
    memory.grow
    drop
  )
  (start $start)
)

implement various exploration strategies

• Depth-First Search (DFS): Traverses states in depth-first order.
• Breadth-First Search (BFS): Traverses states in breadth-first order.
• Random State Search: Randomly selects a state to explore. See how it is implemented in KLEE.
• Random Path Selection: Described in KLEE OSDI’08 paper.
• Non Uniform Random Search (NURS): Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc. See how it is implemented in KLEE.
• Guiding Symbolic Execution with A* (see pre-publication).
• Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding;
• FeatMaker: Automated Feature Engineering for Search Strategy of Symbolic Execution.

make a version where we do not depend on z3

and fail at runtime saying the user should reinstall with z3 available

enforce check/typecheck passes through typing

to make sure we don't forget those
also add a function that do not perform the actual check and link it to a --unsafe flag when we know the module are correct to save time

Typechecking problem ?

This program is not correctly typed but when it is executed with Owi, the error is detected during the interpretation.
Typechecker should intercept it before ?

(module
  (start 0)
  (func
    i32.const -1
    i64.const 0
    i32.const 1
    (if  (param  i32) (param  i64)
      (then
        f32.reinterpret_i32
        drop
        drop
      )
      (else
        drop
        drop
      )
    )
  )
)

add locations

Add the line number to complete "running instr:" label

warning on module name shadowing with linking ?

force grow concretisation ?

cc @chambart

I found 0fd850c and I'm wondering if it's something we want to merge or what ?