論文の概要: Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust

• arxiv url: http://arxiv.org/abs/2605.25411v1
• Date: Mon, 25 May 2026 04:23:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-26 19:50:19.28322
• Title: Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
• Title（参考訳）: Heimdall: レガシeBPFプログラムからRustへの正式な自動移行
• Authors: Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari, Gang Tan,
• Abstract要約: Extended Berkeley Packet Filter (eBPF) は、Linuxカーネルのネットワーク、可観測性、セキュリティ強化に使用されるカーネル拡張である。 In- kernel eBPF verifiers checks low-level memory safety andtermination on eBPF program, but not not enforce many higher-level source-level properties。 We present Heimdall, a automated pipeline that using large language model to translate legacy libbpf C program to Aya Rust。
• 参考スコア（独自算出の注目度）: 14.478602770508523
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Extended Berkeley Packet Filter (eBPF) programs are kernel extensions used for networking, observability, and security enforcement in the Linux kernel. The in-kernel eBPF verifier checks low-level memory safety and termination on eBPF programs, but it does not enforce many higher-level source-level properties, such as initialization discipline, schema consistency, or error handling. We document six classes of source-level bugs that compile, pass the kernel verifier, and can silently corrupt data, leak previously traced events to userspace, or yield incorrect enforcement outcomes. Among these, we identify previously unreported information leaks in ten open-source eBPF programs whose ring-buffer or stack-resident event records carry fully decodable prior traced events, including user-identifying paths and recurring kernel-text return addresses sufficient to recover the KASLR slide on every event, into userspace. To harden such verifier-accepted buggy programs and support safe migration, we present Heimdall, an automated pipeline that uses large language models to translate legacy libbpf C programs to Aya Rust. Heimdall iteratively repairs compilation and kernel-verifier failures, rejects unsafe escape hatches in Rust-Aya with a static analysis safety engine, and proves per-program equivalence to the original via symbolic execution and Z3-based equivalence checking. Across 102 eBPF programs, Heimdall produces 96 formally proven-equivalent translations (94.1%). Heimdall is the first system to automate memory-safe-language migration of production eBPF programs with per-program formal guarantees that the migration preserves observable behavior.
• Abstract（参考訳）: Extended Berkeley Packet Filter (eBPF) は、Linuxカーネルのネットワーク、可観測性、セキュリティ強化に使用されるカーネル拡張である。 カーネル内のeBPF検証器は、eBPFプログラムの低レベルのメモリ安全性と終了をチェックするが、初期化の規律、スキーマの整合性、エラー処理など、多くの高レベルのソースレベルプロパティを強制しない。 ソースレベルの6つのバグを文書化し、コンパイルし、カーネル検証をパスし、静かにデータを破損させたり、トレースしたイベントをユーザ空間にリークさせたり、不正な強制結果を出したりします。 これらのうち、リングバッファやスタック予約イベントレコードが、ユーザ識別パスやカーネルテキストのリターンアドレスを含む、完全に削除可能なトレースイベントを、すべてのイベント上のKASLRスライドをユーザ空間に復元するのに十分な、完全に削除可能な、10のオープンソースeBPFプログラムにおいて、これまで報告されていない情報漏洩を識別する。 このような検証済みバグ修正プログラムを強化し、安全なマイグレーションをサポートするために、大規模な言語モデルを使用してレガシな libbpf C プログラムを Aya Rust に変換する自動パイプラインであるHeimdall を紹介します。 Heimdallはコンパイルとカーネル検証の失敗を反復的に修復し、静的解析安全エンジンでRust-Ayaの安全でないエスケープハッチを拒絶し、シンボル実行とZ3ベースの等価チェックを通じて、オリジナルのプログラムごとの等価性を証明している。 102のeBPFプログラム全体で、Heimdallは96の正式に証明された等価翻訳(94.1%)を生産している。 Heimdallは、プログラムごとの正式な保証により、プロダクションeBPFプログラムのメモリセーフなマイグレーションを自動化する最初のシステムである。

関連論文リスト

• MemEvoBench: Benchmarking Memory MisEvolution in LLM Agents [78.95081012334116]
  永続メモリを持つ大規模言語モデル(LLM)は、相互作用の継続性とパーソナライゼーションを高めるが、新たな安全性リスクをもたらす。 汚染または偏りのある記憶蓄積は、異常な作用を引き起こす可能性がある。 MemeEvoBenchは、LLMエージェントのメモリ安全性を評価する最初のベンチマークである。
  論文  参考訳（メタデータ） (2026-04-17T07:29:52Z)
• ENCRUST: Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-Rust Translation [5.10072982044534]
  安全なC-to-construct通訳のためのLive Scaffoldのカプセル化置換とエージェントリファインメントについて述べる。 現実世界のCプロジェクトを安全にRustに変換するための2フェーズパイプラインを提示する。 フェーズ1(カプセル化された置換)は、ABIutilラッパーを使用して各関数を2つのコンポーネントに分割する。 フェーズ2(Agentic Refinement)は、機能ごとのスコープを超えた安全でない構成を解決します。
  論文  参考訳（メタデータ） (2026-04-06T08:46:14Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBenchは、新たに発見されたカーネルバグのエージェントをスクラップし、評価するセルフ進化ベンチマークの評価フレームワークである。 kEnvは、カーネルのコンパイル、実行、フィードバックのためのエージェントに依存しないクラッシュ解決環境である。 kEnvを用いて3つの最先端エージェントをベンチマークし、最初の試行で74%のクラッシュを解決したことを示す。
  論文  参考訳（メタデータ） (2026-02-02T19:06:15Z)
• 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)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。 このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
  論文  参考訳（メタデータ） (2025-02-17T12:38:57Z)
• VeriFence: Lightweight and Precise Spectre Defenses for Untrusted Linux Kernel Extensions [0.07696728525672149]
  Linuxの拡張バークレーパケットフィルタ(BPF)は、ユーザが提供するバイトコードをジャストインタイムでコンパイルすることで、ユーザ/カーネルの遷移を避ける。 2018年に公表されたSpectreの脆弱性を緩和するためには、潜在的に危険なプログラムを拒否する防衛措置を実施せざるを得なかった。 We propose VeriFence, an enhancement to the kernel's Spectre Defenses that reduce the number of BPF application program from 54% to zero。
  論文  参考訳（メタデータ） (2024-04-30T12:34:23Z)
• MOAT: Towards Safe BPF Kernel Extension [10.303142268182116]
  LinuxカーネルはBerkeley Packet Filter (BPF) を広く使用し、ユーザが記述したBPFアプリケーションをカーネル空間で実行できるようにする。 最近の攻撃は、BPFプログラムがセキュリティチェックを回避し、カーネルメモリへの不正アクセスを得る可能性があることを示している。 我々は,Intel Memory Protection Keys (MPK) を用いて,潜在的に悪意のあるBPFプログラムを分離するシステムMOATを提案する。
  論文  参考訳（メタデータ） (2023-01-31T05:31:45Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。