Yosegine: NaaSを含むネットワークのパケット処理仕様に基づくDesign-Plane Verification

Yosegine: NaaSを含むネットワークの パケット処理仕様に基づく Design-Plane Verification 京都大学 森脇 遼太，岡部 寿男，小谷 大祐

ネットワークを人手のみで安定運用するのは難しい ネットワークは全体で整合性を保った設計・構築が必要 ⚫ 一貫したVLANの設定、正確なパケットのフィルタリングなど ⚫ 1箇所のミスがネットワーク全体の障害につながる可能性 ネットワークが正しい状態であることを人間だけで保証するのは難しい ⚫ 複雑なネットワークの全体の状態を正確に把握し続けるのは難しい ⚫ 分業している場合はチーム間での認識を合わせた連携が必要 システムとしてミスを防ぎセーフティネットとなる技術が必要 2 /23

Enterprise Networkの構成は複雑 複数拠点の接続にNetwork as a Service(NaaS)などが使われる JANOG57 ネットワーク構成図 外部サービスであるOCXなどからは 内部の設定・転送情報を取得できない 様々な種類のネットワークが混在し複雑 3 /23

Network Verification ネットワークの設計や設定、状態が意図した性質を満たすかどうかを 形式手法で検証し、管理者を支援する技術 Data-Plane Verification (HeaderSpaceAnalysis(HSA), SymNet, Katraなど) ⚫ FIBなどの転送情報を収集し、各機器のパケット処理をモデル化 ⚫ 転送状態のスナップショットが意図通りの性質を満たすか確認 Control-Plane Verification (Batfish, Minesweeperなど) ⚫ コンフィグとトポロジから、各機器が持つことになる転送情報を推論 ⚫ コンフィグから意図した転送状態を作ることができるかを検証 対象のネットワークから様々な情報を取得できることが前提 4 /23

NaaSを含む構成における課題 内部情報を取得できない区間についての入力を用意できず，全体の検証が難しい 区間をまたいだ不整合によるトラブルは検出できない 5 /23

従来のNetwork Verificationでは検証できない例 ⚫ クラウド側は会場の10.57.0.0/16からの通信のみ想定 ⚫ 会場側ではネットワーク機器が192.168.157.0/24を使う ネットワーク機器のDNS通信が破棄され，名前解決ができない 各ネットワークの設計の不整合が全体のトラブルとして現れる 6 /23

提案： 全体の設計上の整合性を確認 各区間のネットワークの仕様を入力として全体の設計上の 整合性を確認するDesign-Plane Verificationを提案 管理者はネットワークを構築する前に，各区間についての振る舞いを設計 7 /23

提案手法と既存手法を組み合わせた検証 ⚫ ネットワーク全体の設計上の整合性はDesign-Plane Verificationで検証 ⚫ 自ら管理する区間の実装の正しさは従来の手法で検証 外部サービスは記述した仕様どおりに提供者が構築しているものと仮定する 8 /23

本研究の貢献 課題 NaaSなど内部情報を取得できない区間を含むネットワークでは 従来のNetwork Verificationでの全体の検証が難しい ⚫ Design-Plane Verificationを提案 ⚫ 具体的なDesign-Plane VerificationシステムYosegineを提案 ⚫ JANOG57 イベントネットワークをYosegineを用いて検証できることを確認 NaaSを含むネットワークでも，設計上の整合性を検証可能に 9 /23

Design-Plane Verificationの入力・出力 入力 ① 区間の集合とその接続関係 (例) 会場はNaaSと2本のリンクで接続している ② 各区間に対し管理者が期待する仕様 （例） クラウドは10.57.0．0/16以外からのパケットを破棄する ③ ネットワーク全体が満たすべき性質 (例) 会場のネットワーク機器はクラウドのDNSサーバーに到達できる 区間： 検証を行う管理者が利用可能な情報の粒度などによって定める ネットワークの単位 出力 各区間の仕様を組み合わせたとき， ネットワーク全体が設計上で意図した性質を満たすかどうか 10 /23

Yosegine: Design-Plane Verificationシステム ⚫ 検証エンジンとしてシンボリック実行でネットワークを検証するSymNetを使用 ⚫ 各区間の仕様から，各区間の振る舞いを表すモデルを生成 ⚫ 生成したモデルをSymNetで解析し，指定した性質を検証 11 /23

SymNetの処理 概要 ⚫ パケットの各ヘッダフィールドを変数として表現 ⚫ 各経路を通るパケットについての条件をシンボリック実行で導出 ⚫ 機器は経路表やフィルタリング設定を元にモデル化 12 /23

Design-Plane Verification向けの区間仕様 本来のSymNetは区間を表すにはモデルの粒度が細かい ⚫各機器が行う処理のモデルを入力から作り，組み合わせて全体をモデル化する 転送情報などの入力 処理のモデル化 機器のモデル 区間のモデル Yosegineは管理者が期待する各区間の入出力関係を入力としモデル化 ⚫ HSAのパケット転送を関数として捉える考え方を応用 ⚫ 管理者が期待する振る舞いとして，あるポートから入力されたパケットについて， どうヘッダを変換し，出力するか， あるいは破棄するかを記述 13 /23

説明に用いるネットワーク例の構成 ⚫ 会場ネットワークとクラウドをNaaSであるOCXで接続 ⚫ 会場とOCXは2本のリンクで接続する冗長構成 会場のネットワーク機器からクラウドのDNSサーバーへの到達性を検証する 14 /23

区間とその接続関係の記述 networks: - id: congre interfaces: - id: clients_guest - id: network_devices - id: uplink_01 - id: uplink_02 コングレには 4つのポート - id: ocx interfaces: - id: congre_01 ⋮ links: - endpoints: - { network: congre, interface: uplink_01 } - { network: ocx, interface: congre_01 } ⋮ リンクは2つの端点を指定 15 /23

区間仕様をパケット処理規則として記述 入力ポート，ヘッダ条件，ヘッダ変換，出力ポート を記述 policies: ネットワーク機器から入力されたパケットを対象 - from: network_devices steps: 宛先がゲストのパケットは破棄 - match: ip_dst: prefix-guest actions: - drop: true - match: ip_dst: prefix-cloud actions: - vlan: ocx-local - forward: [uplink_01, uplink_02] 全ての出力先候補を列挙 16 /23

ネットワーク全体が満たすべき性質の記述 - from: 入力元・対象パケット network: congre interface: network_devices packet: ip_src: congre-network-devices ip_dst: prefix-cloud-dns ip_protocol: udp 機器が持つIPアドレス群 dst_port: 53 192.168.157.0/24を含む to: network: cloud 到達先 interface: dns expect: reachable 全パケットが到達可能 via: - network: congre interface: uplink_01 uplink_01経由のパスについて検証 コングレ会場 ネットワーク機器 uplink_01 クラウド DNSサーバー 17 /23

検証の実行と結果の判定 検証する性質: コングレ会場の機器がDNSサーバーに到達可能 対象パケットは全て到達可能であるべきだが， 192.168.157.0/24を送信元とするパケットは到達できない 検証結果: 違反 18 /23

検証に失敗 到達できなかったパケットの情報 19 /23

JANOG57 イベントネットワークのモデル化 ⚫ ルーター13台，スイッチ28台，AP80台 + OCX + クラウド のネットワーク ⚫ 2000台程度のクライアントを収容 ⚫ パケット処理仕様: 合計で約1200行，満たすべき性質: 約2000行 ⚫ 入力の記述にはCoding Agentを使用 （Claude + Codex） 20 /23

JANOG57 イベントネットワークの検証 ⚫ インターネットへの到達性 → 到達可能 ゲスト端末・管理者端末からインターネットに到達できること ⚫ DNSへの到達性 → 到達可能 各端末・ネットワーク機器から利用するDNSサーバーに到達できること ⚫ ゲストネットワークの隔離性 → 隔離性を満たす ゲスト端末から管理者端末・ネットワーク機器への通信が遮断されること 実際のネットワークの仕様を記述し，検証できることを確認した 21 /23

考察: 今後の課題 仕様や満たすべき性質の記述の負担 ⚫ 生成AIは記述の負担を軽減するが，正確な記述は難しい ⚫ より正確な仕様の記述・確認を支援する仕組みが必要 スケーラビリティの評価 ⚫ ネットワークの規模による処理時間・メモリ使用量の評価 ルーティング設計に関するDesign-Plane Verification ⚫ BGPなどのルーティング設計の検証はYosegineの対象外 ⚫ ルーティングに関する設計上の整合性を検証する別の仕組みが必要 22 /23

まとめ 課題 NaaSなど内部情報を取得できない区間を含むネットワークでは 従来のNetwork Verificationでの全体の検証が難しい ⚫ Design-Plane Verificationを提案 各区間の仕様を入力とし，ネットワーク全体の設計上の整合性を検証 ⚫ 具体的なシステムYosegineを提案 各区間に期待する入出力の振る舞いをパケット処理仕様として記述 ⚫ NaaSが使われたJANOG57 イベントネットワークで検証可能なことを確認 仕様の記述の支援・スケーラビリティの評価は今後の課題 23 /23

Appendix 24

Yosegineによる区間仕様からモデルへの変換 仕様の記述をもとに処理モジュールを組み合わせてモデル化 25 /23

Coding Agentを用いた形式的表現の記述 仕様・満たすべき性質の記述にはCoding Agentを使用 ⚫使用したサービス: Claude Code (Team) ＆ Codex (Plus) 自然言語で指示し，Coding Agentで形式的な表現に変換 ① 自然言語でCoding Agentに指示し，生成させる ② 生成物を確認用のwebUIで確認し，意図と異なる部分について修正指示 確認の負担が増え完全な検証は難しいが， 導入する負担は軽減 ⚫ 仕様記述の誤りは検証結果には影響するが，ネットワーク障害は起こさない ⚫ 正しいことの保証は難しくても，ミスを検出する上では有用な検証 26 /23

Prefix定義と中身が分離していると照らし合わせるのが 大変なので一緒に表示 実装上の工夫: yamlの可視化 27 /23

Batfish(pybatfish)での満たすべき性質の記述 TestCase( id="congre_guest_dns-c_tcp53", start_location="@enter(RT-C-01[lan4/1])", src_ips="10.57.0.0/18", dst_ips="10.57.244.8/32", protocol="TCP", dst_ports="53", expected="reachable", ) 28 /23

SymNetの実装に対する変更点 • 一部SEFLモデルの拡張(アドレス範囲の記述を可能に，など) • Header Fieldの値をコピーする時に条件もコピーするように修正 • ルーティングループ検出の実装 • 探索順を幅優先→深さ優先に • 探索が終了したパスはファイルに出力しメモリから解放 • Z3Solverをプロセス全体で1個だけ使うように • IPアドレスと符号付きIntの対応の実装 29 /23