WASCII: Bridging WebAssembly Specifications and Implementations through LLM-Enhanced Validation

Abstract

The rapid evolution of WebAssembly (Wasm) has led to significant implementation inconsistencies between its specification and the behavior of various Wasm runtimes, posing critical threats to application reliability and security. Verifying that a runtime's implementation adheres to the natural-language specification is a profound challenge. While Large Language Models offer a promising way to bridge the semantic gap between specification text and source code, their inherent fallibility makes them untrustworthy for direct verification. In this paper, we introduce WASCII, a novel framework for bridging specification and implementation with execution-based validation. Our approach first constructs a Check Tree from the natural-language specification, which captures the validation rules that runtimes must enforce. We then align runtime code to the Check Tree, and employ a Clean Room design with execution-based validation to ensure the correctness of the bridging. The validated test cases are then used for cross-runtime differential testing to identify behavioral inconsistencies. Evaluated on seven major Wasm runtimes, WASCII identified 248 differential behaviors, among which 35 are confirmed as previously unknown specification conformance issues, with 17 confirmed or fixed by developers. These results demonstrate that our approach is a highly effective strategy for discovering subtle yet critical bugs in complex systems.