Wanilla：WebAssembly 的声音非干扰分析
密码学与安全
2025-09-11 v1
摘要
WebAssembly（Wasm）正快速获得作为嵌入various security-critical domains中软件组件分发格式的流行度。尽管其设计考虑周到，WebAssembly 作为内存不安全语言的主要编译目标仍然留下了内存损坏的可能性。独立于此之外，Wasm 作为一种具有接口角色的目标，对信息流分析本身具有内在的兴趣。Wasm 模块与其嵌入上下文之间的信息流，以及模块内部的内存完整性，都可由超属性非干扰（noninterference）描述。迄今为止尚未提出针对 Wasm 的全静态、完备的非干扰分析，但已有可靠的可达性分析。本工作提出了一种新颖且通用的方法，通过在值上跟踪污点并使用值敏感的关系推理来适时删除污点，从而将可达性分析提升为非干扰分析。我们在 Wanilla 中实现了该方法，这是首个自动、完备且全静态的 WebAssembly 非干扰分析工具，并通过多个合成和真实世界基准测试展示了其性能和精确度，验证了内存完整性和其他非干扰属性。
关键词
引用
@article{arxiv.2509.08758,
title = {Wanilla: Sound Noninterference Analysis for WebAssembly},
author = {Markus Scherer and Jeppe Fredsgaard Blaabjerg and Alexander Sjösten and Matteo Maffei},
journal= {arXiv preprint arXiv:2509.08758},
year = {2025}
}