lucet-validate

根据 witx 规范验证 WebAssembly 模块。

什么是 witx？

• Witx 是作为 WASI（https://github.com/WebAssembly/WASI）努力的一部分开发的规范语言。witx crate 存放在该仓库中，以及描述 WASI 标准的 .witx 文件。

• 由 witx crate 从 .witx 文件中解析和验证 Witx 规范。这些文件定义的类型和模块集合被称为 Witx 文档。

• Witx 规范包含模块，模块包含接口函数。这些函数是用参数（输入）和结果（输出）定义的，它们都可以具有复杂的类型，如指针、数组、字符串、结构体等。

• 每个接口函数都有一个方法来计算其类型签名，这个签名是用“核心”WebAssembly 类型（在 WebAssembly 1.0 函数类型中使用，如 i32、i64、f32、f64）表示的。这个计算考虑到了一些复杂类型作为线性内存中的指针传递，或者是一个指针长度对，而其他类型（如较小的 int，如 u8 或 s16）可以表示为原子值（在这个例子中是 i32）。

什么被验证？

• WebAssembly 模块本身被验证为 WebAssembly 1.0。我们目前不支持验证规范扩展，但应该能够在没有任何问题的前提下做到这一点。

• WebAssembly 模块的每个导入都被验证为存在，并且具有由 Witx 文档给出的预期核心类型签名。

• 如果验证器被设置为验证 wasi-exe，它还会检查模块是否导出了一个名为 _start 的函数，其类型签名是 [] -> ()。 (这不同于具有一个 start 部分，它是一个不同的概念，与 WASI 可执行程序的入口点 _start 不同。)

什么没有被验证？

• WebAssembly模块不包含足够的信息来确定在类型签名中找到的核心类型是以与witx文档中的复杂类型（字符串数组结构等）相匹配的方式被WebAssembly程序使用的。此属性只能在源语言编译为WebAssembly之前进行验证。