論文の概要: HarnessLLM: Rust Verification Harness Generation with Large Language Models
- arxiv url: http://arxiv.org/abs/2607.22161v1
- Date: Fri, 24 Jul 2026 10:06:52 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-27 20:58:57.11086
- Title: HarnessLLM: Rust Verification Harness Generation with Large Language Models
- Title（参考訳）: HarnessLLM: 大きな言語モデルでRustを検証するHarness生成
- Authors: Minghua Wang, Yuwei Liu, Lin Huang,
- Abstract要約: Rustのオーナシップモデルと型システムは、強力なメモリ安全保証を提供するが、安全でないコードとランタイムパニックは依然として重大なリスクを伴っている。
メモリ安全性を確保するためには形式的検証が不可欠だが、検証ハーネスの開発は依然として困難な作業である。
私たちは、大規模な言語モデルを活用して、既存のテストスイートから直接Rustコードの検証ハーネスを生成する自動化ワークフローであるHarnessLLMを紹介します。
- 参考スコア（独自算出の注目度）: 8.14069260667009
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract（参考訳）: Rustのオーナシップモデルと型システムは、強力なメモリ安全保証を提供するが、安全でないコードとランタイムパニックは依然として重大なリスクを伴っている。
メモリ安全性を確保するためには形式的検証が不可欠だが、検証ハーネスの開発は依然として困難な作業である。
大規模言語モデル(LLM)は、様々なコード解析タスクにおいて強力なパフォーマンスを示しているが、それらを生成に直接適用すると、不正確なAPI呼び出し、非効率な非決定的データ生成、および修正が生じることが多い。
本稿では、LLMを利用して既存のテストスイートから直接Rustコードの検証ハーネスを生成する自動化ワークフローであるHarnessLLMを提案する。
HarnessLLMは、テストケースからコールシナリオを自動的に抽出し、依存性分析に基づいて非決定論的引数を生成し、インクリメンタルにハーネスを合成する。
その後、ハーネスを反復的に洗練し、重要なコード領域を保持し、修正のためにLLMに偽造されたタイプや関数を報告する。
実世界のRustコードベース9つの評価において、HarnessLLMは94.66%の精度で494のテストケースから294の呼び出しシナリオを抽出し、平均145秒毎にすべてのシナリオに対してハーネスを生成する。
既存のアプローチであるAutoharnessよりも優れており、これらのシナリオはわずか41%に過ぎなかった。
最後に,実世界のメモリ安全性に関する6つのバグを,生成したハーネスを用いて検出し,本手法の有効性を実証した。
私たちの知る限り、現実のRustプロジェクトでメモリ安全性検証を目的としたハーネスを生成するためにLLMを使用するのは、これが初めての作業です。
関連論文リスト
- SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
RLM(Reasoning Language Model)は、プログラミングにおいてますます使われている言語モデルである。
しかし、最先端のRLMでさえ、生成されたコードに重大なセキュリティ脆弱性を頻繁に導入する。
我々は、構造化されたセキュリティ推論を内部化するためのRTMを教える微調整パイプラインであるSecPIを提案する。
論文 参考訳（メタデータ） (2026-04-04T04:29:11Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - HALURust: Exploiting Hallucinations of Large Language Models to Detect Vulnerabilities in Rust [5.539291692976558]
2018年以降、442のRust関連の脆弱性が現実世界のアプリケーションで報告されている。
本稿では,大規模言語モデル(LLM)の幻覚を利用して,現実のRustシナリオの脆弱性を検出する新しいフレームワークであるHALURustを紹介する。
HALURustは、54のアプリケーションにまたがる447の関数と18,691行のコードを含む、81の現実世界の脆弱性のデータセットで評価された。
論文 参考訳（メタデータ） (2025-03-13T18:38:34Z) - Bridging the Safety Gap: A Guardrail Pipeline for Trustworthy LLM Inferences [18.36319991890607]
本稿では,Large Language Model(LLM)推論の安全性と信頼性を高めるために設計されたガードレールパイプラインであるWildflare GuardRailを紹介する。
Wildflare GuardRailは、セーフティインプットを識別し、モデルアウトプットの幻覚を検出するSafety Detectorなど、いくつかのコア機能モジュールを統合している。
軽量なラッパーは、コストのかかるモデルコールなしで、クエリ毎に1.06sのモデル出力で悪意のあるURLに100%の精度で対処できる。
論文 参考訳（メタデータ） (2025-02-12T05:48:57Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。
11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。
最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
論文 参考訳（メタデータ） (2024-07-23T15:31:26Z) - SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
SORRY-Benchは、安全でないユーザ要求を認識し拒否する大規模言語モデル(LLM)能力を評価するためのベンチマークである。
まず、既存の手法では、安全でないトピックの粗い分類を使い、いくつかのきめ細かいトピックを過剰に表現している。
第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。
論文 参考訳（メタデータ） (2024-06-20T17:56:07Z) - LLMs Cannot Reliably Identify and Reason About Security Vulnerabilities (Yet?): A Comprehensive Evaluation, Framework, and Benchmarks [17.522223535347905]
大規模な言語モデル(LLM)は、自動脆弱性修正に使用するために提案されているが、ベンチマークでは、セキュリティ関連のバグが一貫して欠如していることが示されている。
SecLLMHolmesは,LLMがセキュリティ関連のバグを確実に識別し,原因を判断できるかどうか,これまでで最も詳細な調査を行う,完全に自動化された評価フレームワークである。
論文 参考訳（メタデータ） (2023-12-19T20:19:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。