Enhancing Symbolic Execution of Programs for Interprocedural Control Flow Path Feasibility Analysis
本文提出了一种通过自动符号化和循环边界策略增强的定向符号执行方法，旨在高效验证过程间控制流路径的可行性，并证明了在应用于实际项目和静态分析集成时，其召回率和精确度均优于 KLEEF 等现有工具。
原始论文采用 CC BY 4.0 许可（https://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下你是一名试图在一栋巨大的、多层建筑（即计算机程序）中破解犯罪案的侦探。你的任务是检查警察报告中所描述的嫌疑人行踪是否真的具有可行性。
警察报告（即“静态分析器”）写道：“嫌疑人从大厅出发，爬上楼梯，穿过厨房，然后从窗户跳了出去。”
然而，通过查看蓝图，你意识到楼梯并不通向厨房，或者那扇窗户被油漆封死了。警察的报告是一个“虚假警报”——一条在纸面上看起来可行，但在现实中物理上不可能实现的路径。
这篇论文介绍了一种更聪明的方法，让侦探能够检查这些路径，而不会被庞大的建筑规模所压垮。以下是其工作原理，使用简单的类比进行说明：
1. 问题所在：“路径爆炸”
传统的侦探工作试图检查建筑中每一条可能的路径，以观察嫌疑人究竟能去哪里。在一栋拥有数千个房间和无数走廊的巨型建筑中，这需要耗费极长时间。侦探会迷失在海量的可能性中（这个问题被称为“路径爆炸”），并在找到答案之前就耗尽了精力（计算机资源）。
2. 解决方案：“定向”侦探工作
作者提出了一种名为**定向符号执行（Directed Symbolic Execution）**的方法。侦探不再漫无目的地游荡，而是被给予了一张特定路线的地图来进行验证。
- 诀窍： 如果地图显示嫌疑人向左走，侦探就会忽略所有向“右”转的路径。他们只追踪特定的路径，从而剔除了所有的死胡同和无关房间。这使得工作效率大大提高。
3. 处理“未知情况”（自动符号化）
在现实生活中，侦探可能会遇到一个家具还没搬进去的房间，或者一扇没有钥匙的门。在计算机程序中，这些就是“未知值”（例如尚未设置的变量）。
- 旧方法： 侦探会停下来并说：“我无法继续，因为我不知道这个房间里有什么。”
- 新方法： 侦探会说：“好吧，让我们假设这个房间里可以包含任何东西。”他们将未知情况视为一个“神秘盒子”，只要能让路径成立，这个盒子可以填充任何数值。
- 神奇之处： 论文教会了侦探如何自动处理这些神秘盒子，包括：
- 未初始化的变量： 空房间。
- 外部函数： 由邻居（另一个程序）控制的门，侦探无法看到其内部情况。
- 指针： 一张写着“去写有房间号的纸条所指向的房间”的便条。即使房间号会发生变化，侦探也会学习如何跟随这张便条。
4. 无限走廊问题（循环界定）
想象一条环形走廊。如果嫌疑人不停地走，理论上可以永远走下去。
- 问题： 如果侦探试图模拟每一个循环步骤，他们将永远无法完成任务。
- 解决方案： 侦探设定了一条规则：“我最多绕这个圈走 4 圈。”如果走完 4 圈后循环仍在继续，侦探会强制嫌疑人退出循环并继续主路径。
- 为什么有效： 这防止了侦探陷入无尽的死循环，使他们能够完成对特定路径的调查，即使这意味着要跳过一些非常冗长、重复的步骤。
5. 结果：识破谎言
作者在真实世界的软件（如作为计算机基础工具的 GNU Coreutils）和著名的测试集“Juliet”上测试了他们的新型侦探方法。
- 准确性： 他们发现，该方法正确识别了 95.3% 实际上可行的路径。
- 清理虚假警报： 当他们使用这种方法来复核其他安全工具（如 MLH、Infer 和 Clang）的工作时，效果显著。
- 有一个工具（MLH）报告了 666 个虚假警报。新方法过滤掉了所有这些警报，在保留所有真实漏洞的同时，实现了零虚假警报。
- 另一个工具（KLEEF）在尝试检查这些路径时甚至让情况变得更糟，出现了崩溃或几乎丢失了所有真实漏洞。而新方法依然保持强劲且准确。
总结
可以将这篇论文看作是给机器人侦探的一套新指令。与其尝试探索整个宇宙的可能性，这个机器人：
- 专注于它需要检查的特定路径。
- 想象它所不知道的一切可能性（例如空房间或神秘锁具）。
- 强制要求自己在走廊循环过久时停止行走。
其结果是，该系统在区分真正的安全威胁与虚假威胁方面表现得更加出色，且不会感到疲劳或困惑。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。