In this paper, we present the design of Owi, a symbolic interpreter for WebAssembly written in OCaml, and how we used it to create a state-of-the-art tool to find bugs in programs combining C and Rust code. WebAssembly (Wasm) is a binary format for executable programs. Originally intended for web applications, Wasm is also considered a serious alternative for server-side runtimes and embedded systems due to its performance and security benefits. Despite its security guarantees and sandboxing capabilities, Wasm code is still vulnerable to buffer overflows and memory leaks, which can lead to exploits on production software. To help prevent those, different techniques can be used, including symbolic execution. Owi is built around a modular, monadic interpreter capable of both normal and symbolic execution of Wasm programs. Monads have been identified as a way to write modular interpreters since 1995 and this strategy has allowed us to build a robust and performant symbolic execution tool which our evaluation shows to be the best currently available for Wasm. Moreover, because WebAssembly is a compilation target for multiple languages (such as Rust and C), Owi can be used to find bugs in C and Rust code, as well as in codebases mixing the two. We demonstrate this flexibility through illustrative examples and evaluate its scalability via comprehensive experiments using the 2024 Test-Comp benchmarks. Results show that Owi achieves comparable performance to state-of-the-art tools like KLEE and Symbiotic, and exhibits advantages in specific scenarios where KLEE's approximations could lead to false negatives.

翻译：本文介绍了Owi的设计原理，这是一个用OCaml编写的WebAssembly符号解释器，并阐述了我们如何利用它构建了一个用于检测C与Rust混合编程中漏洞的先进工具。WebAssembly（Wasm）是一种可执行程序的二进制格式。该技术最初面向网络应用设计，凭借其性能优势与安全特性，现已成为服务端运行时和嵌入式系统领域的重要替代方案。尽管Wasm具备安全保证和沙箱隔离能力，其代码仍可能遭受缓冲区溢出和内存泄漏等漏洞威胁，这些漏洞可能对生产环境软件造成实际攻击。为防范此类风险，可采用包括符号执行在内的多种技术手段。Owi围绕模块化单子解释器构建，该解释器能够同时支持Wasm程序的常规执行与符号执行。自1995年以来，单子结构已被确认为实现模块化解释器的有效途径，基于此策略我们构建了鲁棒性强、性能优异的符号执行工具。评估结果表明，该工具是目前Wasm领域最先进的解决方案。此外，由于WebAssembly是多种语言（如Rust和C）的编译目标，Owi不仅能用于检测C和Rust代码的缺陷，还能应用于两者混合的代码库。我们通过典型案例展示了该工具的灵活性，并基于2024年Test-Comp基准测试进行了可扩展性评估。实验结果显示，Owi在性能上与KLEE、Symbiotic等前沿工具相当，并在特定场景中展现出独特优势——例如当KLEE的近似处理可能导致漏报时，Owi仍能保持检测准确性。