1282740 - Wasm verifier does not catch some invalid programs

Status: RESOLVED FIXED

(Core :: JavaScript Engine: JIT, defect, P1)

Description

[Lars T Hansen [:lth]]

The background is bug 1280930 comment 5 and later; also discussed with Dan on IRC.

The verifier pushes a void value at the beginning of blocks to ensure that there's always a value on the stack.  This trick allows non-well-formed bytecode programs to consume that value, and some of those programs will then be deemed valid.  For example, the program

   nop
   i32.const 1
   select

will be deemed valid (with type void).  This is wrong, both because it consumes a value that is not technically present and because the type of select should probably never be void (this last observation due to Dan, I don't have anything to back it up with).

Generally speaking, I'm concerned about having too few test cases that test that we reject illegal programs properly.  One possibility is for bytecode combinations to be generated (randomly or systematically) and for our verifier to be tested in lockstep with the reference implementation; we should reject iff the reference implementation does.

Comment 1

[Dan Gohman [:sunfish]]

At the spec level, the explicit drop proposal [0] has recently landed, so this is already an area that is going to need several changes in Baldr already. It's now looking likely that we'll eliminate the "void" type altogether.

Also, I agree that we have too few tests for invalid bytecode.

[0] https://github.com/WebAssembly/design/pull/694

Comment 2

[Christian Holler (:decoder)]

If you can provide a reference command line tool that correctly rejects testcases that the jsshell otherwise would accept, then we might be able to automate this for you (no guarantee though, especially time-wise). We can also advise you how to build/run such a tool yourself, so you can create tests from the results directly.

Comment 3

[Lars T Hansen [:lth]]

Dan, is this still an issue after 0xC landed?

Comment 4

[Dan Gohman [:sunfish]]

Right, with 0xc this is no longer an issue. Void is no longer a value that gets pushed on the stack.