G.O.S.S.I.P 阅读推荐 2025-06-16 Empc：化繁为简，应对符号执行的路径爆炸难题

投稿团队简介：
Shuangjie Yao（姚双捷） is a first-year PhD student under the supervision of Dongdong She at the Hong Kong University of Science and Technology. He earned his bachelor’s degree from Shanghai Jiao Tong University. His research interests currently include program analysis. He was honored with the Distinguished Paper Award at the 2025 IEEE S&P. During his undergraduate studies, he took research internships at Microsoft Research Asia and Alibaba DAMO Academy.
Dongdong She（佘东冬） is an assistant professor at the Hong Kong University of Science and Technology, CSE department. He obtained his PhD from the CS department at Columbia University. Before Columbia, He earned his M.S. from UC Riverside and B.S. from Huazhong University of Science and Technology. He is broadly interested in security and machine learning. He is particularly interested in applying data-driven approaches (e.g., LLM, optimization) to solve traditional security problems (e.g., vulnerability detection, software testing, program analysis). PhD/RA/Visiting positions for both undergraduate and graduate students are available; if you are interested, email me at dongdong@cse.ust.hk.

在软件测试领域，符号执行作为一种强大的分析技术，能够系统性地揭示程序中的隐藏漏洞。然而，路径爆炸问题始终是符号执行的“阿喀琉斯之踵”。那么，有没有一种方法可以在不牺牲覆盖率的前提下，显著减少路径数目，并提升符号执行的效率呢？本文介绍香港科技大学在符号执行的新工作 Empc: Effective Path Prioritization for Symbolic Execution with Path Cover。该论文在今年五月召开的46th IEEE Symposium on Security and Privacy上获得展示并荣获杰出论文奖（Distinguished Paper Award）。论文第一作者是香港科技大学博士生姚双捷，由其导师佘东冬共同指导。

什么是路径爆炸（Path Explosion）？为什么它难以解决？

在符号执行中，程序的每一个分支条件都会产生新的路径。当程序规模变大时，这些路径的数量会呈指数增长（路径爆炸），导致计算资源消耗过大，甚至无法完成分析。如下图所示： 该程序有 3 个分支条件，那么理论上最多会出现6条路径。而在更复杂的程序中，路径数目可能轻松突破数百万！这样的规模不仅让分析时间剧增，还会让内存资源消耗殆尽。

Empc：用最少的路径覆盖最多代码

这项研究提出了一种全新的路径优先级技术，称为 Empc（Effective Path Prioritization with Path Cover）。其核心理念是并非所有路径都需要符号化求解。

Empc的关键创新点

1. 最小路径覆盖（MPC）

   Empc 利用图论中的最小路径覆盖算法，只选择少量的路径，这些路径能够覆盖程序中所有的代码区域。与传统方法需要分析指数级路径不同，Empc 只需分析一个小子集。

2. 多样化路径选择

   Empc 为了避免单一路径集的局限性，计算多个最小路径覆盖集（MPCs），以确保路径选择的多样性。

3. 动态路径调整

   如果某条路径在运行时被证明是不可行的，Empc 能够动态调整，选择新的路径继续执行。

Empc是如何实现的？——技术解析

Empc 的实现分为两个核心模块：

1. 基于图论的路径优先级（MPC 技术）

   Empc 将程序的控制流图（CFG）转化为无环图，并通过最小路径覆盖算法提取覆盖所有代码区域的路径集合。相比传统的符号执行方法需要探索所有路径，Empc 仅需要探索这些少量路径即可完成分析。假设程序中有 6 条可能的执行路径，传统符号执行可能需要穷尽所有路径，而 Empc 只需选择 3 条路径即可覆盖全部代码。

2. 处理不可行路径

   在符号执行中，不可避免地会遇到一些路径因约束条件无法满足而变得不可行。Empc 引入了经典的程序依赖分析，通过追踪变量和分支之间的依赖关系，动态调整路径选择，确保符号执行能够继续进行。

Empc的效果如何？

研究团队在符号执行工具 KLEE 上实现了 Empc，并在 12 个开源程序上进行了全面评估。

1. 代码覆盖率：比 KLEE 的最佳搜索策略多覆盖 19.6% 的基本块；比当前最先进的路径搜索方法（cgs）多覆盖 24.4% 的代码行数。
2. 资源消耗：内存使用量减少最多 93.5%；符号状态数减少最多88.6%。
3. 漏洞发现能力：Empc 在 8 个程序中发现了 24 个比其他方法更多的安全漏洞。

结语

符号执行作为软件测试的重要技术，未来仍有许多挑战等待解决。 Empc通过结合图论与程序分析技术，在提升覆盖率的同时，显著降低了资源消耗，展示了符号执行的全新可能性。

如果您对 Empc 有兴趣，欢迎访问论文地址

https://arxiv.org/abs/2505.03555

和代码仓库

https://github.com/joshuay2022/empc

或第一作者个人主页

https://sjyao.net

原文始发于微信公众号（安全研究GoSSIP）：G.O.S.S.I.P 阅读推荐 2025-06-16 Empc：化繁为简，应对符号执行的路径爆炸难题