# カーネル内VM ## 定義 カーネル内VM(in-kernel virtual machine)とは、OS カーネル内でユーザ提供のプログラムを安全・効率的に実行するための仮想機械実行エンジンである。ユーザ空間が記述したロジックをカーネル空間で走らせることで、システムコールやコピーのオーバーヘッドなしに高頻度のカーネルイベントを処理できる。BPF(1993 年、[[@1993__USENIX__The BSD Packet Filter A New Architecture for User-level Packet Capture]])がパケットフィルタリング用途でこのパターンを確立し、eBPF([[eBPF]])が汎用カーネル拡張機構へ発展させた。 ## 設計上の根本的トレードオフ カーネル内VM は以下のトレードオフを resolve するための装置である。 | 課題 | 内容 | |---|---| | 安全性 | ユーザ提供コードがカーネルをクラッシュさせてはならない | | 性能 | カーネルイベントごとにユーザ空間とのコンテキストスイッチは許容できない | | 柔軟性 | ユーザがフィルタロジック/処理ロジックを動的に変更できなければならない | | 移植性 | 特定の CPU アーキテクチャに縛られてはならない | BPF はこれらを「専用命令セット + 静的解析 verifier + バイトコードインタープリタ(+JIT)」で解いた。 ## 安全性保証の機構 カーネル内VM の安全性は verifier(検証器)が担う。BPF/eBPF の verifier は以下を静的に検査する。 - **終了性**: 無限ループが存在しない(DAG であること) - **メモリ安全性**: 境界外アクセスがない - **レジスタ初期化**: 未初期化レジスタの使用がない - **権限チェック**: 操作に必要な権限が呼び出し元にある verifier が通過したバイトコードのみカーネル内で実行される。この「事前検証 + 制限された実行」モデルは、[[eBPF]] の「AI for eBPF」研究群(Kgent・GPTtrace 等)が LLM 生成 eBPF コードを Z3 や意味検査で囲む際に直接活用されている。 ## BPF からの進化 | 世代 | 技術 | 命令数 | レジスタ | フックポイント | |---|---|---|---|---| | BPF (1993) | パケットフィルタ VM | ~30 | A, X, M[16] | ネットワーク(ソケット) | | Linux cBPF | BPF 移植(kernel 2.x) | 〃 | 〃 | ソケットフィルタ | | Linux eBPF (2014〜) | 汎用カーネル VM | ~80 | r0〜r10 | kprobe / tracepoint / XDP / LSM / sched_ext など多数 | ## 横断的知見 - **BPF verifier は「ユーザ提供コードをカーネルで安全に実行する」という問題の最初の実用解である**: 1993 年の BPF verifier は「ループなし DAG」という単純な安全モデルを採用した。eBPF はこれを「有界ループを許容する形式的検証」へ拡張した。AI/ML コード生成([[@2026__eunomia.dev__eBPF × AI-LLMs - The Convergence of System Observability and AI]])では、LLM が生成した eBPF コードを verifier が自動的に拒否することで安全性が保たれる——生成系を検証器で囲む定石の最初の事例が BPF に遡る。(Source: [[@1993__USENIX__The BSD Packet Filter A New Architecture for User-level Packet Capture]]) ## 未解決の問い - GPU 内カーネル実行(eGPU の PTX 注入、[[@2025__HCDS__eGPU - Extending eBPF Programmability and Observability to GPUs]])は「GPU 内 VM」への拡張とみなせるが、安全性検証はどう行うか。eBPF verifier の GPU 対応がないため、現状では verifier なし実行になるリスクがある。 - eBPF の「有界ループ」許容(kernel 5.3 以降)は verifier の複雑度を大幅に増した。LLM 生成 eBPF コードに対する verifier の承認/拒否率はどの程度か。 ## 関連 - 概念: [[BPF]] / [[eBPF]] / [[パケットフィルタリング]] / [[動的インストルメンテーション]] / [[テレメトリ]] - エンティティ: [[Steven McCanne]] / [[Van Jacobson]] / [[LBNL]] - ソース: [[@1993__USENIX__The BSD Packet Filter A New Architecture for User-level Packet Capture]] / [[@2021__yuuk.io__Linux eBPF Tracing Technology]] ## 出典 - [[@1993__USENIX__The BSD Packet Filter A New Architecture for User-level Packet Capture]](カーネル内 VM の原型。register-based VM + verifier + CFG 評価の設計)