ネットワークのトラブルを全自動で検査　人間の判断を機械化するVPC Reachability Analyzerの機能

自己紹介とセッションの注意事項

チェシャ猫氏：スピーカーはProofCafeのチェシャ猫が務めます。「ネットワークはなぜつながらないのか」というタイトルでお話しします。私は、ふだんCloudNativeの界隈で活動しているので、もしかするとみなさんとどこかでニアミスしているかもしれません。

今日の話について、重要なディスクレーマーがあります。私は「AWSの中の実装はこういうふうだよ」という話をしますが、AWSの中の人ではありません。今回の内容は公開情報から再現されたもので、その論文が書かれた時はそうだった、ということしか意味していないので、もしかすると最新の情報とは違う可能性はあるかもしれないということを断っておきます。

セッションのアジェンダ

（スライドを指して）今回紹介したいのはこの論文です。『Reachability Analysis for AWS-Based Networks』。つまり「AWSのネットワークに対して、到達可能性を解析しよう」という、2019年に出ている論文です。これをベースにして解説していきたいと思います。

ただ、いきなり論文といってもたぶんみなさん困ると思うので、（スライドを指して）今日はこんなコンテンツの流れでやろうと思っています。話したいセクションは3つに分かれています。

まずセクション1として、VPC Reachability Analyzerがどういう機能なのかの概要です。一言でいうと、自動でネットワークの到達可能性を検査するツール・サービスですが、これを最初に解説します。

次に、セクション2として、SAT（Satisfiability Problem）ソルバとSMT（Satisfiability Modulo Theories）ソルバについて話したいと思います。真ん中にこれを持ってきた理由は、今日メインで話したいReachability Analyzerの要素技術として、中でこれらが使われているからです。そのため、復習しつつどういう仕組みになってるかを押さえておきたい、というのがセクション2です。

最後にセクション3として、SMTソルバを使って、実際にVPC（Amazon Virtual Private Cloud）の到達可能性をどうやって表現し、検査しているのかを話そうと思います。

VPCの構成

セクション1として、VPC Reachability Analyzerについてどんな機能なのかを解説していきます。（スライドを示して）今日はサンプルとして、すごく単純なネットワークですが、このようなVPCの構成を持ってきました。

プライベートネットワークが2つあって、それぞれインスタンスA、B、Cが3つ立っています。それぞれセキュリティグループが22を許すものと、まったく許さないものと2種類がついています。見てもらってわかるとおり、インスタンスA〜BはSSH、ポート22が通るのですが、Cには通らないです。セキュリティグループ2は22を開けてないからです。

みなさんこの図を見ると「まあそうだな」と思うわけです。しかし、これが実際はプロダクションに上げているような複雑なネットワークで、且つ、いろいろな設定が入っていることを考えると、パッと見て「ここSSHいけますね」とか「ここネットワーク通りますね」というのはなかなかわからないわけです。実際にデプロイしてみると「あれ？　なんか通らない」ということがあります。

ネットワークのトラブルシューティングとしてやるべき2つのこと

こういう時に、我々がやるべきことは大きく2種類あります。1種類目は、実際に通信してみて、疎通を確認することです。いわゆるスモークテストです。古典的にはpingやtraceroute、telnetのようなコマンドや、あるいは最近ではncを打つであるとか、実際にアプリケーションを動かしてみて、DBに接続できることを確認できます。

ただこの場合は、例えばping、tracerouteを打って特定のところまでいっていることはわかっても、それはAWSの設定とは直接紐づいていないので、どうやって直したらいいかは、やはりAWSのドメイン知識がいるわけですね。

もう1つの方法は、実際の通信を行わずに設定から確認することです。つまり、マネジメントコンソールを眺めて「ここの設定がおかしい」というアタリをつけることです。ただ、これをやろうとすると、各種設定項目を入れた時にどういう効果が発現するのかという意味を知っている必要があり、いわゆる職人芸になりがちです。

さて、この両者はある意味で対極的な2つのトラブルシュートの方針です。この2つに共通する顕著な性質があります。みなさんはたぶんピンとくると思います。

この2つに共通するトラブルシュートの性質は、「つらい」ということです。冒頭に挙げたような単純なネットワークならともかく、いろいろな設定といろいろなネットワークがあって、1ヶ所ルートテーブルがおかしいと全部台無しになるような複雑なネットワークを組んでいると、このネットワークのトラブルシュート、デバッグは非常につらいです。

VPC Reachability Analyzer

そんなあなたに今回紹介したいのが、先ほどから名前はずっと出てますが、VPC Reachability Analyzerです。どういう機能かというと、ネットワークの到達性、到達可能かどうかを、ある種全自動で検査してくれる機能です。

人間は何をやるかというと、送信元、送信先、ポート番号、プロトコルといった、通信を行う時のパスをワンセットで定義することです。それをReachability Analyzerに与えると、「到達可能です／不可能です」という答えが返ってきます。

人間がpingを打って「ここまでは行っているけれど、ここから先が行かない」ということやって原因究明をするという、あのつらい時間がなくなるのが、VPC Reachability Analyzerのウリです。

おもしろいことに、これは実際にはパケットの送出はしません。何をやってるかというと、設定項目のみを見て検査しています。つまり、先ほど「ドメイン知識が要る」という話をしましたが、このAnalyzerはドメイン知識を実際に持っています。

しかも、実際にパケットを送ったら、どこかで止まった時にその先がわからないわけですが、これは設定全体を見ているので「どこを直せばいいか」「どこが詰まっているか」を含めて判定してくれます。そこがReachability Analyzerのおもしろいところです。

（スライドを示して）具体的には、VPCの画面から左のメニューを見てもらうと、Reachabilityがあって、Analyzerが作れるようになっています。

パスの設定は、送信元と送信先、ポートとプロトコル。今回はインスタンスですが、他のネットワークコンポーネントでも可能です。

先ほど「AからBは通るけど、AからCは通らない」という話をしましたが、（スライドを示して）到達可能な場合に出てくる結果が左側で、送信元から送信先にどういうホップやコンポーネントをたどっていくかが逐一見えています。

不可能な場合は「何が原因です」というのが返ってきます。今回の場合は「イングレスルールがいずれにも適用されません」といっているので、このインスタンスCについているセキュリティグループ2のほうは、どのイングレスルールにも合致しないので通信がブロックされています。「ここを直しなさい」と言ってくるわけです。

3つのインフラの自動検査水準

VPC Reachability Analyzerは意味を理解している検査だという話をしました。これは重要なところで、私が思うに、インフラを何か自動的に検査したい時に、3つの水準があります。

まずは、レベル1です。一番単純なレベルとしては、構文論的な検査があります。典型的なのは、例えばCloudFormationのようなテンプレートを書いている、IaC（Infrastructure as Code）を書いている時に、そのテンプレートがYAMLとして文法的に正しいかどうかです。

ただ、みなさんご存じのとおり、これだけ正しくてもぜんぜん駄目なので、次にレベル2として、ルールベースの検査があります。例えば、個別の項目がルールに合致するかで、よくあるのは「0.0.0.0/0を開いてはいけない」みたいなものです。あるいは、「ボリュームは必ずエンクリプション（暗号化）されていること」というルールもあり得ると思います。これがレベル2の検査です。

その上にレベル3があります。レベル2の検査は、あくまでも個別の項目です。これに対してレベル3の検査は、意味論を含んでいます。

つまり、いろいろなコンポーネントに「こういう設定が入っています」ということで、「それなら結論として通信できますか、どうですか」というところの意味まで考えて、正しいかどうか（を判断する）というのが一番高度なレベルで、レベル3の検査水準です。今回話しているVPC Reachability Analyzerは、レベル3の検査が可能です。

セクション1のまとめ

というところで簡単ですが、VPC Reachability Analyzerそのものについて概要を解説しました。まず、VPCネットワークに限らず、ネットワーク全般について、トラブルシュートをやろうとするとわりとつらいという話です。

なぜつらいかというと、いろいろなところに設定があって、しかも全体がきちんと設定されていないと、途中で引っ掛かりする。そうなると「じゃあどこが原因なんだ」とコマンド打ったり、自分でコンソールを見たりして判断しつつ調べるという、人間の判断が入る必要性があるからです。

この判断をどうにかして機械化したいという動機がある時に、インフラの検査にはレベル感があって、まず一番単純なところから構文論があり、ルールベースがあり、そして一番上の意味論の検査までたどり着きたい、ということです。

そして、VPC Reachability Analyzerの到達可能性判定は、実際にパケットを送るのではなくて、設定の「意味」のみを見て意味論的な検査を行えます。いわゆるドメイン知識を内部に実装して自動化できているというのが特徴です。

さて、この後は、このVPC Reachability Analyzerがどうやって意味を実装されていて、Analyzerはその意味を元にしてネットワークについて検証しているのかを話したいと思います。

（次回に続く）