本文提出了一种在原生编译的 WebAssembly（Wasm）上实现软件故障隔离（SFI）安全保证的方法。研究背景在于，WebAssembly 最初设计为在浏览器中以解释或 JIT 方式运行，其内存安全依赖于运行时检查；然而随着 Wasm 被广泛应用于边缘计算、插件系统和云原生环境，越来越多的场景选择将 Wasm 直接编译为原生代码（AOT）以提升性能。但 AOT 编译会绕过原有运行时边界，导致 Wasm 固有的沙箱隔离能力退化，恶意或受损的 Wasm 模块可能直接访问宿主进程的地址空间，造成严重安全风险。为此，作者提出了一个名为 “Trust, but verify” 的框架，其核心思想是在不牺牲原生执行性能的前提下，通过静态验证与轻量级运行时检查相结合的方式，重新建立 SFI 边界。具体而言，该方法利用编译器在生成原生代码时插入必要的安全检查（如边界检查和间接调用目标验证），并辅以形式化方法证明这些检查的完备性，从而保证即使模块是恶意的，也无法逃逸其隔离域。作者在基于 LLVM 的原生 Wasm 编译器上实现了原型，并通过一系列安全相关基准测试和真实应用测试，验证了该方案能够有效检测并阻止多种越权访问尝试，同时性能开销远小于传统的纯软件沙箱方案。该研究适合系统安全、编译器安全和边缘计算领域的从业者，以及任何依赖 Wasm 插件生态的软件架构师阅读，以深入了解在不安全的原生执行路径上如何保持隔离保证的可行路径与工程权衡。