Page 134 - 《软件学报》2024年第6期

2710 软件学报 2024 年第 35 卷第 6 期

供了一个平面内存模型的抽象, 在 GPU 上自动交错底层虚拟机的地址空间, 为 GPU 加速提供了新的机会.

5.3 二进制符号执行

符号执行作为一种强大的软件分析和错误检测技术, 根据处理对象不同可以分为两种: (1) Source-based 符号
执行. 在源代码可用的前提下, 利用编译器将其编译为 IR 后再植入符号执行信息; (2) Binary-only 符号执行. 对于
源代码不可用的二进制程序, 利用二进制翻译将其变换为 IR 后再植入符号执行信息. 然而, 在实际情况中大多数
程序不提供源代码, 基于 Binary-only 二进制符号执行被广泛使用.
Shoshitaishvili 等人 [194] 提出符号执行翻译器 Angr, 它基于 VEX IR 对关键符号信息插桩并符号化解释执行,
对于不带符号的代码采用具体执行方式. Angr 具有较强的通用性, 但执行速度较慢. 为了将 Source-based 符号执
行系统 KLEE 扩展到第三方依赖库和操作系统内核, Chipounov 等人 [195] 创建了 S2E 系统. S2E 使用 QEMU 将目
标程序从二进制转换为 TCG IR, 之后将包含符号信息的 TCG IR 进一步转换为 LLVM 字节码并传递给 KLEE, 最
后使用 KLEE 符号化解释执行. S2E 相比于 Angr 的设置和运行更复杂, 但程序分析范围更加全面. 不足的是, S2E
与 Angr 的性能均较差. QSYM [196] 作为一个高性能的二进制符号执行工具, 利用动态二进制翻译技术将符号执行
与本地原生执行紧密集成, 实现更细粒度、更快的指令级符号分析与执行. QSYM 不再依赖目标程序的 IR 做符
号插桩, 而是直接基于指令级进行符号插桩与翻译, 相较于基于 IR 的符号执行具有更强的鲁棒性. 然而, QSYM
面向 x86 指令集设计, 迁移到其他架构难度较大.
Poeplau 等人提出一种 Source-based 的符号执行器 SYMCC [197] , 它在程序源代码的编译阶段插入符号信息. 实
验结果表明, SYMCC 的执行性能相比于 QSYM 可以提升两个数量级, 但 SYMCC 基于源码编译插桩的设计方法
限制了其面向二进制文件的分析使用. 受 SYMCC 启发, SymQEMU [30] 关注如何实现基于编译的符号执行在二进
制文件上工作. SymQEMU 将二进制翻译和符号执行充分融合, 基于 QEMU 设计了面向二进制的符号分析工具,
通过插桩 TCG IR 中间代码来建立符号约束表达式. 与 Anger 和 S2E 相比, SymQEMU 的执行效率更高. 与
QSYM 相比, SymQEMU 在保持高效的同时具有平台可扩展性. 此外, 测试结果表明 SymQEMU 在执行效率和测
试覆盖率方面优于 SYMCC 技术. 表 9 给出了上述基于二进制翻译的符号执行工具的对比情况.

表 9 基于二进制翻译的符号执行工具对比
利用动态二进制翻译技术实现了
工具 实现语言 IR类型 执行效率 支持多平台 基于二进制程序 跨平台执行
Angr [194] Python VEX 低 √ √ √
S2E [195] C/C++ TCG & LLVM 低 √ √ √
QSYM [196] C++ 无 高 × √ ×
SYMCC [197] C++ LLVM 高 √ × ×
SymQEMU [30] C/C++ TCG 高 √ √ √

5.4 虚拟化
虚拟化技术可以在一个特定的抽象层中, 使用下层系统提供的接口为上层系统实现约定接口的功能. 虚拟化
技术被应用于子系统、组件以及整个计算机系统. 二进制翻译本身作为一种虚拟化技术, 其在虚拟化应用中被广
泛采纳.
VMware 虚拟平台 [198] x86 架构 CPU 的完全虚拟化, 允许多个操作系统环境
在 x86 的 PC 机上并发运行. Transmeta 公司推出的 Crusoe 微处理器 [4] 采用软硬件协同设计的二进制翻译技术实
现指令集虚拟化. Cota 等人 [15] 提出了基于动态二进制翻译的跨指令集多线程模拟器 Pico, 它可以在保持速度、可
移植性和正确性的同时, 在多核主机上高效的模拟多核客户机, 支持 64 核的全系统虚拟化. QEMU 在虚拟化中被
广泛使用, 可以提供对多种源平台的虚拟支持. 著名的 KVM [199] 和 Google Android [186] 等模拟器均是基于 QEMU 的
二次开发实现.
Wang 等人 [19] 结合龙芯 GS464E 处理器和 QEMU 二进制翻译融合, 实现了软硬件融合的访存虚拟化优化.
Huang 等人 [90] 利用二进制翻译技术提出了一种名为 BTMMU 的跨 ISA 内存虚拟化方法. Spink 等人 [9] 利用二进制