华为云 WebAssembly 代码静态符号执行技术实现新突破

2023-11-23
广东
本文字数：1620 字
阅读完需：约 5 分钟

本文分享自华为云社区《华为云WebAssembly代码静态符号执行技术实现新突破，相关论文被软件工程顶会ISSTA2023接收并荣获杰出论文奖》，作者：华为云软件分析 Lab 。

WebAssembly（Wasm）最初由 W3C 的 Mozilla、谷歌、微软、苹果等著名公司合作研发，最初是作为浏览器内应用程序的高性能执行引擎。因为 Wasm 的高性能、多语言支持、安全性和可移植等特性，Wasm 也正在从 Web 走向云、边缘和嵌入式，成为软件创新的热点。鉴于 Wasm 的优越特性，业界专家一致预测 Wasm 语言在云计算场景中的应用将会越来越广泛。然而针对 Wasm，业界目前缺乏成熟、高效的静态符号执行引擎，而且当前的符号执行路径搜索技术通常过于粗糙，主要支持整个程序的全局搜索策略，但不同的代码块可能适合不同的局部策略，这使得 Wasm 的缺陷发现存在较大挑战。

静态符号执行技术是程序分析领域中至关重要的一项技术，可以在软件源码中寻找软件缺陷为填补这一业界空白，，相关的分析和优化方法一直在学术界和工业界得到持续关注。但是，符号执行会遇到路径爆炸的问题。在实践中，用户经常需要利用各种搜索策略来指导符号执行以达到他们的分析目标，减少路径爆炸，但是现有的基于搜索或者引导的符号执行方法通常过于粗糙，它们主要支持整个程序的全局搜索策略，但不同的代码块可能适合不同的局部策略。而对于 WebAssembly（Wasm），目前尚无成熟、高效的符号执行引擎。

针对上述问题，华为云 PaaS 技术创新 LAB 联合北京大学郭耀教授、李锭助理教授研究团队，针对 WasmWebAssembly 代码孵化开发了一个可工业场景落地的静态符号执行引擎服务 Eunomia。该工作对应论文“Eunomia: Enabling User-Specified Fine-Grained Search in Symbolically Executing WebAssembly Binaries”已被软件工程顶会 ISSTA 2023 在 2023 年国际软件测试与分析会议（2023 ACM International Symposium on Software Testing and Analysis 2023, ACM ISSTA 2023）录用发表上，发表题为 “Eunomia: Enabling User-Specified Fine-Grained Search in Symbolically Executing WebAssembly Binaries” 的论文，并荣获 “荣获该会议的 ACM SIGSOFT 杰出论文奖（Distinguished Paper Award）”。论文第一作者为北京大学计算机学院 2019 级博士生贺宁宇。

图 1 ACM SIGSOFT 杰出论文奖证书

Wasm 是在泛在计算领域广泛使用的一种新的中间语言范型，可以为 C/C++、Go 等语言提供统一的泛在应用执行环境。Wasm 已被广泛应用于网络应用程序、区块链应用以及服务器无感知（severless）应用。但是现有的针对 Wasm 的符号执行引擎不完全支持 Wasm 接口（WASI），导致应用范围受限。研究团队针对 Wasm 语言的特点设计了一种领域专用语言（DSL）AES Script，该语言允许用户将先验知识形式化的引入到被测试程序中。通过作者提出并实现的基于用户细粒度知识引导的 Wasm 符号执行引擎，相较于目前的前沿工作，该工作可以将针对 Wasm 语言的静态符号执行分析效率提升一到两个数量级，成功在实际应用和系统中发现了多个 0-Day 漏洞，证明了该工作的有效性，并为后续工作指出了一个新的研究方向。

图 2 论文工作的框架与工作流图

实验结果表明，在 Logic Bomb 基准测试集上成功触发逻辑炸弹和超时的案例数量上，Eunomia 明显优于 Manticore。在所有 12 个类别中，Eunomia 在专注于符号内存、浮点数和外部库函数的逻辑炸弹方面有更好的表现。对于分析真实世界的应用程序，结果如表 2 的第三列和第四列所示。我们可以看到，在 8 个应用程序中，Manticore 只能在 2 小时内完成对 3 个应用程序的分析，而 Eunomia 的数量是 5 个。此外，很容易观察到，与 Manticore 相比，Eunomia 的效率提高了一到两个数量级，并发现了 2 个新漏洞。