eBPFヘルパ関数のメモリ引数仕様と実装の整合性検査

• Item type: SIG Technical Reports(1)
• 公開日: 2026-09-17
• タイトル / 言語: ja
• タイトル: eBPFヘルパ関数のメモリ引数仕様と実装の整合性検査
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: OS
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 慶應義塾大学
• 著者所属: 慶應義塾大学
• 著者所属: 慶應義塾大学
• 著者所属: 慶應義塾大学
• 著者所属: 慶應義塾大学
• 著者名: 粟根,颯偲; 鈴木,幹理; 丸山,裕貴; 仲嶋,裕希; 河野,健二
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: eBPFは，ユーザが作成したプログラムをLinuxカーネル内で実行し，カーネル機能の拡張や計測を可能にする機構である．eBPFでは，プログラムの安全性をeBPF verifierによる静的解析で検査する．また，カーネル機能の一部はeBPFヘルパ関数として提供され，verifierは各ヘルパ関数のプロトタイプに記述された引数型および型フラグに基づいて，呼出し時の引数を検証する．しかし，プロトタイプが表す引数仕様とヘルパ関数の実装が一致しなければ，verifierは実装とは異なる前提に基づいて安全性を判断する可能性がある．本研究では，メモリへのポインタを表す引数型ARG_PTR_TO_MEMを対象として，eBPFヘルパ関数のプロトタイプと実装との整合性を静的に検査する手法を提案する．提案手法は，プロトタイプの型フラグおよびサイズ情報が表す引数仕様を複数の検査項目へ分解する．一方，LinuxカーネルのLLVM IRを解析し，対象引数を介した読取りや書込みなどのメモリ操作を関数呼出し先まで追跡する．得られた意味情報を用いて各検査項目を証明または反証し，証明・反証のいずれも行えない場合には未確定とする．適用されるすべての検査項目を証明できた引数のみを整合と判定する．提案手法を静的解析ツールとして実装し，upstream Linuxカーネルの特定の構成に適用した．評価対象となった106引数のうち，14引数を整合，5引数を不整合，87引数を未確定と判定した．また，521件の検査項目のうち，119件を証明し，5件を反証し，397件を未確定とした．
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA12326962
• 書誌情報: 研究報告インターネットと運用技術（IOT）; 巻 2026-IOT-75, 号 10, p. 1-9, 発行日 2026-09-17
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8787
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会