経験・勘ではなくロジックを使ってネットワークをテストする　MonoSATによる回答の仕組みと探索の効率化

3種類のバックエンドの候補

チェシャ猫氏：残りはTirosについて、もう少し深く掘っていきましょう。SMTソルバを使う話をしました。Tirosの中ではどういうふうにネットワークの意味論をSMTソルバに食わせられるかたちにして、具体的な検査を行なっているのかを、セクション3として話したいと思います。

（スライドを示して）冒頭にも挙げた論文ですが、基本的にはこの中に書かれていることに沿って話したいと思います。

この論文の特徴として、今までSMTソルバの話をしてきましたが、実はSMTソルバだけではなく、3種類のバックエンドの候補があります。

1つはSouffléで、これはDatalog言語というPrologのような言語の処理系になっていて、質問に答えるような機能を持っています。

2つ目はMonoSATで、これが本命です。SMTソルバで、且つグラフに関する理論ソルバを持っています。SATと名前がついていますが、実態はSMTソルバです。

3つ目がVampireで、これは自動定理証明器です。論理的な、つまり推論のステップについてもともとルールを持っていて、もともとある与えられた前提から欲しい結論が導かれるかどうかを、証明の筋道をたどって自動的に探索するのが、Vampireの動き方になります。

（スライドを示して）実際にベンチマークを取ると、こんなグラフが出ます。Vampireは遅すぎて論外です。なので、グラフには2つしか書いていません。右側の系列で見るとSouffléとMonoSATがあって、だいたいの場合はMonoSATのほうが早いです。どれぐらいかというと、10万インスタンスで1,000秒以内というぐらいのオーダーになります。

一部Souffléのほうが勝ってるものがあります。それはSATソルバ、SMTソルバの特徴で、複数解があり、その数え上げをしなければならない場合に、性能が劣化することがわかっています。

MonoSAT

というわけで、本命のMonoSATについて話しましょう。これはどういうものかというと、SMTソルバでグラフに関連する理論が実装されています。ユーザーの入力はエッジの候補です。そうすると、実際につなげるエッジをMonoSATが返してきます。

どういうことかを具体例で説明します。（スライドを示して）例えば、n1、n2、n3というものがあって、それぞれe1、e2、e3というエッジがあるとします。

必要な制約として、例えばe1、e2、e3のうち1つは通行不能で、e1かe3は通行可能であり、n1からn3へは到達可能にしたい場合に、これらの条件を与えるとe1、e2、e3のうち、実際に辺を張る必要があるのはどれかをMonoSATが返します。

（スライドを示して）具体的にはこれです。e1、e2という組み合わせでもいいのですが、今回はとりあえず「e1とe2はFalse、つながない状態で、e3にはTrue、ここに辺を張りなさい。そうすると与えられた条件、アサーションは全部満たされます」と答えるのがMonoSATの機能です。

VPCネットワークのエンコーディング

これをVPCの中でどうやって使うかというと、VPCのネットワークをグラフで表現します。ノードはネットワークのコンポーネントで、エッジは所属もしくはアタッチされているコンポーネント同士の関係です。

さらにCIDRに条件がある場合は、ビットベクトルの条件で表現します。例えば、セキュリティグループがブロックされているなど、条件が合わない場合は先ほどの「辺をつないでは駄目です、通行不可能です」という前提を使って、グラフを生成した時にエッジをつながせないようにします。といってもわからないので、具体例を話しましょう。

（スライドを示して）冒頭でやっていた「AからBへ行けるけど、AからCへ行けない」というものを例として取り上げます。

先ほどのネットワークをグラフにするとこんな感じです。インスタンスがあり、それにアタッチされたENIが暗黙のうちにあり、それぞれにセキュリティグループがついていて、サブネットに属しているという状態です。

さらに顕著なところとして、セキュリティグループに条件がついてました。CIDRが特定のものじゃないと通さない、というものです。

（スライドを指して）全部やると多いので、具体的にはこのセキュリティグループ1について話します。

まずセキュリティグループ1個に対して、今の図でいうと、上り側と下り側で関連する辺が計4つあります。イングレスルールについて意味がある値が指定されているので、ここを考えましょう。

イングレスなので、方向としては入ってくる方向、つまりe1とe2です。ファイアウォール、セキュリティグループを通過して、インスタンス側に入ってくるものです。

検査したいクエリはプロトコルがTCPで、srcAdrとdstAdrがあって、ポートが22というもので、これが通るかどうかが検査したい内容でした。

どういうふうにするかというと、先ほどの「つないでいいです／駄目です」という仮定をMonoSATに与える時に、それと同じ方法を使って、ここではImplies、つまり「なんとかならばなんとか」という条件を使い、もともとのクエリのソースアドレスにビットマスクを掛け、そのビットマスクを除いたところが172.0.0.0と一致していない、もしくはプロトコルまたはポートが一致していない、つまり、条件にどれか1つでも合致していないのであれば、e1とe2は「not」であり、どちらも辺をつないではならないということを、MonoSATに教えます。

最終的にインスタンスのAからBというのは、セキュリティグループ1についてはルールが合っているので通れる。つまり、通信がグラフの中をたどって通ることができる、到達可能であるということがMonoSATにわかります。

（スライドを示して）インスタンスAからインスタンスCに行こうとすると、セキュリティグループ2を通らなければならない。2にはイングレスルールが設定されていなかったので、先ほどの条件つきの「なんとかと違ったら通してはいけない」というところは、「何であっても通してはいけない」になるわけです。

そうすると、MonoSATとしてはセキュリティグループの両側にある辺は潰さないといけないことがわかります。そのため、最終的に生成されたグラフは、そこが連結にならないので、インスタンスAからCには通信が通らないことをMonoSATが回答できます。

なぜグラフ理論を採用したのか？

実はMonoSATが持っているグラフの理論は、わりと特殊というか、ちょっと珍しいです。なぜグラフ理論を採用したのか、なぜMonoSATはグラフ理論を効果的にSMTソルバの中に組み込めると思ったのかについて、最後に少し補足します。

これも論文の中身からきています。2015年の論文で『SAT Modulo Monotonic Theories』という、MonoSATの提案論文があります。ここに書かれた内容を簡単に説明します。

SATとModulo Theoriesの部分は「SMTソルバです」と言っていますが、鍵になるのはMonotonicの部分です。日本語だと単調な、という言い方になります。

この論文で定義されている、Boolean Monotonicな理論が鍵になっています。どういうことかというと、変数がBooleanのみであって、且つ各述語の各変数がFalseの時に成立するのであれば、Trueに変えても成立するであろうという特殊な条件式、述語のみを扱うようなもの、セオリーをMonotonic Theoryといいます。

具体的に、グラフの到達性というのはこの1種です。なぜならば、新しくエッジを引き直したとしても、引いていない状態、つまり、ある辺がFalseだった状態で到達可能ならば、Trueに直してもやはり到達可能である。この到達可能性が減ることはないわけです。これを利用して最適化、探索の効率化を行います。

何かというと、先ほどLazy SMTのオンラインインテグレーションのところで2つ効率化の話をしましたが、そこに効いてきます。

例えば、制約伝播を効率的に行えます。どういうものかというと、SATが割り当てを決める時に、TrueかFalseの組み合わせを探索するわけです。探索して、もし枝刈りできるところがあれば枝刈りしたいのですが、Monotonicity、単調性があるので、仮にまだ決まってないところを全部Trueにしてみて、理論ソルバに1回投げてみるわけです。

その状態で充足不可能、つまり決まっていないエッジを全部つないだとしても、そもそも到達可能にならないのであれば、すでに割り当てている範囲で駄目です。なので、その時点で即座にバックトラックに入れる、といった効率化ができます。

もう1つは、学習面の効率性です。最初の例では、P且つQ且つR且つSのどれかが間違っているという話だったので、全体を「且つ」にして「not」を学習させましたが、この場合に学習したい式はどれかというと、n1からn2が到達可能かどうかというものです。

そうすると、全部割り当てを埋めてしまって、仮にTrueにして理論ソルバに投げられるので、そうすると個々の式について成り立つか／成り立たないかは、ピンポイントにわかります。

そのため、最も厳しい、最も正確な情報、情報量が多い情報をグラフ理論の理論ソルバ側からSATソルバに戻すことができるということを使って、単調性を利用して学習を効率化します。この2つがMonoSATの仕掛けです。

セクション3のまとめ

さて、セクション3のまとめです。今回考えている問題は、VPCネットワークをどうやってSMTにエンコードするか、SMTソルバ側に理解できる・解けるかたちにするかという話でした。そしてTirosが採用しているのはMonoSATで、これはグラフに関する理論ソルバを持っています。

実際にはVPCのコンポーネントをノードで、接続をエッジで表現することで解けます。さらに、条件つきの部分はビットベクトルで表現して「合っていなければそのエッジをつないじゃ駄目」というふうにすると、到達度可能性がMonoSATによって回答できるわけです。

さらに、MonoSATの特徴的な部分として、単調性を使って探索の効率化を行っています。単調性というのは、「Falseの状態で成立すれば、Trueでも成立する」ということを使って、ある意味で上下から大さっぱに評価することで、可能性の枝を効率的に刈れる仕組みです。

Test Networks by Logic

さて、最後に本日のまとめをして終わりたいと思います。今回話したVPC Reachability Analyzerの機能として、特徴的なのは実際のパケットを送るのではなく、設定の“意味”をベースとして、そこから推論している、という点でした。

それはどうやって実現してるかというと、SMTソルバを使っています。具体的にSMTソルバというのは、SATソルバで不足している性能を個別ドメインの理論ソルバを使って埋めるのがその仕組みで、特にVPC Reachability Analyzerが依存してるMonoSATは、グラフによる表現を使っている特殊なSMTソルバです。