論文の概要: Verifying the Rust Standard Library
- arxiv url: http://arxiv.org/abs/2606.17374v1
- Date: Tue, 16 Jun 2026 00:11:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-17 17:15:32.181939
- Title: Verifying the Rust Standard Library
- Title（参考訳）: Rust標準ライブラリの検証
- Authors: Byron Cook, Remi Delmas, Zyad Hassan, Bart Jacobs, Ranjit Jhala, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Rebecca Rumbul, Michael Tautschnig, Celina Val, Carolyn Zech,
- Abstract要約: Rustの型システムは、多くのメモリエラーのクラスを防ぐが、標準ライブラリは安全でないコードに大きく依存している。
これは、補完的な検証ツールをRust標準ライブラリからフォークされた検証リポジトリの継続的統合に統合する、オープンでクラウドソースされた取り組みです。
- 参考スコア（独自算出の注目度）: 3.303009078327922
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign's effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.
- Abstract（参考訳）: Rustの型システムは、多くのメモリエラーのクラスを防ぐが、標準ライブラリは、テストを通じて正確性を検証するアンセーフなコードに大きく依存している。
これは、補完的な検証ツールをRust標準ライブラリからフォークされた検証リポジトリの継続的統合に統合する、オープンでクラウドソースされた取り組みです。
キャンペーンの有効性を分析し、未定義の動作のサブセット(例えば、アウト・オブ・バウンドアクセス、ヌルおよびダングリングポインタの参照、未初期化メモリの使用)に対するマシンチェックされた証明の実践的価値を議論し、残りの障害をフォーマル・メソッド・コミュニティのオープン・チャレンジとして枠づける。
関連論文リスト
- Veritas: A Semantically Grounded Agentic Framework for Memory Corruption Vulnerability Detection in Binaries [14.42294978688412]
We present Veritas, a semantically grounded framework for binary memory corruption vulnerability detection。
Veritas は RetDec-lifted LLVM IR に静的スライサ、デュアルビュー LLM 検出器、マルチエージェントバリデータを組み合わせた。
Veritasをモジュールパイプラインとして実装し、実世界のバイナリ脆弱性ケースのキュレートされたベンチマークで評価する。
論文 参考訳（メタデータ） (2026-05-14T17:16:11Z) - Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - 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) - CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。
我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。
最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
論文 参考訳（メタデータ） (2025-04-21T17:33:33Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language [15.164423552903571]
Rustプロジェクトでは、セキュリティ上の脆弱性が報告されている。
これらの脆弱性は、部分的には関数シグネチャの誤った終身アノテーションから生じます。
既存のツールはこれらのバグを検出するのに失敗する。
我々は,新たな静的解析ツールであるYugaを考案し,潜在的なライフタイムアノテーションのバグを検出する。
論文 参考訳（メタデータ） (2023-10-12T17:05:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。