この記事は「2025 Japan AWS Jr. Champions 夏のQiitaリレー」の20日目の記事です。
過去の投稿（リンク集）は 以下からご覧ください！
https://qiita.com/natsumi_a/items/80539843482fed4cd648?utm_campaign=post_article&utm_medium=twitter&utm_source=twitter_share
はじめに
この記事では「VPC Reachability Analyzer」でネットワークの到達可能性を検証する際に、裏側で何がされているのかがなんとなく理解できことをターゲットにしています。
VPC Reachability Analyzerとは
VPC Reachability Analyzerとは、AWS上のネットワークに関する静的な設定分析ツールであり、ネットワークにおけるパケットの到達可能性の評価に利用する。
ここでいう「静的な設定分析ツール」とはどういう意味だろうか。
例えば、最も単純なネットワークの到達可能性として思いつく評価手法は、対象となるネットワークに対して実際にパケットを流し、それを観察することで評価する方法である。
ネットワークエンジニアでなくとも、Pingでの疎通確認を行った経験があるかもしれないが、それも動的評価の一種である。
※実際にパケットを生成してTCP通信の確認をしたい場合には、ICMP pingではなく、hpingなどを利用する。
これが動的なネットワークの到達可能性評価である。
一方で、Reachability Analyzerは先述のとおり「静的」な手法であり、実際にネットワークに対してパケットを流すといったことは行わない。
AWSのリソース情報をもとに、送信元から宛先まで到達可能な経路が存在するかをAWSにおける設定値にのみ基づいて評価する。
AWS上のネットワークはルートテーブルやセキュリティグループ、ネットワークアクセスコントロールリストなどの設定値に基づいてルーティングされるが、Reachability Analyzerではこの設定値に対して、調査対象のパケットがたどる経路を網羅的に探索している。
AWSのパラメーターシートと格闘するネットワークエンジニアの仕事をもっと効率的に行っているツールといえる。
Reachability Analyzerは実際にパケットを流すということをしないため、システムに対して一切の影響を与えることなく評価が可能であり、稼働中のシステムにおけるネットワークの評価手法として重宝されている。
実際に経路の探索を行うと以下のように、到達可能であるかや到達可能な際にはその到達経路を示してくれる。
では、Reachability Analyzerはどのようにしてパラメータから到達可能性を評価しているのか。
今回は2019年に公開されたReachability analysis for AWS-based networksを元にかいつまんで見てみる。
Reachability AnalyzerとTiros
Reachability Analyzerで経路探索する際には、エンジンとしてTirosと呼ばれる推論エンジンを用いている。
TirosはAWSによって開発された推論エンジンだ。
Tirosでは、大雑把には下記の流れで到達可能性を評価している。
- AWSのネットワークリソースをモデル化
- 論理式として到達可能性を定式化
- SMTソルバーを利用して評価
そもそもSMTやSATとはなにか
もう少し細かくTirosでの到達可能性の評価手法を追う前にSMTとSATについてざっと記載する。
SAT (Satisfiability：充足可能性問題）
命題について真か偽のどちらかの値をとる変数とみなした上で、考察対象である推論を記号化した命題論理式に対して変数の組み合わせによって命題論理式正となる組み合わせを探る問題である。
例えば下記の論理式を正とするようなx1、x2が存在するかを扱う問題である。
※x1=真、x2偽で論理式全体として正になる。
SMT（Satisfiability Modulo Theories：背景理論付き充足可能性問題）
命題のみしか扱えないSATに対して理論(Theory)を追加し、命題以外も扱えるように拡張したものがSMTである。
SMTではSATに比べて整数理論、ビットベクトル、グラフ理論など扱える幅が広がる。
特にMonoSATは reachability（到達性）・path(経路)などのグラフ構造をネイティブにサポートしているという特徴がある。
MonoSATによる到達可能性の評価
TirosではMonoSATと呼ばれるSMTソルバーを内部で利用している。
MonoSATはグラフ理論に特化しており、コンポーネント(node)間のつながりを表すedgeについてその到達性を評価するツールである。
VPC Reachability Analyzerでは、AWS上のネットワークコンポーネントと、コンポーネント間の繋がり、そしてクエリをなんとかして充足可能性問題にモデル化して解いてあげようということを行っているのである。
つまり、検証したい経路の送信元(start)と宛先(end)について、下記の論理式が正となりうるかを評価したいのだ。
モデル化と評価
ではどのように評価していくか、天下り的ではあるが説明をしていく。
構成要素
モデル化では、ENI、サブネット、ルートテーブル、IGW、NAT などのAWSネットワークコンポーネントの「ノード(node)」とし、nodeのつながりを意味する「エッジ(edge)」という構成要素によって、シンボリックグラフ(symbolic graph)でネットワーク構成を表現する。
繋がりという表現ではやや曖昧であるが、言い換えれば、あるノードから別のノードに通信が到達可能であるかを表現するための変数であると言い換えることができる。
到達可能性を表現しているので、その変数が取り得るのは当然True or Falseである。
この到達可能性の変数をedge(eni1,sunbetWeb) とした場合に、edge(eni1,sunbetWeb) はeni1からsunbetWebへ到達可能であれば正(True)であり、到達不可であれば偽(False)であるという具合である。
一方で、到達可能かを評価するには経路だけではなく、ネットワークを流れるパケットもモデル化する必要がある。
パケットはシンボリックパケット(symbolic packet)としてビットベクトルの形式（ビットで設定を表現）で表現される。
パケットにはプロトコル(protocol)、送信元アドレス(srcAdr)、宛先アドレス(dstAdr)、送信元ポート(srcPort)、宛先ポート(dstPort)で表現され、それぞれビットベクトルで次のように表現される。
| フィールド | ビット数 |
|---|---|
| protocol | 8ビット |
| srcAdr | 32ビット |
| dstAdr | 32ビット |
| srcPort | 16ビット |
| dstPort | 16ビット |
制約条件の追加と評価
到達可能性を評価するために、edge(eni1,sunbetweb) に対してパケットの送信元アドレスや宛先アドレスが ENI の IP アドレスと一致しない場合にエッジが無効になるような制約を加える。
つまり、ENIから送信されるパケットはその送信元アドレスがENIのIPアドレスに一致し、ENIで受信するパケットはその宛先アドレスがENIのIPアドレスに一致するということである。
これを論理式で表現すると下記のようになる。
セキュリティグループなどについても同様にして制約条件として追加することができる。
最後に、SMT ソルバー（MonoSAT）を使って、記号グラフに対して到達性制約を追加していく。
- 開始ノード（start）と終了ノード（end）をグラフに追加
- 開始ノードからクエリの送信元へのエッジを追加
- クエリの宛先から終了ノードへのエッジを追加
ここまで文章と式によって記載をしてきたが、これを図にすると以下のようなイメージだ。
ここまでに作成したモデルに対して、論理式reaches(start,end)が正となる場合に、クエリの送信元から宛先に到達する経路が存在すると評価することができる。
例
インターネットからSSH接続可能なインスタンスが存在するかをクエリする場合には下記のような成約を追加する。
- 開始ノード（start）をインターネットとする
- 終了ノード(end)をインスタンス1とする
- パケットのビットベクタを下記のように設定する
protocol = 6 (TCP)
dstPort = 22
これらに対してSMT ソルバー MonoSAT を用いてreaches(start,end)が正になる組み合わせが存在するかを評価することで到達可能性を得ることができる。
先の図についてNGパターンの経路も追加すると、ちょうど赤字の経路が到達可能な経路として返されることになる。
このように到達可能な経路が存在すればその経路を返し、存在しなければ到達不可としてTirosは経路の到達可能性を評価しているのだ。
まとめ
細かいことを長々と記載をしたが、結局のところ、Reachability Analyzerは下記にて経路の探索をしている。
- AWSのネットワークリソースをモデル化
- 論理式として到達可能性を定式化
- SMTソルバーを利用して評価
MonoSATについても公開情報(論文)の閲覧が可能なため、気になった読者の方がいらっしゃれば、ぜひ読んでみてほしい。
そして私のために記事を書いてください。
※なお、2019年の公開情報を元に記載しているので現在は異なっている可能性があります。