論文の概要: XRust: Detecting Logical Races in Rust Linux Drivers
- arxiv url: http://arxiv.org/abs/2610.27325v1
- Date: Mon, 19 Oct 2026 21:43:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-21 21:58:47.52166
- Title: XRust: Detecting Logical Races in Rust Linux Drivers
- Title(参考訳): XRust:Rust Linuxドライバの論理的競合を検出する
- Abstract要約: XRustは、手動で指定した不変量なしでLinux Rustドライバの論理競合を検出するテクニックである。
XRustは論理的順序付けに関連する共有状態アクセスを特定し、操作ペアハーネスを自動構築し、シリアルディファレンシャルオラクルを使用して、両方のシリアルオーダーと矛盾した同時実行を検出する。
- 参考スコア(独自算出の注目度): 7.021591046647238
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Rust is increasingly used in Linux to improve memory safety, but its guarantees do not prevent logical races: individually synchronized operations can still interleave in ways that violate higher-level invariants. Detecting such bugs typically requires manually written specifications and carefully controlled execution environments. We present XRust, a technique for detecting logical races in Linux Rust drivers without manually specified invariants. Using Logical Happens-Before (LHB) analysis, XRust identifies shared-state accesses relevant to logical ordering, automatically constructs operation-pair harnesses, and uses serial differential oracles to detect concurrent executions inconsistent with either serial order. XRust also uses lightweight userspace abstractions to execute driver code under reproducible schedules. Applied to Linux 7.3-rc2, XRust identifies 17 shared objects across 102 Rust files from ten drivers, constructs 1,654 executable harnesses, and discovers two previously unknown logical races. The rnull block-driver race has been confirmed by Linux maintainers, with a fix accepted into the Linux block subsystem tree.
- Abstract(参考訳): RustはLinuxでメモリ安全性を改善するためにますます使用されているが、その保証は論理的な競合を防ぐものではない。
このようなバグを検出するには、手動で記述された仕様と注意深く制御された実行環境が必要である。
XRustは、手動で指定した不変量なしでLinux Rustドライバの論理レースを検出する技術である。
Logical Happens-Before (LHB)分析を用いて、XRustは論理的順序付けに関連する共有状態アクセスを特定し、演算ペアハーネスを自動構築し、シリアルディファレンシャルオラクルを使用して、どちらのシリアルオーダーとも一致しない同時実行を検出する。
XRustはまた、再現可能なスケジュール下でドライバコードを実行するために軽量なユーザスペース抽象化を使用している。
Linux 7.3-rc2に適用されたXRustは、102のRustファイルにまたがる17の共有オブジェクトを10のドライバから特定し、1,654の実行可能なハーネスを構築し、これまで知られていなかった2つの論理競合を発見した。
rnullブロックドライバレースがLinuxメンテナによって確認され、Linuxブロックサブシステムツリーに修正が受け入れられた。
関連論文リスト
- AnomalyGen: Enhancing Log-Based Anomaly Detection with Code-Guided Data Augmentation [42.87177529900358]
AnomalyGenは、ラベル付きログシーケンスをソースコードから合成することによってトレーニングデータを増強する新しいフレームワークである。
12のさまざまな異常検出モデルに対するHDFSとZookeeperの評価は、AnomalyGenが一貫してパフォーマンスを改善していることを示している。
論文 参考訳(メタデータ) (2026-04-13T07:24:43Z) - Arch: An AI-Native Hardware Description Language for Register-Transfer Clocked Hardware Design [0.0]
Archはパイプライン、FIFO、アービター、レジスタファイル、バス、時計領域横断のための第一級言語構造を導入している。
中心となる設計選択は、クロックとリセット自体がパラメータ化された型であることである。
Archコンパイラは、決定論的でリントクリーンなIEEE 1800-2017 SystemVerilogを出力する。
論文 参考訳(メタデータ) (2026-04-07T15:12:14Z) - QiMeng-CRUX: Narrowing the Gap between Natural Language and Verilog via Core Refined Understanding eXpression [48.84841760215598]
大規模言語モデル(LLM)はハードウェア記述言語(HDL)生成において有望な能力を示している。
既存のアプローチは、しばしば曖昧で冗長で構造化されていない自由形式の自然言語記述に依存している。
我々は、ハードウェアコード生成を、オープンな自然言語空間からドメイン固有の高度に制約されたターゲット空間への複雑な変換として扱う。
構造化された中間空間であるCore Refined Understanding eXpression (CRUX)を導入し、ユーザの意図の本質的な意味を捉えながら、正確なVerilogコード生成のための式を整理する。
論文 参考訳(メタデータ) (2025-11-25T09:17:32Z) - RustAssure: Differential Symbolic Testing for LLM-Transpiled C-to-Rust Code [2.1413732583497826]
Rustは、ソフトウェアのセキュリティを大幅に改善するメモリセーフなプログラミング言語である。
Cのような安全でないメモリ言語で書かれた既存のものは、Rustの改善された安全性保証を活用するために、まずRustにコンパイルされなければならない。
RustAssureは、Large Language Models(LLM)を使用して既存のCをRustに自動的にトランスパイルするシステムを提供する。
論文 参考訳(メタデータ) (2025-10-08T22:52:34Z) - Securing Mixed Rust with Hardware Capabilities [12.52089113918087]
CapsLockは、マシンコードのレベルで動作し、混合コードの実行時にRustの原則違反を検出するセキュリティ執行機構である。
CapsLockは、最近の機能ベースのハードウェア抽象化に実装できるほどシンプルに保たれている。
論文 参考訳(メタデータ) (2025-07-04T07:12:43Z) - 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) - VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners [6.824327908701066]
Rustはメモリ安全性と低レベルのコントロールを組み合わせたプログラミング言語で、Cライクなパフォーマンスを提供する。
既存の作業はルールベースと大規模言語モデル(LLM)という2つのカテゴリに分類される。
私たちは、正式な正確性を保証する形で、可読性のあるRustトランスパイルを生成するツールであるVERTを紹介します。
論文 参考訳(メタデータ) (2024-04-29T16:45:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。