HarnessLLM: Rust Verification Harness Generation with Large Language Models
HarnessLLM 是一个利用大语言模型从现有测试套件中生成并迭代优化 Rust 验证 harness 的自动化框架，成功检测出真实世界的内存安全漏洞，且其精度和效率显著高于以往的方法。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，计算机编程的世界就像一座由代码构建的、繁忙且规模宏大的城市。在这座城市中，Rust 语言以其极其严苛的建筑师形象而闻名。它拥有内置的安全规则，能够防止建筑物坍塌或道路消失，确保城市运行过程中不会发生自我碰撞或崩溃。然而，即使是在这座规划精良的城市中，也存在着“不安全区域”——在这些特殊区域，严格的规则可以被暂时解除，以执行一些强大的操作。如果建筑师不够小心，或者交通灯出现故障，整个城市都可能遭受灾难性的失败，例如内存泄漏或突然的恐慌（panic）。为了保持城市的安全，工程师们使用一种叫做“形式化验证”的方法，这就像是运行一个超级严格的模拟过程，以证明无论发生什么情况，建筑物都不会倒塌。但问题在于，为了运行这个模拟，你首先需要构建一个“测试夹具”（hress）。把夹具想象成一条测试赛道或一个训练假人。你必须手动构建这条赛道，告诉模拟器哪些车要行驶、行驶速度多快，以及要抛出哪些障碍物。手动完成这些工作既缓慢、枯燥，又容易出错，尤其是当城市规模巨大且复杂时。
于是，一群研究人员决定尝试一种不同的方法：他们请求一个被称为“大语言模型”（LLM）的超智能 AI 来为他们构建这些测试赛道。这些 AI 就像数字天才，它们阅读过几乎所有的书籍和代码片段，这使得它们非常擅长理解指令并编写代码。但出现了一个问题：当研究人员第一次要求 AI 构建这些测试赛道时，AI 感到很困惑。它有时会凭空捏造不存在的部件，或者搞错操作顺序，或者无法创建那些真正用于测试城市安全性的复杂、随机场景。AI 擅长写代码，但不擅长遵循安全测试所需的特定、严苛的规则。
这就是论文《HarnessLLM》所介绍的内容。作者 Minghua Wang、Yuwei Liu 和 Lin Huang 并没有只是简单地对 AI 说“去建造一条测试赛道”。相反，他们构建了一个巧妙的、循序渐进的工作流，这个工作流充当了 AI 的项目经理。他们意识到 Rust 代码库本身就拥有一座宝藏：现有的由人类开发者编写的测试用例。这些测试就像是蓝图，展示了代码应该如何被使用。HarnessLLM 首先通过观察这些现有的测试，来寻找特定的“调用场景”——即代码投入使用的确切时刻。随后，它将这些时刻隔离出来，并将其转化为一份干净、简单的配方供 AI 使用。
真正的魔力发生在 AI 需要创建“非确定性”参数时。用通俗的话说，这意味着 AI 必须发明随机的输入来冲击代码，以观察是否会使其崩溃。如果代码预期的是一个简单的数字，AI 可以很容易地猜出一个随机数。但如果代码预期的是一个复杂的、具有许多活动部件的自定义对象，AI 往往会迷失方向。为了解决这个问题，HarnessLLM 构建了一个“依赖图”（dependency graph）。想象一下，这是一张显示拼图每一块是如何相互连接的地图。随后，系统会给 AI 一个“思维链”（Chain-of-Thought）指令，这就像是一张循序渐进的食谱卡。它告诉 AI：“首先，建造小砖块。然后，利用这块砖建造墙壁。最后，利用这面墙建造房子。”这防止了 AI 在打好地基之前就试图建造屋顶。
此外，该系统还内置了一个“事实检查器”。当 AI 编写代码时，代码会被编译（转化为计算机可以运行的形式）。如果计算机发现错误，系统不会仅仅说“修复它”，而是会明确告知 AI：“你虚构了一个不存在的类型，”或者“你修改了原本已经正确的代码部分。”这阻止了 AI 产生幻觉式的虚假解决方案，并迫使它只专注于实际存在的错误。
研究人员在 9 个真实的 Rust 库（这些库就像是城市的不同区域）上测试了这个系统。他们从 494 个现有的测试用例开始，要求 HarnessLLM 将它们转化为验证夹具。结果令人印象深刻。该系统成功提取了 294 个独特的调用场景，准确率达到了 94.66%。随后，它为这些场景中的每一个都生成了可运行的夹具，实现了 100% 的成功率。平均而言，生成每个夹具仅需约 145 秒。相比之下，一个名为 Autoharness 的现有工具只能处理大约 41% 的相同场景，主要是因为它无法处理像 HarnessLLM 那样复杂的自定义类型。
或许最重要的一点是，这不仅仅是一项理论上的练习。当研究人员将生成的夹具应用于代码时，他们发现了 6 个真实的内存安全漏洞（memory safety bugs）。其中 5 个漏洞已被开发者修复，另 1 个正在审核中。这证明了该工具不仅能生成漂亮的漂亮代码，它实际上还能发现可能导致现实问题的危险缺陷。该论文表明，通过将现有的测试套件知识与 AI 的创造力相结合，并在严格的规则和反馈循环引导下，我们可以实现软件安全性验证这一繁琐且困难的任务自动化，从而让我们的数字城市变得更加安全。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。