NDD - ネットワーク検証のための新世代データ構造

に公開

はじめに

Xi'an Jiaotong UniversityとGoogleの研究者による論文「NDD: A Decision Diagram for Network Verification」を読んだメモ。

最近のネットワーク運用者にとって、ネットワーク検証は重要なツールチェーンになっている。大規模サービスプロバイダーの中には、誤設定を検出するためにネットワーク検証ツールを導入しているところもある。多くのネットワーク検証ツールでは、パケットヘッダやルート、障害などのネットワーク状態をコンパクトに表現するためにBDD(Binary Decision Diagram)を使用している。


https://www.usenix.org/system/files/nsdi25-li-zechun.pdf

しかし広く使われているにもかかわらず、BDDはネットワーク検証タスクに最適ではないことが明らかになってきた。この論文では、ネットワーク検証用にカスタマイズされた新しい決定図であるNDD(Network Decision Diagram)を紹介する。NDDは基本的に、BDDに別のレイヤーの決定図を追加したもので、各NDDノードはネットワークのフィールドを表し、各エッジはそのフィールドの値を示すBDDでラベル付けされている。

ネットワーク検証におけるBDDの限界

BDDはネットワーク検証で広く使われているが、以下の3つの側面で理想的ではない点が明らかになっている。

問題点 詳細
メモリ効率の低さ BDDベースのネットワーク検証ツールは多数の冗長なノードを作成する。これらのノードは一部のフィールドで同じサブ構造を共有しているが、他のフィールドでの違いがあるため削減できない。この冗長性は、検証ツールが等価クラス(原子述語、単にアトムとも呼ばれる)を計算するときに増幅され、「アトムの爆発」につながりメモリをオーバーフローさせる。
計算効率の低さ BDDベースのネットワーク検証ツールは、a∧bなどの論理演算によって速度が低下する。BDD演算は再帰的な方法で進行し、各再帰はaとbの単一ビットを検査する。さらに悪いことに、BDDが異なる変数をエンコードしている場合、それらの変数を「整列」するためにより多くの再帰が必要になる。ネットワークは多くの場合、複数のフィールド(5タプルで104ビットなど)に一致するため、再帰は非常に深くなり、非常に遅くなる可能性がある。
ネットワーク検証のサポート不足 BDDライブラリは、アトムの計算やアトムの増分更新、パケット変換処理など、ネットワーク検証の一般的なタスクにほとんどサポートを提供していない。そのため、ネットワーク検証ツールは、これらの一般的なタスクのための独自のアルゴリズムを設計する必要があり、その設計は非常に複雑になる可能性がある。

これらの問題は、BDDがネットワークでは重要な「フィールド」という概念を知らないことに起因している。「フィールド局所性」と呼ばれる特性により、異なるフィールドは直交しており、各フィールドのノード数の掛け合わせになるため、ノード総数が非常に大きくなる。


https://www.usenix.org/system/files/nsdi25-li-zechun.pdf

NDDの基本概念と設計思想

NDDとは何か

NDDの基本的なアイデアは、ネットワーク状態全体を1つの単位として扱うのではなく、一連のフィールドに分割し、論理演算が同じフィールドのBDDに限定され、同じフィールドの冗長なノードが他のフィールドとは完全に独立して削減できるようにすることだ。

BDDの場合、各ノードは単一のビットを表す変数を検査し、高いエッジと低いエッジの2つの後続ノードを持つ。対照的に、NDDでは各ノードはネットワークのフィールド(複数ビット)を表し、複数のエッジを持つことができる。各エッジはBDDでラベル付けされ、そのフィールドの値の範囲を表現する。

これによりNDDはBDDと比較して次のような利点を持つ。

  1. フィールドごとにBDDノードを分離することで冗長性を大幅に削減
  2. 各NDDノードが多くのビットを一度に処理できるため、論理演算がはるかに少ない再帰で済む
  3. 各フィールドに対して別々のアトム集合を計算することで、アトムの数が減少

原子化されたNDD

NDDの特徴的な概念の一つが「原子化されたNDD」(Atomized NDD)だ。これは、各エッジのラベルがBDDからアトムのセットに変換されたNDDを指す。原子化NDDはBDDに対して次のような利点がある。

利点 説明
アトム数の削減 アトムは単一のフィールドに対するものなので、クロスプロダクト効果を回避し、ネットワーク内のアトムの総数を劇的に減らすことができる
透過的な操作 アトム関連のすべての操作はネットワーク検証ツールに対して完全に透過的で、検証ツールはアトムを意識せず、独自のアトム関連アルゴリズムを実装する必要がない
セット操作の簡素化 NDDの論理演算(∧、∨など)をより単純なセット操作(∩、∪など)に置き換えることができる

NDDライブラリの実装詳細

既存のBDDライブラリをネットワーク検証ツール用のNDDライブラリに置き換えることは簡単なタスクではない。最新のBDDライブラリはメモリコストを削減し計算を高速化するために様々な最適化を適用しているからだ。

論文の著者らは、JDDなどの既存のBDDライブラリをベースにしたNDDライブラリを設計・実装した。主な拡張点は以下の通り。

  1. 標準APIの拡張(atomize、updateなどの新機能)
  2. 論理演算、ガベージコレクション、ノードテーブルの設計をNDDに適応
  3. 操作キャッシュなどのBDDの最適化を再利用
  4. falseノードの削除などのNDD固有の最適化を適用

主要API

NDDライブラリのAPIは、BDDライブラリのAPIと非常に似ているが、いくつかの重要な違いがある。

API 説明
createVar(Integer len) lenビットを持つNDD変数を作成する
apply(op, NDD a, NDD b) 2つのNDDにop ∈ {and, or, diff}の論理演算を適用する
not(NDD a) NDDに論理否定を適用する
exist(NDD a, Field field) fieldに対する存在量化をNDDに適用する
atomize(Set<NDD> N) NDDのセットN内のフィールドごとのアトムを計算し、NのエッジのBDDをアトムのセットに置き換える
update(NDD δ, NDD a) 新しいNDD δが追加されたときにアトムのセットを更新する; aはδ⇒aを満たす原子化されたNDD

特にatomizeとupdateは、NDDライブラリがアトムの計算と更新をネイティブにサポートするための重要な追加APIだ。これにより、検証ツールはこれらの操作のための独自のアルゴリズムを実装する必要がなくなる。

内部アーキテクチャ

NDDライブラリの内部実装で特に重要なのがノードテーブル(ユニークテーブル)だ。BDDでは各ノードが正確に2つの後続ノードを持つのに対し、NDDノードは可変数の後続ノードを持つため、可変サイズのメモリが必要になる。

NDDの実装では、各NDDフィールドごとに独自のノードテーブルを維持し、各ノードは後続ノードへのエッジマップを持つ。これにより、異なるフィールドのBDDノードは論理的に分離され、互いに干渉することなく同じBDDノードテーブルを共有できる。

最適化テクニック

NDDライブラリでは、いくつかの重要な最適化テクニックを採用している。

最適化テクニック 詳細
冗長性排除 NDDは「ユニーク性」「冗長ノードなし」という2つのBDDの冗長性排除ルールに加え、「冗長エッジなし」という第3のルールを適用する。同じ後続ノードを指す2つのエッジがある場合、それらをマージして単一のエッジにし、その条件は2つのマージされたエッジの条件の論理和にする
falseノードの削除 BDDでは通常この最適化をしないが、NDDでは各エッジがテスト条件を表すBDDと関連付けられているため、falseノードへのエッジを削除することでBDDを節約できる。これらのBDDは「デフォルト」ケースを表すことが多く、複雑になる傾向があるため解放することで他のBDDよりも大きな削減が得られる
操作キャッシュ BDDライブラリと同様に、NDDライブラリも操作キャッシュを維持し、操作の結果をキャッシュすることでNDD操作を大幅に高速化する

既存ネットワーク検証ツールへの適用

著者らはNDDライブラリを使用して、BDDベースの5つのネットワーク検証ツールを再実装した。これらの検証ツールは元のコードにわずかな修正を加えただけで、NDDライブラリを使用できるようになった。

検証ツール 修正行数
AP Verifier +25行, -159行
APT +84行, -167行
APKeep +66行, -311行
SRE +205行, -53行
Batfish +8行, -7行

修正行数が少ないことは、NDDライブラリがBDDベースの検証ツールにとって「ドロップイン」の代替品となることを示している。基本的に、検証ツールはBDDライブラリをNDDライブラリに置き換え、アトム計算のために独自に実装していたコードを削除するだけでよい。

例えば、データプレーン検証用のコードは次のように変更される。

// BDDを使用したコード
foreach 1≤i≤32: vars(i) ← bdd.createVar();
foreach d ∈ devices: Preds.add(calPortPred(d, vars));
// アトムを計算
foreach pred ∈ Preds:
  foreach a ∈ Atoms:
    set.add(bdd.and(a, pred));
    set.add(bdd.and(a, bdd.not(pred)));
Atoms ← set;
// ポートごとのアトムを計算
foreach d ∈ devices, p ∈ d.ports:
  foreach a ∈ Atoms:
    if (bdd.and(p.pred,a) = a):
      p.atoms.add(a);
// 到達可能性を検証
traverseRec(Atoms, src);
// NDDを使用したコード
var ← ndd.createVar(32);
foreach d ∈ devices: Preds.add(calPortPred(d, var));
// アトム化
ndd.atomize(Preds);
// 到達可能性を検証
traverseRec(ndd.true, src);

NDDを使用すると、コードが大幅に簡素化され、アトムの計算が完全に透過的になっていることがわかる。

性能評価と実験結果

著者らは3種類のデータセットを使用して実験を行った。

  1. 仮想化されたデータセンターネットワーク(VXLANベース)
  2. WANおよびキャンパスネットワーク(Stanford、Internet2、Purdueなどの実際のネットワーク)
  3. ファットツリートポロジー(BGPを実行)

データプレーン検証の実行時間


https://www.usenix.org/system/files/nsdi25-li-zechun.pdf

仮想化されたデータセンターネットワークでは、APKeep(NDD)は全てのスナップショットで実行が完了したが、BDDベースの検証ツールはタイムアウト(>24時間)またはメモリ不足(>256GB)で終了した。BDDベースの検証ツールが終了したスナップショットでも、APKeep(NDD)は10倍から105倍高速だった。

単一レイヤーネットワークでは、StanfordとInternet2でBDDとNDDの実行時間は同程度だったが、Purdueネットワークでは、NDDの使用はBDDよりも3倍高速だった。これらのネットワークでは、主に単一のフィールド(dstIP)のみに一致するため、フィールドを分離する利点はマルチレイヤーネットワークほど顕著ではない。

データプレーン検証のメモリコスト

リーフノード数 APKeep(BDD)メモリ KatraR(BDD)メモリ APKeep(NDD)メモリ
6 4.36GB 0.17GB 0.01GB
10 >20GB 2.88GB 0.01GB
20 >32GB >115GB 0.05GB
50 >80GB >115GB 0.16GB
100 >180GB >115GB 0.45GB
200 >180GB >115GB 1.42GB
500 >180GB >115GB 7.19GB

APKeep(NDD)のメモリ使用量はBDDをベースとする同等品と比較して桁違いに少ない。具体的には、6リーフノードのネットワークでは、APKeep(NDD)のメモリコストはAPKeep(BDD)の1/100未満、KatraR(BDD)の1/10未満だ。

メモリコストの主な要因はアトムの数だ。NDDを使用すると、アトムの数はネットワークサイズにほぼ線形に増加し、BDDベースの検証ツールよりもはるかに少ない。

パケット変換処理の効率


https://www.usenix.org/system/files/nsdi25-li-zechun.pdf

Purdueデータセットには合成したNATルールを追加し、NDDがパケット変換をどのようにサポートするかを評価した。

APKeep(NDD)はわずか4つのNATルールでもAPKeep(BDD)よりも10倍高速で、40個のNATルールでは100倍高速だった。APKeep(BDD)は80個のNATルールを挿入した後にメモリ不足に陥ったが、APKeep(NDD)は最大2000個のNATルールまで完了できた。

コントロールプレーン検証

BDDとNDDの両方を使用してBatfishとSREの2つのコントロールプレーン検証ツールを実行し、ファットツリートポロジー上でk=1,2,3のリンク障害下での全対到達可能性を確認した。

SREはBDDをNDDに置き換えることで、スケーラビリティが向上した。例えば、500ノードのファットツリーでk=1障害のケースでは、SRE(BDD)はBDDテーブルのオーバーフローにより中止したが、SRE(NDD)は完了できた。

Batfishの場合、NDDを使用してもスケーラビリティの向上は限定的だった。これは、データセットが単一のフィールド(dstIP)のみを使用し、SREのようなリンク変数を持たないためだ。

フィールド局所性の重要性

NDDの有効性を理解するために、著者らはPurdueデータセットのACLルールを修正し、より多くのルールが5つのフィールドすべてに一致するようにした実験も行った。


https://www.usenix.org/system/files/nsdi25-li-zechun.pdf

この実験から、NDDの性能向上は「フィールド局所性」の仮定に依存していることが明らかになった。すべてのルールがすべてのフィールドに一致する場合、フィールド局所性の現象は消失し、BDDを使用した場合のアトム数は非常に多くなくなる。これは理論的には失敗する可能性があるが、一般的なネットワークでは「フィールド局所性」の仮定は通常成り立つ。

NDDの応用シナリオ

NDDライブラリが提供する主要なAPIは、以下のような複数の応用シナリオで有効に活用できる。

自動アトム化

検証ツールは、NDDのatomize関数を使用してポート述語からアトムを自動的に計算できる。これにより、カスタムアルゴリズムを実装せずにアトム化されたNDDを取得できる。

インクリメンタルなアトム更新

ネットワーク更新後にアトムを一から再計算する代わりに、update関数を使用してアトムを効率的に更新できる。このプロセスは以下の手順で行われる。

  1. 変更の特定(ルールの挿入/削除)
  2. update関数を使用したアトムの更新
  3. アトムの転送(diff/or操作を使用)

パケット変換処理の効率化

NDDはパケット変換(NAT、IP-in-IP、VXLANなど)を効率的に処理できる。変換器は(match, field, action)のタプルとして表現でき、NDDを使用して効率的に処理できる。

まとめと展望

この論文では、ネットワーク検証用にカスタマイズされた新しいデータ構造であるNDD(Network Decision Diagram)を紹介した。NDDはBDDをベースにしているが、ネットワークのフィールドの概念をネイティブにサポートし、各フィールドを別々に処理することでメモリと計算効率を大幅に向上させる。

NDDを使用することで、5つのBDDベースのネットワーク検証ツールのメモリ使用量と実行時間を2桁削減できた。これは、NDDがBDDベースのネットワーク検証ツールの「ドロップイン」代替品となることを示している。

NDDはネットワーク検証の効率を大幅に向上させる可能性を持っており、今後の研究と実装により、さらなる進展が期待される。

Discussion