一句话：提出 WEST，从 SpecTec 机械化规范自动生成 Wasm 测试用例，在四个引擎中发现并修复多个缺陷。
WebAssembly 规范随提案不断演进，手工构建测试套件难以扩展，模糊测试又缺乏与形式规范的原则性联系。本文提出 WEST，一个基于规范的测试生成框架：以 Wasm 专用规范语言 SpecTec 编写的机械化规范为输入，针对完整或子集变体，系统生成符合语法与验证规则并覆盖执行语义的测试程序。框架支持灵活集成不同生成策略，文中展示自顶向下与自底向上两种 Wasm 模块生成方法，并可为仅实现规范子集的引擎定制测试用例。在多个规范变体与引擎配置上的评估表明，WEST 能生成有效且多样的测试用例，在四个 Wasm 引擎中发现 16 个缺陷，其中 11 个已确认并修复。
WebAssembly (Wasm) is a low-level binary instruction format designed for safe and high-performance execution across diverse computing environments and runtimes. As Wasm evolves with new features and proposals, testing the correctness and conformance of Wasm runtimes has become increasingly complex. Manually constructing test suites is labor-intensive and difficult to scale, especially as the specification grows in complexity. While fuzzing-based approaches offer partial automation, they often lack a principled connection to the formal specification, and adapting to evolving or restricted subsets of the specification typically requires manual intervention.In this paper, we present WEST, a specification-based test generation framework that automatically produces Wasm test cases from mechanized specifications written in SpecTec, a Wasm-specific specification language. Given any full or subset variant of the Wasm specification as input, WEST aims to systematically generate test programs that conform to the input grammar and validation rules, and capture the runtime behavior defined by its execution semantics. The framework allows flexible integration of different test generation strategies. For instance, we demonstrate both top-down and bottom-up approaches for generating Wasm modules, but the architecture is compatible with other generation techniques as well. The framework enables the creation of customized test cases for engines that support only subsets of the Wasm specification. We evaluate WEST across multiple specification variants and engine configurations, demonstrating that it produces valid and diverse test cases. As a result, it reveals 16 bugs across four Wasm engine implementations, 11 of which are confirmed and fixed. We believe that this work provides a solid foundation for future specification-driven test generation.
DOI 原文 ·
@inproceedings{paperbot9529,
title = {WEST: Specification-Based Test Generation for WebAssembly},
author = {Dongjun Youn and Wonho Shin and Sukyoung Ryu},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00119}
}