WebAssembly

破除误解：WASM 不是 JavaScript 的替代品，也不是「就是原生」#

WASM 不负责 DOM、不负责页面布局、不负责你熟悉的字符串运行时。浏览器里它通过 JavaScript 的 WebAssembly API 实例化，经导入函数与宿主说话。把 WASM 说成「要取代 JS」，忽略了语言分工：脚本仍是胶水，WASM 是计算核。边缘运行时和嵌入式宿主可以没有 JS，那是另一类嵌入，不是规范要求「必须有浏览器」。

第二个误解是把 WASM 当成原生机器码的别名。原生进程看到的是操作系统虚拟地址空间、可执行页、任意跳转、以及系统调用的环境权限。WASM 模块看到的是：一块（或几块）线性内存、一张函数表、结构化控制流、以及由宿主显式导入的函数。没有验证通过的模块不能启动。这使它更接近软件故障隔离（SFI）加类型化指令集，而不是「把 .so 换了个扩展名」。

第三个误解是：验证等于形式化证明了实现无漏洞。规范层的验证排除了一类非法指令与类型错误；引擎的编译器、JIT、信号处理器仍可能有实现缺陷。WASM 降低的是默认攻击面：任意指针算术不能直接指向宿主堆。它没有自动消灭逻辑漏洞、导入函数上的注入、或旁路。安全论证必须停在规范保证的那一层，不能写成「有 WASM 所以安全」。

线性内存、模块与执行模型#

线性内存是一块可按页增长的字节数组，页大小 64 KiB。MVP 里地址是 32 位，模块内部的指针只是这个数组上的偏移。越界访问被定义为陷阱，而不是未定义行为悄悄写到宿主。这与 C 的「越界就是 UB」不同：编译到 WASM 的 C 程序，其越界在引擎里变成可捕获失败，前提是编译器没有先在模块内部把逻辑搞乱。Memory 64 把地址空间做大，不改变「指针不得逃出线性内存」这条边界。

模块的组件是：类型、函数、表、内存、全局、导出与导入。表存放函数引用，用于间接调用；间接调用仍要核对类型标签，不能跳到任意字节偏移当代码。全局可以是不可变常数或可变单元，用于栈指针等 ABI 细节。启动时可选跑一个 start 函数。执行是栈式虚拟机：指令从栈取操作数、把结果压回。控制流是结构化的：block、loop、if、br 只能跳到外围块的标签，不能跳进块中间。这消灭了不可约控制流图，使验证可以一次前向完成。

数值类型在 MVP 里是 i32、i64、f32、f64。SIMD 后来加入 v128。引用类型、函数引用、异常、GC 堆上的结构体，把 WASM 从「C 的目标」推向「托管语言的目标」。每一类扩展都要回到验证：新指令的栈效应必须可判定，不能打开任意类型混淆。

验证：类型、栈与控制流#

验证器把函数体看成栈类型的状态机。每条指令有输入类型与输出类型；块有签名，分支必须与目标块的栈约定一致。不可达代码仍要类型良好，或被明确标成不可达。这套系统被做成小步语义和类型系统，并在规范里与执行语义并列——这在工业指令集里并不常见。Brendon 等人以及后来的形式化工作（包括 Isabelle/Coq 中的部分机械化）要证明的性质是：通过验证的模块，执行时不会对线性内存以外的宿主状态做未导入的访问，也不会把整数当成代码指针乱跳。

结构化控制流是可验证性的设计选择，不是审美。任意跳转的 CFG 需要可约性或更重的数据流分析才能保证栈高一致；WASM 直接禁止那种程序。从 LLVM 或 Cranelift 生成 WASM 时，必须把不可约流改写成块嵌套，必要时插入辅助块。这是编译器的税，换来的是引擎可以用一次线性扫描做完验证，并在流式下载尚未结束时就开始编译。

陷阱与回滚也在语义里。除零、越界、间接调用类型不符，使当前调用栈展开到宿主定义的边界。MVP 没有完整的异常，只有陷阱；后来的 exception handling 提案把 catch 放进结构化指令，仍然拒绝任意 unwinding 到未保护的宿主帧。验证关心的是类型与边界，不是「这段 C++ 逻辑对不对」。

WASI、组件与三处落地#

WASI（WebAssembly System Interface）要把「没有浏览器的 WASM」从「只有线性内存」变成「有能力做 I/O」。Preview 1 接近 POSIX 的一套文件、时钟、随机数导入，能力用文件描述符和预打开目录表示：模块默认看不见整个文件系统。Preview 2 转向组件模型（component model）：接口用 WIT 描述，值可以是字符串、列表、记录，而不是全挤在线性内存里自己约定 ABI。组件之间的链接由运行时做规范化，目标是让 Rust、Python、Go 的 WASM 产物互相调用，而不先经过 C ABI。

三处落地不要混成一句「WASM 到处跑」。

浏览器：下载、流式编译、与 JS 共享内存（共享 ArrayBuffer 时要面对数据竞争，线程提案引入 atomic 指令）。这里的威胁模型是恶意网页模块，沙箱必须对渲染进程负责。

边缘与无服务器：Cloudflare Workers、Fastly 等用 WASM 做隔离单元，冷启动比容器小。威胁模型是多租户：模块之间不能看见对方内存，导入的能力按请求授予。这里的性能故事是隔离密度，不是游戏帧率。

插件：Figma、游戏引擎、数据库扩展把不可信插件编译到 WASM，宿主只导入绘图或查询接口。这与浏览器同源策略无关，而与进程内插件的历史事故有关：原生插件一次越界就拿走整个应用。WASM 把插件重新放回可验证的指令集。虚拟化在这里是软件隔离，不一定是硬件虚拟机；与 虚拟化 的对照是：虚拟机切的是机器与操作系统，WASM 切的是模块与线性内存。

沙箱对原生：保证停在哪一层#

原生代码的内存安全依赖语言、页表和进程边界。C 的缓冲区溢出可以直接改返回地址。操作系统进程隔离很硬，但每个插件一个进程的代价，正是浏览器在站点隔离里付过的那种代价。WASM 选择第三条路：在同一进程里跑不可信计算，用验证过的指令集和线性内存当墙。墙的设计目标是 software fault isolation：故障停在模块里。

墙不覆盖：导入函数实现错误、JIT 编译器漏洞、时序与缓存旁路、以及故意导出的危险能力。把文件系统以可写根目录预打开，WASI 模块就接近有了一台小机器。能力列表才是安全策略；WASM 只保证策略之外的内存摸不到。与原生模块相比，默认权限从「和环境一样大」变成「只有导入表」。这是规范层的胜利，不是对所有漏洞的保险。

性能上，AOT 或基线编译后，计算密集型代码可以接近原生，前提是没有频繁进出宿主、没有边界检查无法消除的不规则访存。引擎用追踪与范围分析消除一部分检查；不能消除时，安全税就是多一次比较。这是刻意的税。

编译路径：验证之后才降到机器码#

浏览器通常先跑一次快速基线编译（Liftoff、JavaScriptCore 的 BBQ 一类），让模块在下载完成前就能开始跑，再对热函数做优化编译。验证必须在任何本地代码执行之前完成，或与流式编译交错但不得执行未验证块。Cranelift、Ion、B3 把栈式指令先变成 SSA，再做寄存器分配。结构化控制流在这里是礼物：块嵌套对应嵌套的 CFG 区域，不必先做不可约流的 node splitting。从 LLVM 前端来的不可约流，必须在降到 WASM 前改写，于是「WASM 比原生慢」有时量的是前端改写税，不是引擎。

SIMD 提案加入 128 位向量与车道操作，目的是让图像、编解码、线性代数不必降到标量循环。验证仍然按栈上的 v128 类型检查，不打开「把向量寄存器当成任意字节改写宿主」。线程提案允许共享线性内存加 atomic 指令；数据竞争的语义被写成非确定性的字节层结果，而不是 C++ 的 UB 可以摧毁整个进程。共享内存一旦打开，站点隔离与跨模块的内存隔离就要靠「不共享这块 ArrayBuffer」，而不是靠验证器。验证器不管你把内存导入给了谁。

多内存、尾调用、异常、GC 各自在验证里加规则。GC 提案引入托管对象引用，引用不能被整数伪造，也不能被线性内存里的加载凭空造出。这把「C 指针世界」和「托管世界」分成两种对象。语言若两边都要，必须经显式转换或复制。组件模型的规范适配器负责在线性内存布局与规范类型之间搬数据，避免每个语言自造一套 ABI。适配器本身也要可验证，否则组件边界会变成新的越界面。

能力：WASI 不是完整操作系统#

Preview 1 的文件 API 看起来像 POSIX，缺的是任意 open("/etc/passwd")。预打开目录是能力：模块只能在被授予的目录树下用相对路径走。随机数、时钟、环境变量同样按导入授予。网络套接字在 Preview 1 里基本缺席，边缘运行时用自己的导入（HTTP 对象、套接字 API）补上，于是可移植性在 I/O 层裂开。Preview 2 用 WIT 把「HTTP 发出去」写成接口，而不是假装所有宿主都是 Linux。这是诚实的分裂：计算核可移植，能力不可假装可移植。

插件宿主应当把导入表当成安全策略审查清单。只导入「把路径画到画布」的模块，与导入「任意文件与网络」的模块，验证结果可以同样通过。沙箱保证的是后者不能用指针摸到宿主堆，不是保证后者不能把用户文件读走。把 WASM 与「无权限」画等号，是把验证器的定理读成了能力系统的定理。两条定理要分开写。边缘运行时还把 CPU 时间与内存页数写成请求级配额：线性内存的增长会撞上宿主的页上限，陷阱在这里是资源隔离，不是类型错误。配额与验证一起，才构成多租户。页上限按请求重置，避免一个模块把线性内存胀到挤占同进程里的下一个租户。

代价与争议#

代价与争议#

MVP 刻意不做的事后来都变成争论。垃圾回收、异常、尾调用、多内存、线程，每一项都在「保持验证简单」和「让语言把 WASM 当真正后端」之间拉扯。GC 提案让托管语言不必把运行时塞进线性内存，却增加了规范与实现的耦合。组件模型要解决 ABI 混乱，自身又引入一套接口类型与规范适配器。可移植性的理想，会周期性地撞上「这一家引擎还没实现该提案」。

形式化与实现的距离是第二条争论。规范有核心数学，引擎有 Cranelift、Liftoff、Ion、JavaScriptCore 的 B3。验证通过不等于所有引擎在所有边角上语义一致。Web 的兼容性测试（wasm-spec tests）是社会契约，不是机器检查过的全覆盖。

生态上，把所有语言编译到 WASM 会暴露源语言的假设：Go 的大运行时、Java 的线程、C 的 UB。UB 在原生上是任意行为，在 WASM 上常常变成「模块内的任意行为」——对宿主仍隔离，对模块作者仍是灾。把 WASM 当成 UB 的消毒剂，期望过高。

跨域连接#

• 证明：WASM 的验证是可判定的类型证明：函数体要么在栈类型系统里可推出，要么拒绝。结构化控制流把「证明对象」从任意 CFG 的数据流不变式收成块嵌套的语法。规范把验证与小步语义并列，是为了让「通过验证 ⇒ 不越出线性内存」成为可陈述的定理，而不是引擎的口头保证。
• 范畴论：模块的导入导出是接口的态射：把宿主能力填进导入，得到可运行实例。组件模型把这一层从原始函数升到带类型的接口同态，链接成为合成。线性内存则是一个显式的对象，指针是内部态射，不能直接指到另一个对象（另一块宿主堆）上。隔离被写成不可见性，而不是事后检查。
• 信息哲学：线性内存把「程序知道什么地址」收成一块可观察的字节数组：模块的全部数据知识原则上可被这数组穷尽（加上表与全局）。原生进程的知识边界是页表与内核，观察者通常看不到完整状态。WASM 让沙箱的认识论变简单——可观察状态被规范列出来——也让人看清：一旦导入函数把外部世界接进来，这块穷尽性立刻消失。
• 组合学：结构化控制流限制了合法 CFG 的组合形状：只能是块的嵌套与按标签跳出，不能是任意有向图。合法程序是一种被计数限制过的组合对象。验证器的线性时间，来自这种组合限制，而不是来自更聪明的启发式分析。禁止不可约流，是用组合约束换证明可行性。

参考文献#

• Haas, A. et al. "Bringing the Web up to Speed with WebAssembly." Proceedings of PLDI, 2017.
• World Wide Web Consortium. WebAssembly Core Specification. W3C Recommendation, 2019（及后续版本）。
• Watt, C. "Mechanising and Verifying the WebAssembly Specification." Proceedings of CPP, 2018.
• WASI Subgroup. WebAssembly System Interface Preview 1 / Preview 2 规范文档，Bytecode Alliance。
• WebAssembly Community Group. Component Model 设计文档与 WIT 说明。

延伸阅读#

• Rossberg, A. 等关于 WASM 类型系统与提案演进的说明（社区组设计笔记）。
• Jangda, A. et al. "Not So Fast: Analyzing the Performance of WebAssembly vs. Native Code." USENIX ATC, 2019.