(cache)JAWS DAYS 2018 で形式手法による IAM の検証について話してきました

だいぶ日が空いてしまって今更ですが、先日行われた JAWS DAYS 2018 で登壇してきました*1。モデル検査器 Alloy を使って AWS の IAM を検証してみるという内容です。

形式手法 × AWS というテーマではこれまでにもいくつかのイベントで発表していますが、題材はネットワーク関連の検証がメインでした。

ccvanishing.hateblo.jp

さすがに同じことばかり話していても芸がないので、今回は新ネタとして IAM を投入してみました。CFP も Security Slot で採択されています。

現状と既存手法の限界

IAM 設定の難しさ

いや、説明するまでもなく実際ややこしいですよね。一つ一つはさほど複雑ではないんですが、多数の設定項目が互いに影響し合うため最終的な影響を把握するのに神経を使います。

一例を挙げると、IAM には NotAction という記述方法があって、指定した「以外」のアクションについて制御をかけることができます。しかし「Action を指定して Allow」と「NotAction を指定して Deny」は字面は似ていても最終的に表れる効果が違っていたりして、しかもそんな設定が複数重複して作用するとなるとどう考えても混乱のもとです。会場で聞いた感じでも、完璧に活用されている現場はさほど多くないようでした。

それでも、日々の固定されたフローを回すだけなら何とかなります。問題はインフラの構成や運用をドラスティックに追加・変更する必要があるときです。既存のインフラに影響を与えないようにして新しい要素を導入しようとすると、ちょっと考えたくない程度に複雑になるというのは、経験者の皆様には同意して頂けるでしょう。

特にセキュリティ系は設定ミスが直接リアルなダメージにつながるため、他の部分より余計に気を使わざるを得ません。

Policy Simulator

さて、この複雑性を何とかするためのツールとして、既に公式から IAM Policy Simulator が提供されています。

リンク先を見てもらえばわかる通り、このツールは割とよくできていて、IAM のポリシが最終的にどういう影響を与えるか、実際に運用中の設定に影響を与えないよう確認することができるようになっています。

しかしこの Policy Simulator も完璧ではありません。特にここで指摘したいのは以下の 3 点です。

論理的な不整合が検出できない

Simulator が返してくるのは「指定したリソースに対して最終的にアクションが許可されるか否か」です。したがって、設定が論理的に矛盾していて無駄があるとき、より具体的には例えば

あるポリシに複数のステートメントが設定されていて、同じリソースに対してそれぞれが Allow と Deny を指定している
あるロールに複数のポリシが指定されていて、個々のポリシは問題なくてもポリシ間で矛盾している

といった状況では、Simulator は単に Deny を返すだけで矛盾を指摘することはできません。

一方、このような設定は少なくとも設計者が意図したものではないでしょう。ポリシやロールの数が少ないうちは明らかにおかしいことに気付くことができますが、運用が長期化するに従って複雑化、やがて既存の設定に手が付けられなくなりカオス化の原因になります。

仕様から設定を得ることができない

Simulator では「こう変えたら結果がどうなる」は確認できますが、逆ができません。つまり、アクセス制御の要件があるときにそれをどうやったら実現できるかは試行錯誤が必要で、結局のところ個人の経験とカンに基づいた作業になります。

これも問題になるのは既にある程度の規模で運用されている設定が多数あるときで、新しい要素を導入しようとすると、あっちを変えるとこっちが壊れる、みたいなループに陥って非常に疲れます。もうちょっとシステマティックに解決する方法が欲しいところです。

IAM 以外の要素を考慮できない

Simulator はあくまでも「IAM ポリシの評価器」なので、当然ですが IAM 以外の要素まで含めて確認することができません。

しかし実際のインフラ設計は IAM だけで完結するわけではなく、

このインスタンスは他の VPC にいるので直接通信できない
S3 へのアクセス経路がインタネット経由とエンドポイント経由の 2 種類ある
他システムとの連携の都合で CIDR によって通信の許可・不許可を切り替える必要がある

みたいな条件について（システムの本質か、あるいは政治的な妥協かはおいといて）考えざるを得なくなる場合は少なからず発生します。

今回の提案手法

このような、人間が直接整合性を把握するには困難な対象を扱う場合、形式手法、特にモデル検査が有効な手段になり得ます。

Alloy 以外のモデル検査器だと、SPIN/Promela や TLA+ が有名です。しかしこの両者はオートマトンをベースにしていて、（特に分散）アルゴリズムを検証する目的には便利ですが、今回のような設定の整合性の検証には向きません。

これに対して Alloy では関係論理を用いてモデルを記述するため、IAM の評価ルールをずっと自然な形でモデル化することが可能です。

Alloy による検証のメリット

Policy Simulator の不足点として上に挙げた 3 つのそれぞれに対して、Alloy を用いた検証は以下のようなアドバンテージを持ちます。

矛盾した設定の検出

モデル検査器の用途そのものです。Alloy では aseert で守られるべき条件記述して check で検査すると、自動的に全探索が行われて条件に違反する例を列挙・図示してくれます。

プレゼン中では「同じリソースに対して Allow と Deny が同時に指定されない」という条件を検査するサンプルを挙げました。

仕様からの設定の導出

Alloy に特徴的な機能ですが、pred で欲しい条件を記述して run で検査すると、assert とは逆にその条件を満たす具体例を出力してきます。Alloy が「モデル発見器 (model finder)」とも呼ばれる所以です。

実は内部的な仕組みは assert と共通していて、pred で指定された条件の否定を検査することで、もし具体例が存在すれば反例として検出されるようになっています。

プレゼン中では、同じ仕様に対して設定を自動的に探索させ、「Action を指定して Allow する」「NotAction を指定して Deny する」という二つのパターンを人の手に依らず発見するサンプルを挙げました。

IAM 以外の条件の記述

Alloy は簡単なモジュールシステムを持っていて、モデルを分割して記述・再利用することができます。

プレゼン中ではこれを利用して、

IAM ポリシの評価ロジック
S3 関連のリソース
EC2 関連のリソース

を別々に記述する方法をサンプルとして挙げました。

まとめ

以上、AWS の IAM 設定について、既存の Policy Simulator がカバーできない部分を Alloy で検証する、という内容をお話ししました。スライド中にはサンプルコードも挙げてあるので、このブログと合わせて読んでもらえればおおむね当日話した情報量と同程度になるかと思います。

ちなみに上に挙げた論点の内、モジュール化の部分は割と非自明です。いくつか方法は考えられるのですが、普通に書こうとするとロジックの重複が排除できずモジュール化の恩恵が得られないことがわかります。

このモジュール化の工夫についてはいずれ記事を改めて解説したいと思っていますが、それはまた別の話。

*1:所属がいつもの「ProofCafe」ではなく「非公開」になっているのは、単に連絡に行き違いがあったためです。

チェシャ猫の消滅定理

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

JAWS DAYS 2018 で形式手法による IAM の検証について話してきました