Stream: wasmtime

Topic: Pulley validation


view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:42):

It's not clear to me from the RFC whether Pulley will provide a similar validation mechanism as Wasm to guarantee sandboxing (reducing the number of runtime tests). I would guess no, because the goal is to be a target, so validation is done before compiling to Pulley. But I would like to know whether this interpretation is correct. And also what would be the cost to restore sandboxing (where are runtime checks needed, what additional data the runtime needs). Thanks!

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:44):

Could you clarify what you mean by validation in this context? Usually in Wasmtime when we say "validation" we mean Wasm validation, which happens at translation time (to machine code for Cranelift and Winch, or Pulley bytecode for Pulley) regardless

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:44):

You also mention sandboxing however, which has to do with strictly runtime properties like concrete memory access patterns. Those undergo the same set of optimizations our other Cranelift targets do, because we use Cranelift to compile to PBC

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:45):

Yes I mean validation as in type checking

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:45):

Which provides some soundness property

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:45):

Necessary for proper sandboxing

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:46):

(at least as I understand it)

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:46):

OK, yes, so as above, that always happens at compilation time -- whether compilation to machine code or Pulley bytecode.

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:46):

Sandboxing also needs some runtime checks, but those are reduced because we don't need to track types at runtime

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:47):

Ok I see. I was planning to use Pulley as an untrusted "source". So I'll need some additional mechanism to guarantee its behavior

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:48):

Yes, the bytecode has the same security properties as Wasmtime's precompiled machine code (cwasm files) -- that is, we trust it absolutely, and the raw PBC opcode set includes raw loads and stores

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:48):

so you'll need to have a trusted way of e.g. vetting hashes, if you don't trust the store or the transport from wasmtime compile to the execution context

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:48):

(essentially a notion of Pulley applets, because I can't have a Wasm to Pulley compiler on device)

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:49):

Yes exactly, thanks!

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:49):

One other thing to note here is that we haven't really given thought, as far as I know, to stability of the format: the expectation is that the versions match between compiler and interpreter backend. If you have a fleet of devices in the field with different versions you'll need to keep all the compiler versions active

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:49):

and manage versioning appropriately

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:50):

I see, that's good to know. I assumed the format would eventually be stable

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:51):

We might go that way if there's demand and if we're satisfied that it includes what we need; but so far the thing is very early stages

view this post on Zulip Chris Fallin (Oct 21 2024 at 20:51):

(I'll let @fitzgen (he/him) speak more to his long-term vision here, I'm mostly repeating what I've understood about it)

view this post on Zulip Julien Cretin (ia0) (Oct 21 2024 at 20:54):

Sounds good, thanks for your answers!

view this post on Zulip fitzgen (he/him) (Oct 21 2024 at 23:55):

the emitted pulley bytecode will have things like hard-coded vmctx offsets in it, so even if the pulley instructions themselves don't change, the bytecode will not really be usable across Wasmtime versions

this is the same as how the machine code that wasmtime creates via cranelift for a compiled wasm module is not reusable across wasmtime versions, despite x86 (for example) instructions not changing between wasmtime versions

you always have to match the wasmtime version that runs the pre-compiled machine code or bytecode with the wasmtime that did the compilation to produce that code

view this post on Zulip fitzgen (he/him) (Oct 21 2024 at 23:58):

re validation and sandboxing:

view this post on Zulip fitzgen (he/him) (Oct 21 2024 at 23:59):

if anything is not clear, please let me know which parts, and I can try to clarify

view this post on Zulip Julien Cretin (ia0) (Oct 22 2024 at 06:05):

Thanks! This is pretty clear. I was thinking of Pulley as a portable bytecode like Wasm (but interpreter friendly). But that's actually not the case. It is really more of an internal implementation detail of wasmtime.


Last updated: Nov 22 2024 at 17:03 UTC