AI 中文总结
研究针对Rust代码内存安全验证开发验证框架难的问题，提出HarnessLLM自动化工作流程，利用大语言模型从测试套件生成框架，经实验评估效果良好，能检测内存安全漏洞，是首个用大语言模型为Rust项目内存安全验证生成框架的工作。
AI 中文摘要
Rust的所有权模型和类型系统提供了强大的内存安全保证，但不安全代码和运行时恐慌仍存在重大风险。形式验证对确保内存安全至关重要，但开发验证框架仍然是一项具有挑战性的手动任务。虽然大语言模型在各种代码分析任务中表现出色，但直接将它们应用于框架生成往往会导致API调用不准确、非确定性数据生成效率低下和虚假修复。本文提出了HarnessLLM，这是一种自动化工作流程，利用大语言模型直接从现有测试套件中为Rust代码生成验证框架。HarnessLLM自动从测试用例中提取调用场景，基于依赖分析生成非确定性参数，并逐步合成框架。然后迭代优化框架，保留关键代码区域，并将虚假类型或函数报告给大语言模型进行修正。在对9个真实世界Rust代码库的评估中，HarnessLLM从494个测试用例中提取了294个调用场景，精度为94.66%，平均每个场景在145秒内生成框架。它优于现有方法Autoharness，后者仅在41%的场景上成功。最后，使用生成的框架检测到6个真实世界的内存安全漏洞，证明了我们方法在验证中的实际效用。据我们所知，这是第一项使用大语言模型为真实世界Rust项目中的内存安全验证生成框架的工作。
英文摘要
Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks. Formal verification is essential to ensure memory safety, but developing verification harnesses remains a challenging and manual task. Although large language models (LLMs) have shown strong performance in various code analysis tasks, directly applying them to harness generation often results in inaccurate API invocations, inefficient nondeterministic data generation, and fabricated fixes. In this paper, we present HarnessLLM, an automated workflow that leverages LLMs to generate verification harnesses for Rust code directly from existing test suites. HarnessLLM automatically extracts calling scenarios from test cases, generates nondeterministic arguments based on dependency analysis, and incrementally synthesizes harnesses. It then iteratively refines the harnesses, preserving critical code regions and reporting fabricated types or functions to LLMs for correction. In our evaluation on 9 real-world Rust codebases, HarnessLLM extracted 294 calling scenarios from 494 test cases with 94.66% precision and generated harnesses for all scenarios in an average of 145 seconds each. It outperformed the existing approach, Autoharness, which succeeded on only 41% of those scenarios. Finally, 6 real-world memory safety bugs were detected using the generated harnesses, demonstrating the practical utility of our approach in verification. To our knowledge, this is the first work to use LLMs for generating harnesses aimed at memory safety verification in real-world Rust projects.
