finite-wasm

Cheating a little to solve the halting problem at scale

Guarantee deterministic limits on execution time and space resources made available to the WebAssembly programs in a runtime-agnostic way.

Contents

This projects provides a couple things:

• Ammendments to the WebAssembly core module specification describing the changes to the execution model such that the resource use is kept track of and limits are enforced;
• Analyses that inspect a given WebAssembly module and produce the information necessary to enforce the limits based on the amended execution model;
• A test suite validating the implementation of analyses against a modified reference WebAssembly interpreter.

The results of the provided analyses can be utilized quite flexibly: to instrument the WASM code; to augment the machine code generated during compilation of the WASM code; to enforce the resource limits at the interpreter runtime; or some other way, thus achieving the portability properties of this project.

Using finite-wasm

The test suite implements a rudimentary WebAssembly module transformation pass. The intent is for it to be just enough to validate the properties of the analyses against the reference interpreter, but it can definitely be taken as a base and adapted into a full production-grade transformation. This is probably the best way to start with.

However this approach may prove to be less than satisfactory performance wise. Transforming a WASM module will require parsing it, modifying it and then serializing it again. While parsing the WASM module at least twice may be be unavoidable, the analyses are constructed such that modification and re-serialization of the modules is not required.

Examples

use finite_wasm::{wasmparser as wp, prefix_sum_vec};

struct MySizeConfig;
impl finite_wasm::max_stack::SizeConfig for MySizeConfig {
    fn size_of_value(&self, ty: wp::ValType) -> u8 {
        use wp::ValType::*;
        match ty {
            I32 => 4,
            I64 => 8,
            F32 => 4,
            F64 => 8,
            V128 => 16,
            FuncRef => 32,
            ExternRef => 32,
        }
    }

    fn size_of_function_activation(
        &self,
        locals: &prefix_sum_vec::PrefixSumVec<wp::ValType, u32>,
    ) -> u64 {
        u64::from(locals.max_index().map(|&v| v + 1).unwrap_or(0))
    }
}

macro_rules! define_fee {
    ($(@$proposal:ident $op:ident $({ $($arg:ident: $argty:ty),* })? => $visit:ident)*) => {
        $(
            fn $visit(&mut self $($(,$arg: $argty)*)?) -> Self::Output { 1 }
        )*
    }
}

struct MyGasConfig;
impl<'a> wp::VisitOperator<'a> for MyGasConfig {
    type Output = u64;
    wp::for_each_operator!(define_fee);
}

fn analyze_module(wasm_code: &[u8]) -> finite_wasm::AnalysisOutcome {
    finite_wasm::Analysis::new()
        .with_stack(MySizeConfig)
        .with_gas(MyGasConfig)
        .analyze(wasm_code)
        .expect("something went wrong!")
}

License

This project is licensed under the MIT or Apache-2.0 license.