谁能帮忙解释一下 WebAssembly design rational 中显示的 "one-pass verification" 过程

Can anyone help explain the "one-pass verification" process shows in WebAssembly design rational

"one-pass verification"是什么意思?为什么基于堆栈的机器可以简化这个过程?

此外,我在 WebAssembly 文档 "Semantic->Validation" 部分找到了以下句子:

A module binary must be validated before it is compiled.

我想知道何时会进行验证过程?在 "wat2wasm" 的过程中还是在任何其他阶段?谢谢!

One pass verification 意味着您不必遍历字节码两次来收集验证程序所需的所有信息。

它依赖于两个机制:

线性记忆与代码脱节space;执行栈;引擎控制结构,因此您的程序不能跳转到任意位置或破坏执行环境。因此引擎不必在运行时进行繁琐的检查以确保内存安全。如果它完全消除了内存安全漏洞的风险?我无法回答。我相信 Spectre/Meltdown 错误确实导致某些引擎限制了 WebAssembly 执行引擎的权限。

结构化控制流意味着通过构造的程序不能形成不可约循环或包含分支到堆栈高度未对齐的块。

结构化控制流部分简化了解析和验证机制。每条控制流指令都包含在一个块中,这意味着对于前向跳转,我们已经知道目的地,无需再次解析程序即可找到。

validation process 发生在编译之前。例如,在 Firefox 中,它隐藏在一个迭代器后面,该迭代器从二进制代码的 reader 获取数据并将每条指令传递给编译器。这是验证每个函数体的函数:https://searchfox.org/mozilla-central/source/js/src/wasm/WasmValidate.cpp#903

实际验证是通过将操作数放在类型堆栈上并验证该堆栈上的类型与指令的类型相匹配来完成的。 Firefox 的一些代码摘录:DecodeFunctionBodyExpr has a case clause for a bunch of i32 functions such as i32.add, i32.sub, i32.mul which all take two i32 operands. From there ReadBinary is called which calls popWithType 每个操作数一次。在 popWithType 内部,可以访问用于跟踪操作数的类型堆栈。如果类型不匹配,则会向调用链发出错误信号。

Ben Smith 撰写了一篇博客 post WebAssembly type-checking,其中解释了如何对教学图片进行类型检查。 WebAssembly 的类型检查很简单,除了控制流中无法访问的代码。有关如何使用 "polymorphic stacks".

解决问题的说明,请参阅 post 的最后一节