2025 Let’s GoSSIP 软件安全暑期学校预告第二弹——Empc

Let’s GoSSIP 软件安全暑期学校的课程内容，向来不缺少高水平的学术研究成果，今年也不例外：我们有幸邀请到了获得2025年IEEE S&P 杰出论文奖（Distinguished Paper Award）的研究团队——来自香港科技大学佘东冬教授及博士生姚双捷，介绍他们的研究成果背后的新型工具。在他们的课程中，将会为大家介绍的就是一套能够“化繁为简，应对符号执行的路径爆炸难题”的新型符号执行系统 Empc 以及相关的使用。

符号执行技术（Symbolic Execution）作为程序分析（尤其是程序安全分析）中最为重要的核心技术之一，多年来一直受困于一些实用性问题，其中一个难以解决的问题就是所谓的路径爆炸（Path Explosion）。在符号执行中，程序的每一个分支条件都会产生新的路径。当程序规模变大时，这些路径的数量会呈指数增长（路径爆炸），导致计算资源消耗过大，甚至无法完成分析。

下面的图中展示了一个简单的例子，图中的程序有 3 个分支条件，那么理论上最多会出现 6 条不同的执行路径。而在更复杂的程序中，由于分支数目更多，路径数目指数级增加，轻松突破数百万也不是梦！

海量的执行路径数目规模不仅会让符号执行的分析时间剧增，还会让内存资源消耗殆尽。因此，对于现实中的代码，我们其实并不能很好地应用符号执行去进行大规模分析。为了解决这个问题，佘东冬教授研究团队提出了一种全新的路径优先级技术，称为 Empc（Effective Path Prioritization with Path Cover）。其核心理念是并非所有路径都需要符号化求解。下面的图例是 Empc 的核心创新点之一的最小路径覆盖（MPC）：与传统方法需要分析指数级路径不同，Empc 在符号执行过程中只需分析一个小子集，通过利用图论中的最小路径覆盖算法，只选择少量的路径，Empc 就能够覆盖程序中所有的代码区域。换句话说，Empc 用最少的路径覆盖了最多代码。

除此之外，Empc 还有其他一些创意，包括使用多样化路径选择，为了避免单一路径集的局限性，计算多个最小路径覆盖集（MPCs），以确保路径选择的多样性；使用动态路径调整，如果某条路径在运行时被证明是不可行的，Empc 能够动态调整，选择新的路径继续执行。

这么好的工具，当然不能错过，我们暑期学校的课程中会给大家带来关于 Empc 的课程，你想知道 Empc 的效果如何？先看看之前的实验数据：