HarnessLLM：使用 大语言模型 生成 Rust 验证Harness

Rust 的所有权模型和类型系统提供了强大的内存安全保证，但不安全的代码和运行时恐慌仍然存在重大风险。形式验证对于确保内存安全至关重要，但开发验证工具仍然是一项具有挑战性的手动任务。尽管大语言模型（LLM）在各种代码分析任务中表现出了强大的性能，但直接将其应用于Harness生成通常会导致API调用不准确、低效的非确定性数据生成和伪造的修复。在本文中，我们介绍了 HarnessLLM，这是一种自动化工作流程，利用 LLM 直接从现有测试套件生成 Rust 代码的验证工具。 HarnessLLM 自动从测试用例中提取调用场景，根据依赖关系分析生成不确定性参数，并逐步综合工具。然后，它迭代地细化工具，保留关键代码区域并向 LLM 报告构造的类型或函数以进行更正。在我们对 9 个真实 Rust 代码库的评估中，HarnessLLM 从 494 个测试用例中以 94.66% 的精度提取了 294 个调用场景，并在平均每个场景 145 秒的时间内为所有场景生成了工具。它的性能优于现有方法 Autoharness，后者仅在其中 41% 的场景中取得了成功。最后，使用生成的工具检测到了 6 个现实世界的内存安全错误，证明了我们的方法在验证中的实用性。据我们所知，这是第一个使用 LLM 生成旨在现实 Rust 项目中内存安全验证的工具的工作。