チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

関数型まつり 2025 で AWS と定理証明について話してきました

こんにちは、チェシャ猫です。

先日開催された関数型まつりで、AWS によって開発されたポリシー言語 Cedar と、その開発に使用された定理証明支援系 Lean について登壇してきました。公募 CFP 枠です。

fortee.jp

（TODO: 録画が公開されたら貼る）

前回登壇との関係

Cedar については、チェシャ猫自身が少し前、PHPerKaigi 2025 でも登壇しています。

前回と今回では、扱っている題材は同じですが、想定しているターゲットや興味の方向性が少し異なります。今回の登壇では Lean が保証している意味論的な定理や開発フローなど「Cedar がどのように設計・開発されたか」に焦点を当てた一方、前回はユーザ側の立場で「Cedar をどのように使うか」に焦点を当てた内容になっています。

AWS での構成例や Slice のアルゴリズムなど、今回オミットされた内容もあるので、もしよろしければこちらも併せてご覧ください。

質問への回答

当日、会場では 25 分間の枠を全てプレゼンで使い切ってしまったのですが、ありがたいことにその後の休憩時間や Twitter でいくつか質問をいただいています。

この質問は、自分では思いつかなかったのですが確かに良い着眼点だと思います。ドキュメントによれば、可用性が 99.9% を下回ると返金の対象になるようです。

はい、第一には複雑になったときに安全側に倒す、というのが目的です。Cedar の特徴として挙げた「安全性」の一環でもあります。

さらに言うならば、ポリシーを設計・定義する主体が分散している、というのも背景の一つです。ポリシー言語自体の動機として、個々のサービスを担当する個々のチームがポリシーを定義しても統一的に管理可能である、という点が挙げられます。仮に、拒否されていたものが許可で上書きできる場合、統制用の禁止ポリシーを定義しても個々のチームがそれを無効化することができてしまいます。拒否が優先する設計はこれを嫌ったものと見ることができます。

ちなみに、Lean で示されている定理「ポリシーの重複や評価順は結果に影響を与えない」にも同じ背景があります。また、これらの性質は IAM にも共通しています。基本的な思想として Cedar は、認可管理の対象が原則 AWS リソースに限られる IAM を、ユーザがアプリ用にも使えるように汎用化したものと考えて良いでしょう。

はい、その通りです。この .ok は、.ok と .error からなる直和型 Except の値コンストラクタです。Except.ok x の形で書くのが正式ですが、推論できる場合は省略しても大丈夫です。

今回紹介した二本目の論文には以下のような記述があり、数分のオーダで証明の検査を含めた Lean コンパイルが通るようです。実際の CI では Rust 側のビルドやテストも含めて実行する必要があるのでこれよりはかなり長くなるとは思いますが、いずれにせよ証明が CI 速度上のボトルネックになることはなさそうです。

Our Lean proofs are fast to verify, and the models are fast to execute. It takes about 3 minutes to check all proofs and compile models for execution.

余談ですが、これはモデル検査とは対照的です。モデル検査は常に状態爆発との戦いであり、多くのモデル検査器では、状態を圧縮したり効率的に枝刈りを行ったりといった最適化がボトルネックになります。

これは非常に鋭く、正しい指摘です。libfuzzer を用いることで未実行パスを重点的にテストするという基本方針の他、さらに論文中では、2 種類の生成戦略を併用していることが述べられています。

一つは型指向 (type-directed) 生成で、まずスキーマを生成した後、それに併せてエンティティとポリシーを生成する方法です。完全にランダムに生成した場合はほとんどの入力がエラーケースになってしまいますが、スキーマを先に確定させることで明らかにナンセンスなデータの生成を抑制します。

しかしこれだけでは、逆にバリデーションエラーになるような経路がテストできず、また when の条件が即値の true や false に偏りすぎる傾向があったようです。そこで Cedar の開発では、when に限って不整合を許容してバリエーションをつけるような生成も行なっています。

さらに論文中では、非常に生成確率が低かったことにより DRT で見逃されたバグについても触れられています。このバグは Cedar のポリシー評価器が無限ループに陥って停止しないというもので、「DRT では発見できなかった、Lean の停止性判定によって検出されたバグの例」として挙げられています。

参考リンク

github.com

PHPerKaigi 2025 で AWS のポリシー言語 Cedar について話してきました

こんにちは、チェシャ猫です。

先日開催された PHPerKaigi 2025 で、AWS によって開発されたポリシー言語 Cedar およびそのマネージドサービス版である Amazon Verified Permissions について登壇してきました。公募 CFP 枠です。

fortee.jp

www.youtube.com

学習リソース

もし、今回のトークを聞いて Cedar や Verified Permissions に興味を持った方がいたら、まずは公式で提供されているワークショップを触ってみることをお勧めします。ワークショップは以下の二種類があります。

前者は Cedar 自体の基本的な記法のみ扱うもので、Cedar の Playground を利用します。後者は AWS Lambda で作られたサンプルアプリと Verified Permissions を実際に AWS 上に構築して行うワークショップで、Cognito との連携やバッチリクエストによる最適化などを含む、より詳細な内容が学べます。若干の課金が必要にはなりますが、アプリケーションまで含めて動かせる後者のワークショップの方がお勧めです。

さらに、Cedar の設計の理論面についてより深く学びたい人は、元論文にもチャレンジしてみましょう。論文中では、今回のトークの中で紹介した式評価の意味論の他、バリデーションを支える型付けの健全性や、SMT エンコーディングも論じられています。

www.amazon.science

質問への回答

大変ありがたいことに、質疑応答や Ask The Speaker でいくつか質問を頂きました。ここにまとめておきます。

デフォルトが forbid であり、かつ forbid が permit に優先するということは、permit を指定した上でその中でピンポイントに forbid を指定するのか？

基本的にはその通りで、forbid が指定されるとそれを覆して許可することはできないため、forbid の範囲が広すぎると後から困ることになります。しかし、統一ポリシーを定義したいセキュリティチームの立場から見ると、これは逆に、forbid に指定した操作は個別のアプリチーム側では覆せないため確実な統制が可能になるという面もあります。

特に Cedar の場合、テンプレートからポリシーを動的に生成する用途が想定されています。つまりアプリチームがポリシーを作成できることは前提として織り込むべきであり、したがって「統制として確実に塞ぎたいところ」についてはセキュリティチーム側で予め forbid しておく、というのが基本的な考え方です。

有効期限付きの一時的な権限を表現する方法はあるか？

今回のスライドには含めませんでしたが、リクエストごとに変化するような条件を付与するための仕組みとして、Context が用意されています。

実際の使い方はアプリケーションの要件によりますが、例えば Resource に expires_at のような属性を持たせておき、リクエスト時の Context に現在時刻を載せて、ポリシーの when の中で比較することが可能です。

認証を Cognito 以外で行なっている場合、Verified Permissions を使用することはできるか？

はい、可能です。Verified Permissions は OpenID Connect (OICD) の ID プロバイダであれば Cognito に限らず連携することができます。また、トークンに含まれる claim は Cedar の属性としてマッピングされるため、ポリシーの中で参照することも可能です。

参考リンク

YAPC::Hakodate 2024 で様相論理について話してきました

こんにちは、チェシャ猫です。

先日開催された YAPC::Hakodate 2024 で、様相論理について登壇してきました。公募 CFP 枠です。

fortee.jp

しばらく後に録画アーカイブも公開される予定です。

質問への回答

当日は、ありがたいことに会場で何名かの方が質問を出してくれました。回答をまとめておきます。

EG φ の検査アルゴリズムにおいて、φ が真になるような強連結成分が複数見つかった場合はどうするのか？

EG φ が真になるのは「その状態から始まって φ を満たし続ける無限パスが存在するとき」なので、そのようなパスが複数見つかっても真偽に影響はありません。

もし実装するのであれば、強連結成分を順に試し、最初に条件に合致したものを見つけた時点で真を返すのが自然だと思います。

濾過法を適用する際の φ はどこから出てきたのか？

濾過法は大まかに言えば、「φ の（有限とは限らない）モデルが存在するとき、そこから有限モデルを作り出す手法」です。

つまり φ は最初から与えられていて、「その φ の有限モデルが存在するか？」という問題を考える上で使用されるのが濾過法です。より一般には、濾過法は「部分論理式について閉じた論理式の集合」に対して定式化されます。

システムを Kripke モデルに変換する際にギャップがあると思うが、実際にはどのように使用されるのか？

基本的に、モデル検査はアルゴリズムやプロトコルの設計時点で役に立つものだと考えておくのが良いと思います。

モデル検査では状態数の爆発が問題になることもあり、検査する対象は実際のソースコードというよりは抽象的な設計の方がメインになります。モデル検査を含む形式手法は品質保証の手法として語られることもありますが、品質保証として一般にイメージするような統合テストではなく、もっと手前の段階で設計検討時に仕様バグを探すという方が実態に近いです。

また、今回のスライドではあまり触れなかった部分ですが、人間が直接 Kripke モデルを書き下すのは困難なので、大抵のツールでは何らかの DSL でアルゴリズムを記述し、それを内部的に変換することになります。

参考文献

#技術書典 16 で Go を使って #自作モデル検査器 をつくる本を頒布します

こんにちは、チェシャ猫です。

今回、技術書典 16 にて、新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』を頒布します。

techbookfest.org

どんな本？

ただツールを使うだけの形式手法から、君の手でつくる形式手法へ。Go 言語でモデル検査器を実装しながら学ぼう！

書名の通り、Go でモデル検査器を実装する本です。Pramo 言語と名づけた本書オリジナルのモデリング言語を定義し、その可視化器と検査器を作成します。

Pramo 言語は、ある種のマルチスレッドをサポートするプログラミング言語であり、Go の埋め込み DSL として記述されます。例えば有名な「食事する哲学者」は以下のように実装されます。

func badPhilosopher(name procName,
    right, left lockName, hold varName) process {

    return Process(name,
        For(
            Case(Lock(left),
                Assign(hold, Add(Var(hold), Int(1))),
            ),
            Case(Lock(right),
                Assign(hold, Add(Var(hold), Int(1))),
            ),
            Case(When(Eq(Var(hold), Int(2))),
                // eating
                Assign(hold, Int(0)),
                Unlock(left),
                Unlock(right),
            ),
        ),
    )
}

よく知られている通り、哲学者が二人以上いる場合、お互いに相手が持っているフォークが空くのを待ち続けることでデッドロックが発生します。そこで、デッドロックが発生するのはどのような状況か、あるいはどう変更したら回避できるのか、といった問題について、プログラムを実際に実行するのではなく、生じうるすべてのタイミングの可能性に対して網羅的にチェックすることを考えます。これがモデル検査であり、本書であなたが実装する Pramo 言語です。

ちなみに、これは本の中には書いていないのですが、Pramo 言語の元ネタになっているのはモデル検査器 SPIN で使用される Promela 言語です。Promela 言語は Dijkstra による Guarded Command がベースとなっており、本書の Pramo 言語も同様ですが、Pramo は Promela の機能をいくつか落として簡略化し、その代わりに Go の DSL として自由度が高い記述できるようにしました。

各章の概要は以下の通りです。まず第一章では、Pramo 言語の構文と意味論を定義します。次の第二章では、モデル検査に使用される Kripke モデルの概念を紹介した上で、Pramo 言語の記述から Kripke モデルへの変換を行い、いくつかの仕様の検査を実際に試してみます。最後に第三章では、よりモデル検査らしい話題として、CTL（Computational Tree Logic、計算木論理）による仕様記述とその検査アルゴリズムを取り上げます。いずれも、実装する過程で動作する完全なソースコードを掲載しています。

読んでみて、もし面白かったとか参考になったなどポジティブな感想を持っていただいた方は、是非 X（旧 Twitter）でハッシュタグ #自作モデル検査器 をつけて投稿してくださると幸いです。形式手法とモデル検査、盛り上げていきましょう！

値段は？

「電子版のみ」もしくは「電子版 + 紙版セット」の二つのコースがあります。「紙版のみ」は技術書典のレギュレーション上ありませんのでご注意ください。特に、電子版を入手しようとして両方ダブって買うことがないように注意しましょう。電子版は常についてきます。

  • 電子版のみ：1,000 円
  • 電子版 + 紙版セット：1,200 円

どこに行けば買える？

オフライン会場での直販と、オンライン会場での通販があります。

オフライン会場

オフラインイベントは以下の通りに開催されます。

  • 日時：2024 年 5 月 26 日（日）11:00〜 17:00
  • 場所：池袋サンシャインシティ 展示ホールD（文化会館ビル 2 F）
  • サークル配置：あ08（入り口すぐ、右手側）

techbookfest.org

入場は無料ですが、事前に入場整理券の発行が必要です。整理券は時間帯ごとに発行されており、25 日現在 12:00 までの枠は売り切れていますが、13:00 以降はまだ残りがあるようです。

また、会計には技術書典公式の「かんたん後払いアプリ」が必要です。現金の取り扱いはありませんのでご注意ください。

オンライン会場

オンラインマーケットは以下の通りに開催されます。

  • 日時：2024 年 5 月 25 日（土）10:00 頃 〜 2024 年 6 月 9 日（日）23:59 頃

techbookfest.org

なお、オンラインマーケットでも「電子版のみ」「電子版 + 紙版セット」の両方が購入可能で、価格もオフラインイベント会場と同じです。ただし、オペレーションの都合上、印刷所への発注は会期終了後にまとめて行うため、手元に紙版の本が届くのは 6 月末以降になります。もし少しでも早く紙版が読みたい場合は、オフラインイベントに参加しましょう。

まとめ

以上、技術書典 16 の新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』の頒布情報でした。読んだら #自作モデル検査器 でよろしく！

Developers Summit 2023 Summer でサーバーレスについて話してきました

こんにちは、チェシャ猫です。

先日開催された Developers Summit 2023 Summer で、サーバーレスコンピューティングの形式化について登壇してきました。公募 CFP 枠です。

event.shoeisha.jp

内容は Jangda et al. (2019) による論文 "Formal Foundations of Serverless Computing" を軸にしています。この論文はサーバーレスコンピューティングに対して操作的意味論の定式化を行うものであり、プログラミングの国際学会 OOPSLA '19 の Distinguished Paper を受賞しています。

なお、同様のテーマは AWS Dev Day 2022 でも登壇しています。スライドも大部分は共通ですが、解説が不足していた点を具体的に補足したり、逆に意図して細部を省略したりしてあるため、前回から比べると全体としてはかなりわかりやすくなっているはずです。

Twitter やチャットでの反響は正直なところいまひとつでしたが、スライドの解説資料としての出来には満足しています。

ccvanishing.hateblo.jp

最後にセッションの本筋とは直接関係しない余談を一つ。質疑応答の最後、自分が登壇する時に何を重要だと思っているかについて触れる機会がありました。自分の中では以前から考えていたことですが、今まで登壇という場で述べる機会がなかったので今回話せて良かったです。ちなみに何を話したのかは、当日の講演を聞いた人だけの秘密。

2022 年、アウトプットの思い出

こんにちは、チェシャ猫です。2022 年中は大変お世話になりました。本記事では自分自身への備忘も兼ねて、本年度の対外的な発表についてまとめておこうと思います。

2022 年の活動実績

2022 年の登壇は 3 件でした。うち（先着や抽選ではなく）CFP に応募して採択されたものは 2 件です。以前は頻繁に登壇していた LT の回数を今年はかなり控えていたこともあり、件数としては少ない水準となりました。

賢く「振り分ける」ための Topology Aware Hints

Kubernetes Meetup Tokyo #52 での発表です。

Kubernetes の Service に対するトラフィックを、ネットワーク的に近い Pod に対してルーティングする機能、Topology Aware Hints を解説しています。具体的には Node に対する Label で表現された各 Zone に対して、その Zone に存在する Node の CPU 数の比によってトラフィックのルーティング先が決まります。ルーティングのロジックはやや複雑ですが、もし興味があればスライドを参照してください。

ちなみに、Kubernetes においてネットワークトポロジに応じてトラフィックを操作する仕組みは、今回の Topology Aware Hints 以前にも、いくつかの KEP で提案され没になっています。スライド中では過去の提案がどのような問題意識でなされ、なぜ没になったのか、その辺りの経緯も解説してみました。

サーバーレスは操作的意味論の夢を見るか？

AWS Dev Day Japan 2022 での発表です。公募 CPF 枠で、昨年も登壇しているので 2 年連続の採択になります。

内容としては、サーバレスコンピューティングに対して操作的意味論による基礎づけを行なった 2019 年の Jangda らの論文、Formal foundations of serverless computing について解説しました。OOPSLA '19 の Distinguished Paper にも選出されています。

解説したのはこの論文のうち前半部分、具体的には Section 4 まで相当です。イベントの参加者の大半はこのような形式化には慣れていないことを考え、後半部分のより現実的かつ複雑な意味論を諦める代わりに「操作的意味論とはなにか」「推論規則の読み方」「双模倣の例」といった基本的な事項を解説することを選択しました。もし興味があれば元論文にもチャレンジしてみてください。

ccvanishing.hateblo.jp

また、同じ論文について Qiita に記事を書かれている方も発見しました。こちらの記事は操作的意味論への基本的な知識は仮定されている一方、元論文の前半だけでなく最後のセクションまで満遍なく記事として起こされています。

qiita.com

謎は全て解けた！安楽椅子探偵に捧げる AWS ネットワーク分析入門

CloudNatice Days Tokyo 2022 での発表です。公募 CFP 枠です。

内容は AWS においてネットワークに関するクエリに回答するエンジン Tiros にまつわるものです。Tiros は内部的に SMT ソルバの一種 MonoSAT を使用しており、AWS のネットワーク構造をグラフ構造としてエンコードして MonoSAT に解かせることで、コンポーネント間の到達可能性について推論を行います。

内容としては昨年の AWS Dev Day Online Japan と共通する部分が多いですが、中盤の SMT ソルバに関する一般論と SAT 問題の単調性に関する解説を一部削り、その代わりに前回扱えなかった Blocked Path Analysis の解説を追加してあります。Blocked Path Analysis は SMT ソルバを使用する Tiros の大きな特徴であり、普通にイメージする Packet Probing によるネットワーク検査と比べて明確な挙動の差が生じる部分です。今回 Blocked Path Analysis について解説を追加できたことで、前回のスライドと比較してもより有意義な解説になったと思います。

ccvanishing.hateblo.jp

ccvanishing.hateblo.jp

まとめ

以上、2022 年のスライド一覧とセルフ短評でした。

ところで、Speaker Deck のスライドページをご覧いただくと分かる通り、今年の登壇はスライド閲覧数が異様に少ないのも特徴です。特に CloudNative Days Tokyo 2022 のスライド は、大規模イベントかつ Twitter 上でそれなりに Like されているにもかかわらず、スライド閲覧数が以前の LT の水準にすら達していません。

もともと Speaker Deck の閲覧数は「たまたま界隈の有名人が好意的なコメントをくれた」「はてなブックマークで初動が良かった」といった要素で変動するため、所詮は水物であり、過剰に意識してもいいことはありません。とはいえモチベーションに影響するのも事実なので、現状の登壇 + スライド公開という発表手段を来年以降もメインに据えるかどうかも含め、ちょっと検討しようかなと考えています。情報のストックと検索性という意味では、スライドよりもブログ記事の方が望ましいかもしれませんね。去年も同じことを書いてますが…。

それでは、2023 年も張り切っていきましょう。よろしくお願いいたします。

CloudNative Days Tokyo 2022 に「謎は全て解けた！ 安楽椅子探偵に捧げる AWS ネットワーク分析入門」というタイトルで登壇してきました

こんにちは、チェシャ猫です。

先日開催された CloudNative Days Tokyo 2022 で、SMT ソルバを用いた AWS のネットワーク検査機能、VPC Rechability Analyzer と VPC Network Access Analyzer について話してきました。公募 CFP 枠です。

イベントサイトにて録画も視聴可能です。

event.cloudnativedays.jp

今回の登壇は「事前録画を提出」「当日リモートで登壇」「現地で登壇」のいずれの方式が選択可能だったのですが、自分は現地で登壇しました。

現地参加者全員が一つの部屋に集まる Keynote では意外と人がいるなという印象でしたが、午後のブレイクアウトセッションでは 6 部屋あったこともあり、自分のセッションの現地参加者は 10 数人程度でした。

完全オフラインだった頃の熱気には及びませんが、対面でお話しする場は数年ぶりで、聴衆の反応を見ながらプレゼンできる体験はやはり良いものです。

講演概要

ネットワークのトラブルシューティングは辛い作業になりがちです。特に AWS の VPC ネットワークは多数の設定が必要であり、疎通ができない場合にその原因を発見・修正するためには往々にして高いスキルが必要となります。

このような状況に対処し、誰でも体系的にネットワーク不通の原因を解消できる助けにするため、AWS は VPC Reachability Analyzer と VPC Network Access Anazlyer という二つの機能を提供しています。前者は、プロトコルやポート番号を指定することで二つのコンポーネント間の疎通を確認し、到達可能でない場合はその原因となっているコンポーネントを指摘します。また後者は、あらかじめクエリを登録しておくことで条件に合致する経路を一覧表示・分析し、コンプライアンス準拠等の目的に役立てることができます。

この機能には「到達不可能な場合であっても、その原因部分を含め送信元から送信先への完全な経路が得られる」という特徴があります。一般によく用いられるパケットを送出するタイプの疎通確認 (Packet Probing) において、不通となっているコンポーネントから先の経路情報は得られません。すなわち、VPC Rechability Analyzer はパケット送出によって経路を探索しているわけではない、ということがわかります。

今回の講演ではこの点について、AWS から公開されている 2 本の論文をベースにして解説を行いました。VPC Rechability / Network Access Analyzer は内部的には AWS Tiros と呼ばれるエンジンがクエリ処理を担っており、さらにそのバックエンドとして SMT ソルバの MonoSAT を使用しています。これに加え「不通の原因部分を含む完全な経路」をユーザに提示するため、与えられた制約をいくつかのクラスに分類し、段階的に Minimal Correction Subset (MCS) を計算する手法が用いられています。

補足

講演動画を見た方向けの補足です。スライド中に、MonoSAT のパフォーマンスについて「10 万（EC2）インスタンスで数 100 秒 〜 1,000 秒」と記載した部分があります。この情報について、講演では咄嗟に「単位の間違いでは」と言ってしまいましたが、グラフを見ればわかる通り間違いではありません。このデータは MonoSAT の規模的な限界性能、かつ Soufflé では解けないベンチマークの例として挙げられています。

Twitter の反応

現地登壇ということもあってか、今回はなんだか語り口が好評でした。この記事を読まれている方は、スライドだけでなく動画をご覧いただくと良いかもしれません。

参考文献

おまけ：デモ環境の作成

以下の CloudFormation テンプレートを使用することで、VPC Reachability Analyzer と VPC Network Access Analyzer による分析を実際に試してみることができます。

このテンプレートの使用によって発生した問題には責任は持てません。特に、小さいとはいえ ECS インスタンスを実際に立てること、および両 Analyzer ともに有料（特に Reachability Analyzer は実行ごとに 0.1 USD と高価）である点にはご注意ください。

---
Description: 'Demo for CloudNative Days Tokyo 2022'
AWSTemplateFormatVersion: 2010-09-09

Mappings:
  RegionMap:
    ap-northeast-1:
      execution: ami-02892a4ea9bfa2192

Resources:
  VPC:
    Type: AWS::EC2::VPC
    Properties:
      CidrBlock: 172.0.0.0/16

  InternetGateway:
    Type: AWS::EC2::InternetGateway

  InternetGatewayAttachement:
    Type: AWS::EC2::VPCGatewayAttachment
    Properties:
      InternetGatewayId: !Ref InternetGateway
      VpcId: !Ref VPC

  SubnetX:
    Type: AWS::EC2::Subnet
    Properties:
      VpcId: !Ref VPC
      CidrBlock: 172.0.1.0/24

  SubnetY:
    Type: AWS::EC2::Subnet
    DependsOn: InternetGateway
    Properties:
      VpcId: !Ref VPC
      CidrBlock: 172.0.2.0/24
      MapPublicIpOnLaunch: true

  PublicRouteTable:
    Type: AWS::EC2::RouteTable
    Properties:
      VpcId: !Ref VPC

  PublicRouteTableAssociation:
    Type: AWS::EC2::SubnetRouteTableAssociation
    Properties:
      RouteTableId: !Ref PublicRouteTable
      SubnetId: !Ref SubnetY

  PublicRoute:
    Type: AWS::EC2::Route
    Properties:
      RouteTableId: !Ref PublicRouteTable
      GatewayId: !Ref InternetGateway
      DestinationCidrBlock: 0.0.0.0/0

  SecurityGroup1:
    Type: AWS::EC2::SecurityGroup
    Properties:
      GroupDescription: 'Sample SG 1'
      VpcId: !Ref VPC
      SecurityGroupIngress:
        - CidrIp: !GetAtt VPC.CidrBlock
          IpProtocol: 'tcp'
          FromPort: 22
          ToPort: 22
      SecurityGroupEgress:
        - CidrIp: 0.0.0.0/0
          IpProtocol: '-1'

  SecurityGroup2:
    Type: AWS::EC2::SecurityGroup
    Properties:
      GroupDescription: 'Sample SG 2'
      VpcId: !Ref VPC
      SecurityGroupIngress:
        - CidrIp: !GetAtt VPC.CidrBlock
          IpProtocol: 'tcp'
          FromPort: 22
          ToPort: 22
      SecurityGroupEgress:
        - CidrIp: 127.0.0.1/32
          IpProtocol: '-1'

  InstanceA:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetX
      SecurityGroupIds:
        - !Ref SecurityGroup1
      Tags:
        - Key: Name
          Value: InstanceA

  InstanceB:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetX
      SecurityGroupIds:
        - !Ref SecurityGroup2
      Tags:
        - Key: Name
          Value: InstanceB

  InstanceC:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetY
      SecurityGroupIds:
        - !Ref SecurityGroup1
      Tags:
        - Key: Name
          Value: InstanceC

  ReachablePath:
    Type: AWS::EC2::NetworkInsightsPath
    Properties:
      Source: !Ref InstanceA
      Destination: !Ref InstanceC
      DestinationPort: 22
      Protocol: tcp
      Tags:
        - Key: Name
          Value: 'Reachable Path'

  BlockedPath:
    Type: AWS::EC2::NetworkInsightsPath
    Properties:
      Source: !Ref InstanceB
      Destination: !Ref InstanceC
      DestinationPort: 22
      Protocol: tcp
      Tags:
        - Key: Name
          Value: 'Blocked Path'

  AccessToInternet:
    Type: AWS::EC2::NetworkInsightsAccessScope
    Properties:
      MatchPaths:
        - Destination:
            ResourceStatement:
              ResourceTypes:
                - AWS::EC2::InternetGateway
      Tags:
        - Key: Name
          Value: 'All Access To Internet'