一句话：提出并评估 WasmCert，融合静态检查、源级启发式、运行时陷阱证据与可选 SMT 后检查的 WebAssembly 安全分析原型。
WebAssembly 已广泛部署于浏览器、边缘平台与服务端运行时，但针对 Wasm 制品的可复现安全分析流水线仍然有限。本文提出 WasmCert，一个混合安全分析原型，结合 token 级静态检查、源级启发式规则、运行时陷阱证据以及可选的 SMT 后检查。在包含 355 个面向漏洞的用例基准上，WasmCert 达到 86.48% 的检测率，而仅运行时基线仅为 8.17%（p = 4.12 × 10^-84）。在面向安全的质量视角下，精确率为 96.21%，特异性为 97.57%；启发式消融实验表明源级启发式贡献了 39.72 个百分点。
WebAssembly (Wasm) is increasingly deployed across browsers, edge platforms, and server-side runtimes, yet reproducible security-analysis pipelines for Wasm artifacts remain limited. We present WasmCert, a hybrid prototype that combines static token-level checks with source-level heuristics, runtime trap evidence, and optional SMT post-checking. On a benchmark of 355 vulnerability-oriented cases, WasmCert achieves 86.48% detection versus 8.17% for a runtime-only baseline (p = 4.12 × 10-84). Under a security-focused quality view, Precision is 96.21% and Specificity is 97.57%. Heuristic ablation attributes 39.72 percentage points to source-level heuristics.
@inproceedings{ZhangLRHT26,
title = {WasmCert: A Reproducible Hybrid Security Analysis Prototype for WebAssembly},
author = {Haoyi Zhang and Tianfeng Liang and Huaijin Ran and Md Maruf Hasan and Xunzhu Tang},
booktitle = {FSE},
year = {2026},
doi = {10.1145/3803437.3807382}
}