こんにちは、チェシャ猫です。
先日開催された July Tech Festa 2021 で、AWS のアクセス制御検査ツール Zelkova について発表してきました。公募 CFP 枠です。
講演概要
一般に、AWS 上のリソース設定を変更したときに何が起こるのかを事前に検査するのは難しい作業です。特に、複数の設定がマージされた結果として最終的なアクセス許可が決まるような場合、単独の項目をルールベースでチェックするだけでは限界があります。
今回の発表中では、インフラに対する検査の水準を以下の 3 つのレベルに分けて定式化しました。
- Level 1：構文論的な検査。テンプレートが文法的に正しいかどうかを確かめる
- Level 2：ヒューリスティックな検査。意図した性質が成り立つかどうかを、特定の設定項目に関する条件として書き下した上で、その条件を確かめる
- Level 3：意味論的な検査。意図した性質が成り立つかどうかを直接確かめる
ここで言う Level 3 の検査を実現するのが Automated Reasoning と呼ばれる技術です。設定ファイルの個別の項目をテストするのではなく、設定ファイルに記述された内容から最終的に意図した性質が成り立つかどうかを「自動的に推論」してくれます。
今回紹介した IAM Access Analyzer は、エンドユーザが Automated Reasoning を利用できる面白い機能です。例えば S3 Bucket の Bucket Policy を変更したい場合、適用する前にプレビューの段階で、外部からの不用意なアクセスが許可されているなどのセキュリティ的な問題を検出できます。
IAM Access Analyzer の基礎になっているのは Zelkova と呼ばれるエンジンで、さらにその内部では SMT ソルバである Z3 が検査を行っています。発表中に述べた Zelkova の実装に関する情報は、以下の論文に基づきます。
参考リンク
IAM Access Analyzer
IAM Access Analyzer 自体は無料で利用することができます。いくつかのリソースに対してアクセス権限の検査ができるようになっていますが、実験する場合は S3 Bucket の Bucket Policy で試すのが最も簡単で、結果もわかりやすいと思います。
例えば、Bucket Policy を用いてアクセス元として 11.22.33.0/24 を Allow し、11.22.33.44/32 を Deny した場合、Deny の方が CIDR の狭いため Access Analyzer はこれを過剰なアクセス許可としてプレビュー段階で検知します。しかしこれを逆にして 11.22.33.44/32 を Allow し 11.22.33.0/24 を Deny するよう書き換えると、今度は Deny の方が Allow を覆い隠す形になるため指摘は消えます。
このことから、Access Analyzer は CIDR 指定を単なる文字列として比較しているわけではなく、包含関係を考慮した上で最終的な権限の状態を推論していることがわかります。
SMT ソルバ
SAT ソルバや SMT ソルバの仕組みについては、以下のスライドがわかりやすく非常におすすめです。
www.slideshare.net
今回紹介した Zelkova には、SMT ソルバとして Z3 が組み込まれています。Z3 は Microsoft Research により開発されたソルバで、SMT ソルバとしては CVC と並んで非常にメジャーなものです。
オンラインで Z3 を実行できるチュートリアルサイトもあります。Zelkova で使用されている文字列やビットベクトルの理論もチュートリアルに含まれているので、実際に動作させてみると理解が深まるでしょう。
Zelkova / Tiros
発表中に名前を挙げた Zelkova や Tiros のような、数学的なバックグラウンドに立脚した AWS のセキュリティ検証の取り組みは、Provable Security というくくりで特設サイトにまとめられています。
Zelkova に関連した記事はいくつかありますが、とりあえずのとっかかりとしてはこの記事から目を通すとよいです。
文章よりも動画が好きだ、という人は以下のふたつをどうぞ。前者はビジネス層向けにポップにまとめられ CMクリップ、後者は re:Inforce 2019 のフルセッションです。
冒頭にも挙げましたが、今回の発表の後半部分は以下の Zelkova の論文が元になっています。発表中に盛り込めなかった SMT エンコーディングのディティールや具体例も載っています。検索すれば PDF も見つかります。
まとめ
以上、簡単ですが July Tech Festa 2021 の登壇報告と、関連情報のリンクをまとめました。
AWS の検査エンジン Zelkova は、IAM Policy を SMT ソルバ用にエンコーディングすることで、実際のアクセスを伴わずに AWS リソースに対するアクセス権限の検査を行うことができます。またエンドユーザの立場では、IAM Access Analyzer を介して Zelkova に問い合わせることで、設定を変更する前にセキュリティ的な問題の有無を確認することが可能です。
今回は時間の都合もあって Zelkova をメインに据えましたが、Tiros も面白い技術です。SMT ソルバ（とその拡張）で完結している Zelkova と異なり、Tiros では SMT ソルバ MonoSAT 以外に、Datalog 互換のソルバ Soufflé と古典一階述語論理の証明器 Vampire を合わせた三種類を用途に応じて使い分けます。こちらも機会があれば是非どこかでお話ししたいのですが、それはまた別の話。
