Have you seen wasm-metering?

[void4]

https://github.com/ewasm/wasm-metering is a library that injects resource metering into webassembly binaries.

This WebAssembly module is the input:


(module
    (func $custom
        nop
    )
    (export "custom" (func $custom))
)



And this is how the transformed, metered code looks like.
A function ("metering/usegas") is added as an import.
It has one argument (the gas that is used in the block after the invocation).
At the top of every block (sequences, conditionals or loops),
this value is pushed on to the stack (here: 32).
Then the function is called. The function adds this value to an external counter.
This counter must not be accessible by the wasm code. wasm-metering also
checks that the usegas function is not called manually, 
to prevent overflow attacks. Usegas raises an exception if the counter
surpasses a certain value (the gas limit) and stops the WebAssembly instance.

(module
    (import "metering" "usegas" (func $usegas (param i32)))
    (func $custom
        i32.const 32
        call $usegas
        nop
    )
    (export "custom" (func $custom))
)

If you have already seen it, what do you think of it? I'd also be interested in your opinion on WebAssembly in general.

[erights]

If you have already seen it, what do you think of it?

I like this approach to metering in general, and I like its application to wasm specifically. The phrase "raise an exception" is alarming if it implies that it could be caught by a try-catch higher on the stack. I have been assuming, though I don't know, that the injection of a gas model into wasm by transformation also turns out-of-gas into a wasm trap.

I'd also be interested in your opinion on WebAssembly in general.

Very positive, though I think some of its fans have overlooked some of its current problems. I left the Google wasm team to form Agoric, but remain on the wasm standards committee. Wasm currently has the ocap safety properties but not the ocap expressiveness properties. Andreas' "reference types" proposal, making opaque function references passable by argument and result over function invocations, brings much of ocap expressiveness to wasm used as a coarse (OS-like) ocap system, where the wasm compartment (approx module instance) is the unit of protection. Andreas' longer term wasm-gc proposal would turn wasm into a real fine-grain ocap machine. At that point it will become much more relevant to us.

Since you raise this issue on the Jessie repository, I'll point out that it should be straightforward to implement Jessie on wasm. Jessie is a simple Scheme-with-records-like language, so one might start with @eholk 's implementation of Scheme on wasm.

[void4]

Thank you for your response!

Can you elaborate on why an exception would be alarming?

The systems that use this metering library use a Javascript-based Wasm embedding environment, and the usegas function is implemented in Javascript (though it could be implemented by another Wasm instance that is securely separated).

One of the limitations of browser based Wasm implementations is that the exception raised in the Javascript function destroys the Wasm instance and with it all interpreter state, the program cannot be resumed.

I'm working on extending a Javascript Wasm interpreter to allow for the usegas funcion to serialize all runtime state, including the stack, which is not accessible in other implementations due to optimization.

I'm interested in this because it provides a different semantics, instead of "success/abort", or "success/revert" as in the Ethereum Virtual machine, it could be a "suspend->refuel->resume" semantics. Another feature is the recursive sandboxing of modules, a lot like the Genode operating system does it - but on the language level. Wasm seems to be the first general purpose, portable object format that ensures proper isolation. I wrote more here, much is inspired by your papers: void4/notes#23