Wanilla：WebAssembly 的可靠非干扰分析
Wanilla: Sound Noninterference Analysis for WebAssembly
AI总结：
本文提出 Wanilla，首个针对 WebAssembly 的自动、可靠且完全静态的非干扰分析工具，通过污点跟踪和值敏感关系推理将可达性分析提升至非干扰分析，并验证了内存完整性等属性。
摘要：
WebAssembly（Wasm）作为一种软件组件分发格式，正迅速在多个安全关键领域中获得普及。不幸的是，尽管其设计审慎，WebAssembly 作为内存不安全语言的编译目标这一主要用例，仍为内存损坏留下了一些可能性。与此独立的是，由于 Wasm 的接口作用，它天然是信息流分析的一个有趣目标。Wasm 模块与其嵌入上下文之间的信息流，以及模块内的内存完整性，都可以用超属性非干扰来描述。迄今为止，尚未有对 Wasm 的可靠、完全静态的非干扰分析被提出，但已有可靠的可达性分析。这项工作提出了一种新颖且通用的方法，通过跟踪值上的污点，并使用值敏感的、关系推理在适当时候移除污点，从而将可达性分析提升到非干扰分析。我们在 Wanilla 中实现了这种方法，这是第一个针对 WebAssembly 的自动、可靠且完全静态的非干扰分析，并通过验证内存完整性及其他非干扰属性，使用多个合成和真实世界基准，展示了其性能和精度。
英文摘要：
WebAssembly (Wasm) is rapidly gaining popularity as a distribution format for software components embedded in various security-critical domains. Unfortunately, despite its prudent design, WebAssembly's primary use case as a compilation target for memory-unsafe languages leaves some possibilities for memory corruption. Independently of that, Wasm is an inherently interesting target for information flow analysis due to its interfacing role. Both the information flows between a Wasm module and its embedding context, as well as the memory integrity within a module, can be described by the hyperproperty noninterference. So far, no sound, fully static noninterference analysis for Wasm has been presented, but sound reachability analyses were. This work presents a novel and general approach to lift reachability analyses to noninterference by tracking taints on values and using value-sensitive, relational reasoning to remove them when appropriate. We implement this approach in Wanilla, the first automatic, sound, and fully static noninterference analysis for WebAssembly, and demonstrate its performance and precision by verifying memory integrity and other noninterference properties with several synthetic and real-world benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
