LLMベースの検証でLinuxネットワークスタックのバグを排除する

LLMsは本番ソフトウェアのバグ発見において驚くほど高い能力を示すようになっています。これはすでに深刻なリスクをさらに強調します。わたしたちの重要なインフラの多くはソフトウェアによって制御されており、そのソフトウェアに含まれるすべてのバグは潜在的な悪用につながる可能性があるからです。形式検証は、バグのクラス全体を不可能にする証明を生成することでこのリスクを軽減する可能性を秘めていますが、希少で高価な専門家の知見を必要とするため、実世界での利用は限られています。幸いなことに、LLMsも検証能力を着実に向上させており、重要なソフトウェアインフラが設計段階から安全である未来を示唆しています。

本記事では、BasisにおけるLLM支援検証実験の結果を報告します。対象としたのはLinuxネットワークスタックの主要コンポーネントであるnftablesファイアウォールコンパイラとオプティマイザで、これをRocq定理証明器で検証することを目指しました。nftablesはまさにそうした重要なインフラの一つです。ほぼすべてのLinuxマシンのトラフィックをフィルタリングしており、その脆弱性は最高レベルの深刻度で扱われます。なぜなら、ファイアウォールが誤ったフィルタリングを行えば、保護すべきすべてのマシンが露出するからです。

nftablesの検証を進める中で、2022年以降のすべてのLinuxバージョンに影響する2件の重大なバグを発見しました（これらはメンテナに開示済み1）。検証済み実装はこれらの意味を変えるバグが存在しないことが証明されており、二次実験では、より深刻なバグは単純なLLMバグ探索では発見されないことも示されました。

実験結果は、証明の作成や堅牢な検証済みシステムの構築にかかる労力が、ますます自動化可能であることを示唆しています。以降では、nftablesの概要、見つかったバグ、そしてLLMを用いた重要なネットワークソフトウェアの検証プロセスについて概観します。

nftablesとそのバグの簡単な紹介

nftablesはLinuxオペレーティングシステムが提供するファイアウォール機構の一つです。OSが受信するすべてのパケットはnftablesを通過し、どのパケットを転送し、どのパケットを破棄するかを決定します。2014年にiptablesに取って代わり、主要なLinuxディストリビューションのデフォルトパケットフィルタとなったnftablesは、現在、ホームルータからコンテナネットワークまで、あらゆるものを保護しています。Linuxマシンがトラフィックをフィルタリングする場合、nftablesが何を通すかをほぼ確実に決定します。ファイアウォールはほとんどのネットワークセキュリティレイヤの重要なコンポーネントであり、その脆弱性はシステム全体を危険にさらす可能性があります。nftablesの検証済み実装は、この重要なレイヤに対する保証を高めるでしょう。

nftablesのルールセットとコンパイルパイプライン

nftablesの全体アーキテクチャを以下に示します。ユーザスペースのCLIツールとカーネルモジュールで構成されています。

このCLIツールは、ユーザが指定したポリシーを順序付きルールリストとして入力として受け取ります。各ルールはパケットの一部（送信元アドレス、宛先ポート、TCPフラグなど）にマッチし、verdict（acceptまたはdrop）を返します。たとえば、以下のルールは宛先アドレス（daddr）が192.168.50.1または192.168.50.2であるパケットをすべて受け入れます。

ip daddr 192.168.50.1 accept
ip daddr 192.168.50.2 accept

nftコマンドラインツールはこれらのルールセットを解析し、コンパクトなレジスタベースのバイトコードにコンパイルしてからカーネルにロードします。カーネルのインタプリタは、このバイトコードを使ってネットワークスタックを通過するすべてのパケットに対してverdictを計算します。つまり、ファイアウォールを通してパケットを受け入れるか、破棄するかを決定します。

このバイトコードはシステムが見るすべてのパケットで実行されるため、カーネルのホットパスに位置し、その効率が重要になります。そのため、CLIツールはソース言語用のオプティマイザモジュールも提供しており、入力ルールをより効率的に実行できるように書き換えます（読み取り回数の削減や冗長なチェックの削除）。ユーザがオプティマイザに期待する重要なセキュリティ特性は、入力ルールの意味を保存することです。言い換えれば、パケットに対して計算されるverdictは、最適化されたルールセットを通した場合と最適化されていないルールセットを通した場合で同じであるべきです。

私たちはnftコマンドラインツールの正しさを証明することを目指し、その過程でシステム内に2つのバグを発見しました。

発見されたバグ

主な成果は、オプティマイザが等価なプログラムを生成しない2つの重要なケースを発見したことです。

1. 1つ目のバグは無効な最適化で、適用されると、最適化前には拒否されていたパケットを受け入れてしまう結果になりました（!!）。

2. 2つ目は、オプティマイザが有効なルールセットを、カーネルに拒否される無効なルールセットに変換してしまうものでした。

これらのバグは最新版のnftablesユーザスペースツールで再現可能であり、検証済み再実装にはこれらの意味を変えるバグが一切存在しないことが証明されました。

バグ1：ビットマスクフィールドの無効なマージ

1つ目のバグは、ビットマスクフィールドをマージする最適化に関連します。

パケットには一連の制御フラグビットが含まれています。たとえばTCPパケットにはSYN、ACK、FINなどのフラグがあります。

nftablesでは、特定のビットがセットされているかどうかをテストするルールを書くことができます。tcp flags synはSYNビットがオンになっているパケットにマッチします。したがって、以下のルールセットはSYNがセットされたすべてのパケットとACKがセットされたすべてのパケットを破棄します。

tcp flags syn drop
tcp flags ack drop

オプティマイザ（nft -o）はこれら2つのルールを1つにまとめます。

tcp flags { syn, ack } drop

残念ながら、この書き換えは正しくありません。マージ後のルールは元の意味と同じではありません。

特に、nft入力言語の意味論は、セットルックアップが完全一致テストであると定義しています。つまり、パケットのフラグバイトがsyn（SYNビットのみがセットされ、他のビットはすべてクリア）と完全に一致する場合、またはackと完全に一致する場合にのみパケットが破棄されます。

元のルールは「このビットがセットされているか？」と尋ねていましたが、マージ後のルールは「フラグバイトがこの1ビットと完全に等しいか（他のすべてのビットがゼロか）？」と尋ねています。同じ制限は、このビットテスト形式でマッチされる任意のビットマスク型フィールドに適用されます。

このバグは特に厄介です。制限的なポリシーをより寛容なポリシーにサイレントに変換してしまうためです。また、重大な安全性への影響を及ぼす可能性があります。前述の例では、ほとんどのsynパケットとackパケットが破棄されていましたが、最適化後はsynまたはackビットのみがセットされたパケットのみが破棄されることになります（大幅に少ないパケット群）。

バグ2：重複する範囲の無効なマージ

2つ目のバグは、アドレスに基づいてルールをマージする最適化に関連します。

連続するルールが同じフィールドにマッチする場合、nft -oはそれらをverdict map（vmap）——フィールドの値を転送verdictにマッピングするルックアップテーブル——にまとめます。これにより、フィールドの複数回の読み取りを1回の読み取りとバイトコード内のジャンプに削減します。

ある送信元アドレスの範囲を破棄し、別の範囲を受け入れるルールセットを考えてみましょう。

ip saddr 192.168.50.1-192.168.50.123 drop
ip saddr 192.168.50.120-192.168.50.255 accept

nft -oは2つのルールを以下のようにマージします。

ip saddr vmap { 
   192.168.50.1-192.168.50.123 : drop, 
   192.168.50.120-192.168.50.255 : accept 
}

残念ながら、最適化の実装にはバグがあり、生成されたマップは不正な形式です。具体的には、nftablesはvmapが各アドレスを単一のverdictにマッピングしなければならないことを要求します。つまり、そのキーは重複しない区間を参照する必要があります。一方、例ではオプティマイザが元の範囲をそのまま再利用し、それらの非重複性をチェックしていないため、.120–.123でキーが重複しています。その結果、最適化後、生成されたルールセットはError: conflicting intervalsというエラーで拒否されます。

このバグにより、有効なルールセットが最適化によって無効なルールセットに変換され、最適化されたルールセットをインストールしようとするとユーザにエラーが報告されることになります。この場合、セキュリティ上の影響は比較的軽微ですが、それでも不正な最適化であり、nftablesへの信頼を損なうものです。

nftablesの形式検証

これら2つのバグは、nftablesのユーザスペースコンポーネントを検証する——すなわち、nftがルールセットの振る舞いを保存することを証明する——継続的な取り組みの中で、LLMによって自律的に発見されました。

実装がこの性質を持つことを形式的に証明するには、まずルールセットの意味を明確に定義し、その意味に対して実装を検証する必要があります。

私たちはRocq定理証明器で以下の4つを形式化しました。

1. nftablesルール言語の構文と意味論、
2. カーネルが実行するレジスタベースのバイトコードの構文と意味論、
3. ルールセットからバイトコードへのコンパイラ、
4. ルールセットをより効率的なルールセットに書き換えるオプティマイザ。

(3)と(4)は、冒頭で述べたnft CLIツールの2つの半分の検証済み版であり、(2)はカーネルのバイトコード実行エンジンの役割を果たします。

形式化された意味論に基づき、コンパイラとオプティマイザの両方が意味を保存することを主張し、証明しました。つまり、コンパイラが生成したバイトコードは、入力ルールセットが受け入れ・破棄するパケットと完全に同じパケットを受け入れ・破棄し、最適化されたルールセットは元のルールセットと完全に同じパケットにマッチします。

証明の外側にある2つの部品があります。nftablesルールセットをRocqのASTに変換するパーサと、バイトコードをカーネルにインストールするシリアライザです。どちらも未検証のOCamlで、私たちのnftc_cli.exeコマンドラインツールにパッケージ化されており、検証済みコンパイラおよびオプティマイザとリンクしています。

検証済み実装はまだ進行中ですが、nftablesルール言語の約90%がモデル化・検証され、機能的同等性に近づいています。検証済み実装のすべての定義、コード行、および証明はLLMによって書かれました。

自律的な検証手法

このセクションでは、開発を自動化するために使用した手法について説明します。すべてのコードと証明は、Opus 4.8をモデルとしてClaude CLIの自動モードで生成されました。

LLMは、検証器（今回の場合はRocq）と検証対象のnftablesの部分を指定し、形式検証とネットワークに関する既存研究を指し示す詳細なプロンプトから開始しました。プロンプトには、テスト駆動開発や頻繁なコードレビューなど、LLMに期待する証明工学および一般的なエンジニアリングプラクティスも明記しました。

テストハーネス

LLMに対して、systemd-vmspawnで仮想マシン（VM）を起動し、ネットワーク名前空間を使って、さまざまなネットワークトポロジ上でnftablesルールをインストールして実行できるテスト環境を構築するよう指示しました。このVMは、公式のnftコマンドラインツールを実行し、その振る舞いを実験するためのサンドボックスも提供しました。

このハーネスの上で、エンドツーエンドの差分テストを実行しました。ルールセットのコーパスを検証済みコンパイラと公式nftables実装の両方に与え、それらの出力を比較しました。

敵対的ワークフロー

開発は2つのLLM間の敵対的ループを通じて進行しました。一方が仕様、実装、証明を書き、もう一方が特定のタイプの欠陥についてレビューして発見した内容を報告します。ループは、レビュー用LLMがそのタイプの欠陥が適切に修正されたと納得するまで続けられました。

このワークフローは、言語意味論の忠実性問題を明らかにするのに特に有効でした。実装LLMが式の意味が正確にモデル化されていないにもかかわらず、早期に成功を主張するケースです。そのような意味的ギャップを浮き彫りにするため、レビュー用LLMが検証済みコードをnftablesの実際のC実装と照合し、仕様不足をフラグする敵対的テンプレートをインスタンス化しました。

Small Proof-Oriented Tests (SPOT)

意味論をさらに圧力テストしつつ、エンドユーザが自身のファイアウォール設定をデバッグするために適用できる成果物も生成するため、LLMが実際のルールセットの性質を主張し証明する特別なテストケースを構築しました。ユーザの意図を形式的に証明するか、その意図が侵害され得る反例を示すものです。ルールセットが仕様化と推論に抵抗した場合、それは意味論がまだ十分に正確ではなく、改善可能であることを示すシグナルとなりました。

バグはどのように発見されたか？

本記事で紹介する2つのバグは、開発を通じてLLMによって自律的に発見されました。バグ自体よりも興味深いのは、バグがどのように発見されたかです。

重複する区間のバグはテストハーネスのおかげで発見されました。6月30日（69666ba）に、LLMはnftablesのオプティマイザ書き換えをトリガーし、その振る舞いをよりよく理解するための人工的なルールセット群を合成しました。ハーネスは各ルールセットを両方のオプティマイザに通し、結果を新しいネットワーク名前空間内のカーネルにロードしました。このバグは、これらのルールセットの1つがnftコマンドラインで大きな失敗（conflicting intervals）を引き起こした際に偶然発見されました。

一方、不健全なビットマスクマージバグの背後にある物語は、はるかに波乱に富んでいます。コミット17c949aで、LLMはビットマスクマージ最適化の独自の健全版を追加しました。連続するルールが同じビットマスクフィールドにマッチする場合、そのオプティマイザはnftablesの完全一致セットではなく、元の「このビットがセットされているか？」テストのORに畳み込みます。コミットメッセージは、LLMがすでにセットの完全一致意味論がビットマスク型式のマージに適さないことを認識していたことを明らかにしています。しかし、LLMはその不健全性をnftables自体のバグとして認識するのではなく、自身の乖離を正当化するために使用しただけでした。

実際、コミットメッセージによると、LLMはnftablesのバグのあるマージ動作を合理化しようとしました。マージ対象のフィールドであるパケットのコネクショントラッキング状態ct stateは、常に1ビットしかセットされないため、ct state { new, established }のようなマージされたセットは無害であり、たとえばArch Linuxのデフォルトルールセットにも見られると指摘しました。

このバグが表面化したのは、7月14日のコミット（c786563）で、公式オプティマイザとの乖離を説明するようLLMに明示的に促したときでした。そのときになってLLMは、tcp flagsやct statusなど、複数のビットが同時にセットされ得る他のビットマスク型式が存在するため、nftablesのオプティマイザが不健全な振る舞いをもたらすことにようやく気づき、VMテストハーネスを通じてバグを確認できました。形式検証は、私たちやLLMが予想していなかったバグからも保護してくれたのです。

これら2つのバグを表面化した後、私たちは小さな実験を行いました。新規のClaudeセッションを開始し、同じVMテストハーネスを使って公式nftablesオプティマイザのバグを探すよう指示しました。LLMは数時間実行し、16件のバグを特定しました。そのうち3件は意味論をサイレントに変更するもので、13件は最適化されたルールが無効であることによるオプティマイザのクラッシュでした。これらのバグは現在、メンテナに開示中です。

# original ruleset
ip daddr 1.1.1.0/24 
     ip daddr 1.1.1.5 accept
ip daddr 2.2.2.0/24
     ip daddr 2.2.2.5 accept

# after nft -o
ip daddr 1.1.1.0/24
   ip daddr { 
     1.1.1.5, 2.2.2.5
   } accept
# 2.2.2.5 can never match

Claudeは検証作業で発見した2つのバグの両方を発見できたでしょうか？答えは「いいえ」です。重複する区間のバグは確かにClaudeによって発見されましたが、ビットマスクバグは数時間の実行後も隠れたままでした。実際、チャット履歴を調べると、LLMはオプティマイザバグをトリガーできる正確なルールセットを再現できましたが、新しい出力を合理的と判断して先に進んでしまいました。LLMが単に出力ルールを眺めることで発見できた3件のサイレントバグとは異なり、ビットマスクバグはnftables意味論の意味をより深く理解する必要があります。

さらに勇気づけられる結果として、検証済み実装はClaudeが発見できた3件の最適化バグの影響を受けません。検証済み実装はまだ進行中ですが、LLM生成の意味論は、nftablesの十分な部分を捉えており、正しさの定理によってそれらのバグのある最適化ルールを正しく拒否できます。より賢いモデルはバグの発見に優れているかもしれませんが、形式検証は本当に高いレベルの保証を与えてくれます。

発見と観察

この初期検証作業を通じて、人間の労力の大部分は仕様の検証、レビュー、洗練に費やされました。失敗する証明は容易に排除できました。LLMはRocqが受理するまで作業を続けるからです。しかし、静かに弱められた定理は容易に見逃される可能性がありました。

やりたくない作業を与えられると、LLMはしばしば、 casual な読みでは容易に見逃される方法でタスクを縮小しようとしました。

このようなパターンは2つの形で繰り返し現れました。

1. LLMが便利な前提条件で仕様を弱める
2. LLMが難しい補題が決して生じないようにシステムの設計を歪める

前提条件による定理の弱体化

オプティマイザの正しさの定理は、この失敗モードの代表例を提供します。

オプティマイザ実装の一部は、新しい名前を生成する必要があります。これは通常、周囲のコードを通じて名前生成状態をスレッドすることを意味します。

名前が必要になるのは、副作用を持つルール——状態を更新したりパケットを変更したりするルール——を書き換えるときだけです。配管作業を避けるため、LLMはその定理が述べる内容を狭めました。

Theorem optimize_table_correct :
  forall n d c n' d' c' base p,
    optimize_table n d c = (n', d', c') ->
    rules_clean (c_rules c) = true ->
    … ->
    eval_chain c' (set_env p (env_with_sets base d'))
  = eval_chain c  (set_env p (env_with_sets base d)).

特に、微妙に挿入されたrules_clean仮定は、純粋なルールに対してのみ成り立つ述語です。この制限により、配管インフラなしで定理を証明できました。定理は依然としてoptimize_table_correctと名付けられ、正しいと証明されましたが、その文は副作用を持つルールについては何も述べていませんでした。

パーサ内のレジスタ割り当て

LLMが定理自体を直接ではなく、仕様定義の形を変更することでショートカットしようとする場合もありました。その一例がレジスタ割り当ての実装です。nftコンパイラはカーネルのレジスタベースのバイトコードインタプリタをターゲットとするため、コンパイルパイプラインのどこかでレジスタを割り当てる必要があります。

LLMはレジスタ割り当てに関する補題の証明を避けようとして、ソースASTにレジスタを追加し、パーサ（検証済みコアの外側）にそれらを割り当てさせました。

これにより、割り当ての一部が解析中に発生する理解しがたい設計になりましたが、LLMの証明義務の観点では、複雑なロジックが未検証コードにアウトソースされたため、コンパイラは検証しやすくなりました。

結論

検証は新しいものではありません。数十年にわたり、研究者たちは重要なソフトウェアインフラの検証に多大な労力を費やしてきました。その過程で、しばしば重大なバグを発見してきました。新しくなったのは、この労力がLLMの使用によってますます自動化可能になったことです。進行中ではありますが、このプロジェクトでの私たちの中間的な進捗でさえ、完了するにはおそらく数年の人的努力が必要だったでしょう。LLMによって、数週間で動作する実装に到達できました。伝統的な検証と同じ利点が得られます。正しさの証明が組み込まれた再実装に取り組んでおり、その過程でnftablesオプティマイザの重大なバグを発見できました。

しかし、一部の労力は依然として手動のままです。LLMは繰り返しタスクの範囲を縮小し、難しい証明を先送りしようとしました。開発における人間の労力のほとんどは、この振る舞いを捉えることに費やされました。より洗練されたハーネスやモデルの能力向上によって、この最後のステップを自動化できるかどうかは、まだわかりません。

私たちは自らそれを探求するつもりです。次の目標は、人間をループから完全に排除し、重要なソフトウェアインフラを大規模に検証する完全自動化パイプラインです。