AWSセキュリティは「論理」に訊け！　Automated Reasoning の理論と実践

セキュリティ系の設定はAWSにデプロイする前にテストしたい

チェシャ猫氏（以下、チェシャ猫）：みなさん、おはようございます。チェシャ猫と申します。毎回出てきている人なのでご存知かとは思いますが、@y_taka_23という名前でTwitterをやっています。

今日の話なんですけれども、メインになるのは「Automated Reasoning」という、セキュリティに関する設定をどうやって検証するかというお話です。

まず、目次なんですけれども、AWSの上でセキュリティ設定をテストしたいという時に、いろいろとツールがあるんですが、みなさんが使っているようなツールと、IAM Access Analyzerというのがあります。この両者がどう違うのかを最初のテーマにしましょう。

2番目は、SATソルバとSMTソルバについてお話しします。自動化された推論をするために、要素技術としてこの2つのソルバが重要になります。ここを2つ目に解説しようと思います。

最後、今回のメイントピックとして、設定を検査するためのエンジンでZelkovaというのがありますので、こいつの中身についてお話ししたいと思います。

まず、そもそもAWS上のConfigurationをテストするにはどうするかという話をしましょう。

みなさん、たぶんセキュリティ系の設定のテストにわりと苦労されていると思うんです。というのは、セキュリティ系の設定は、設定にミスがあるとヤバイわけです。物理的にお金がかかったり、あるいはお客さまの信用を損なったりします。影響が大きいというのが1つです。

もう1つ、実際にアクセスしてみて、アクセスできるかどうかを試そうとすると、アクセスできた時にはすでに遅いんです。この2つがあるので、できればAWSにデプロイする前の設定ファイルの時点で確認したいというのが動機として強くあります。

既存のツールはいくつかあります。例えばCloudFormationについてテストするツールでいうと、ここに挙げているvalidate-templateコマンドであるとか、CFn Linterであるとか、あるいはCFn Guardというツールがあります。

3つに分けられるCloudFormationの検査水準

ここに3つ挙げたツールには1つ仲間外れがあるんです。使っているみなさんはたぶん直感的にわかると思います。仲間外れは、1番上です。なぜか？

これは若干私の私見を含むんですが、CloudFormationを検査する時のレベルみたいなものは、1、2、3に分けられるんじゃないかと思います。

一番ベーシックなパターンが、いわゆるSyntaxの検査。これが、validate-templateで検査できるやつです。テンプレートとして、文法がそもそも正しいかどうかを検査します。もちろんそれだけだと、デプロイして、なんかアクセスできないみたいなことが起こり得るので、その次のレベルとしてヒューリスティックな検査があります。

どういうものかというと、個別の項目を見ています。例えば0.0.0.0/0のパブリックなアクセスは書いちゃダメとか、あるいはアスタリスクを書いちゃダメであるとか、あるいは暗号化は必ずTrueじゃなきゃいけないみたいなルールです。

先ほどに挙げたツールはたぶん、ここのレベルまでだと思うんです。この上が今回お話ししたいところで、Level3として意味論的な検査があります。設定を入れた時に、複数の設定が最終的にからまって結果になるわけですが、その実際に発揮される効果の「意味」にまで踏み込んだ検査を、ここではLevel3と定義しましょう。

さて「意味」とは何か。あるいは「意味を検査するツール」はどんなのかというのが、気になるわけです。Level3に属するものは、果たして存在するのだろうかと。

過剰なアクセス権限をデプロイ前に検出してくれる「IAM Access Analyzer」

ここで、例として挙げたいのがIAM Access Analyzerです。どういう機能かといいますと、使っている方もいると思うんですが、外部のAWSアカウントであったり、パブリックのインターネットであったりからアクセス許可がされている時に、それを自動で発見してくれます。

S3や、あるいはIAM RoleやKMSや、そのほかのセキュリティ系の、外部からのアクセスがあるものに統合されています。

ここでお話ししているとおり、実際の適用前に検出できるんです。AWS Config Ruleをみなさんも使っていると思うんですが、あれは、現物がデプロイされた時にそれをテストしているんです。それとは違って、適用する前に検出が可能です。

さらに、さっきお伝えしたようにLevel3の検証ができるというのが、Access Analyzerの特徴です。

S3のバケットに、ソースIPのCIDRを2つ付けるんですけれども、AllowとDenyで同じ値を指定すると、Denyが勝つわけです。さらに、サブネットのオーバーラップによってDenyのほうが広いと、結局最終的にはDenyじゃないですか。

でも、これってよく考えると奇妙で、サブネットまで含めて値が違うんです。あくまでも、オーバーラップしているから被して消せるだけで、いわゆるStringのイコールではないことがわかります。これが、意味まで踏み込んだ検査です。

つまり実際にサブネットを指定した時に、それがどういう効果を持つのかをAccess Analyzerは知識として知ってるわけです。

AWSセキュリティの設定として、実際にデプロイを行う前に仕切りたいですよね。現物じゃなくて設定そのものを検査したいと思います。そういうことを考えた時に、どこまで検査できるのか、どこまで検査したいのかを考えると、水準としてLevel1、2、3というのがあります。私の考えで、ここで定義しました。

一番下が、構文的にOKかどうか。真ん中が、よくある設定項目を見ていって、この設定項目は不味かろうと検出するやつ。一番強いのが、意味論的な検査です。今回お話ししたいIAM Access Analyzerは、意味論まで踏み込んだ検査が可能です。

Policyを適用した時に、実際にどういう影響が出るかを考えて、どう評価されるかという、中のロジックを知識として持っています。そういう意味論的な検査が可能なのが、今回紹介しているIAM Access Analyzerです。

この意味論的な検査を、実際にアクセスするんじゃなくて、設定ファイルから推測させること。これが、今回のタイトルに挙げたAutomated Reasoningです。

命題論理式の充足可能性を判定する「SATソルバ」

それでは、このAutomated Reasoningを具体的にどうやって実現するかを第2章としてお話ししましょう。

要素技術として重要になるのは、SATソルバ、およびSMTソルバと呼ばれるツールです。どういうものかというと、SATソルバのSATは、SATisfiability、いわゆる充足が可能かどうかという充足可能性から来ています。

何ができるかというと、Booleanからできているようなブール式、論理演算でできているような式について、変数にtrue、falseをうまく割り当てると、全体で成り立つかどうか、そういう組み合わせがあるかどうかを見つけてくれます。

ここに2つ、例1と例2を挙げました。pとqがある原子命題です。pとqにうまくtrue、falseを当てて文全体がtrueになるかというと、例1は、p = true、q = falseとすると、全体として評価された時にtrueになりますが、例2は、例1の答えに、もう1個打ち消す条件が付け加わっているので、どういう組み合わせでやっても、全体はtrueにはなりません。このように充足可能、あるいは充足不可能であるというのを当ててくれるのが、SATソルバです。

「SATソルバ」で足りない部分を補う「SMTソルバ」

ただ、SATソルバだけだと、ちょっと力が足りんのです。そこで、SMTソルバというのを、併わせて使います。SMTは、Satisfiability Modulo Theoriesの略です。SATソルバは今言ったように命題論理しか扱えないので、true、falseの組み合わせで書くと、問題によっては式がメチャクチャたくさんになります。もちろん、書けないこともあります。

仮に書けたとしても、元の解きたい問題はtrue、falseよりももっと豊かな構造を持っている可能性が高いわけです。

例えば、ここで例に挙げた、aがbより小さくて、bがcより小さいなら、推移律があるので、aはcより小さいですね。というのは、算術のいわゆる不等号の意味を知らないとわからない推論なので、SATソルバだとちょっと力不足です。

ここを埋めるために、SMTソルバは特定領域の理論に関する推論を、別途くっつけています。

いろいろあるんですが、ここで例に挙げたやつでいうと、例えば整数の算術（不等号、プラス、マイナス）や、文字列、正規表現の操作、あるいはビット演算もできます。

特定理論は、この別途実装された部分が解いていて、残った純粋な論理の部分をSATソルバに投げるというように、お互いに組み合わさって、解の可能性の範囲を絞っていくというのが、SMTソルバの動作原理です。

SMTソルバは、例えば算術の不等号であるとか、あるいは文字列の操作みたいなものが、Satisfiableかどうかを当ててくれます。

AWSにおけるSMTソルバの利用　その1「Zelkova」

AWSにおけるSMTソルバが、どうやって具体的に利用されているか、ここでは2つの例を挙げたいと思います。

1個目はZelkovaです。Zelkovaはどういうものかというと、アクセス制御に関する質問に答えてくれます。例えば、S3オブジェクトがあったとしましょう。ほかのAWSアカウントから読み取り可能であるかどうかを聞くと、「はい」「いいえ」みたいなのが返ってきます。

Access Analyzerの話の時に言いましたが、実際のアクセスを行うわけではなくて、今どういう設定になっているか、今どういう設定でアプライされようとしているかという2つから推論して、質問に対する答えを返してくれるのがZelkovaの機能です。

バックエンドのSMTソルバは、Z3というのを使っています。Microsoft Researchがもともと開発して、今はOSSになっているソルバです。

どういうものかというと、AWS独自の最適化が正規表現周りに入っていて、これをZ3Automataと呼びます。なぜこれがいるかというと、もともとのZ3の文字列の操作は、このZelkovaが必要とするよりも広い範囲のものを使っていて、より一般な問題が解ける代わりに、特定の時に遅くなるので、そこを切って最適化しているのがZ3Automataです。

先ほど挙げたAccess Analyzerのほかにも、ここに挙げたようなConfigであるとか、あるいはMacieとかGuardDutyとか、いろいろなセキュリティ系の機能に統合されています。

AWSにおけるSMTソルバの利用　その2「Tiros」

もう1つは、Tirosです。こいつは、ネットワークに関するクエリに答えてくれます。例えば、EC2インスタンスA、Bがあった時に、お互いSSHでログインできるかとかですね。

こいつもLevel3の水準を持っていて、実際のパケットは送出せずに、設定のみから推論できます。こちらはZ3ではなくて、グラフに関する理論を使いたいので、MonoSATというのを使っています。SATとついているんですけど、こいつはSMTソルバです。

身近なところだと、VPC Reachability Analyzerという、つながれているかどうか、どこでパケットが落ちてるかを調べてくれる機能があって、こいつのバックエンドとして使われています。

さて、Sectionの2では、SATソルバとSMTソルバについてお話ししました。SATソルバがどういうものだったかというと、充足可能性をうまい組み合わせで答え、全体としてシャンシャンになるかどうかを調べてくれるんですが、SATソルバのみだと力不足なので、理論を知っているソルバを個別に実装して、必要なところはそっちにアウトソースするという仕組みでSMTソルバは動いています。

AWSの中でも、SMTソルバベースの検査器を開発、あるいは利用していてサービスにたくさん統合されていることがすでにわかっています。具体的な例として挙げたのは、ZelkovaとTirosで、Zelkovaはリソースへのアクセス権限の検査、Tirosはネットワーク設定の検査を行ってくれます。

Zelkovaの新規性はIAM Policyそのものを検査できること

今回は、1番目のZelkovaについて、Section3でお話ししようと思います。

さて、Section3です。Section3では、いかにしてPolicyを表現するかというお話をしましょう。ここでお話しする内容は、元の論文があって、Zelkovaについて書かれてるやつです。「Semantic-based Automated Reasoning for AWS Access Policies using SMT」と言うタイトルです。

まさにこのタイトルの言っているとおりで、AWSのアクセスポリシーについて、SMTソルバを使って自動で推論しましょうと。どういうことかと言うと、Semantic、いわゆるLevel3の意味論的な検証である、というタイトルがついています。これに沿ってお話ししたいと思います。

Zelkovaの今タイトルを挙げた論文の概要は、以下です。まず、この論文の新規性がどこにあるかというと、従来の我々が知っているIAM Policy文法を検査できるという点です。なぜならば、これより先に出ている研究は「Policyを記述するためのDSLフレームワークを開発しました。それが検査できます」みたいなものばかりだからです。

それとは違って、ZelkovaはIAM Policyそのものを検査できるようになっているのが新規性です。

そして、実際にAWSにおける利用実態についても述べられています。半分、事例論文みたいな感じです。

稼働はLambda Functionとして動いていて、JSON APIを内部に提供してます。どれぐらい使われているかというと、1日あたり数百万から数千万回クエリが飛んでるというオーダーです。99パーセンタイルは160msで応答するので、かなり速いと言えるでしょう。

ZelkovaによるIAM Policyのエンコードと検査

何をしなきゃいけないかというと、IAM Policyの意味を、SMTソルバ向けに変換して食わせます。どういうエンコードをするかというと、まずリクエストを送る時に、PrincipalとActionとResourceの組が送られてきます。それが許可されることを論理式で表現すると、Allow Statementsが合致していて、Deny Statementsがどれも合致しないという条件になります。

さらに、それぞれのStatementに合致するという部分を書こうとすると、PrincipalsとActionsとResourcesと、あとはConditionsに全部合っているとなります。

Conditionsに合っているのは、OperationとKeyとValueがあった時に、そのOperationが全部&&で結ばれていて、全部満たしているものがStatementに合致していることになります。これで論理式になります。

また、いくつか特殊な書き方があって、ワイルドカードの場合は文字列の操作になります。例えばここは、foo*/*barになってますが、これはprefixOfとcontainsとsurfixOfで書けます。必要な場合は、正規表現も使うようになっています。

先ほどは見せられなかったんですが、デモの中では最大の範囲をマスクされているというものがありました。どういう風にやっているかというと、ビット演算の理論、SMTソルバの理論を使っています。

本当にサブネットマスクなので、サブネットマスクをビットワイズでANDすると、サブネットのマスクで隠された部分が消えます。それとイコールを取れば、実際の条件が抽出できるという仕組みになっています。

さて、これを使って検査する時にどうするかというと、Zelkovaが判定するのはPolicyの強弱です。XとYがあった時に、Xで許可される時、常にYが許可される、Yでも許可されるということができれば、Xの方がYより厳しいわけです。この関係を論文では、less-or-eqully-permissive、つまり、なになに以下の許容度であるという言い方をします。

実際には、デプロイしたい対象をXとして、ガードレールをYにします。もし、反例が充足されてしまうということがあれば、それはYが許可してないのにXが許可してしまう例があるということです。これは要するに、Policyの違反になります。

数学的な理論を使ってAWS環境のセキュリティを「証明可能」にしてみよう

さて、Section3のまとめです。Section3では、Zelkovaについてお話ししました。独自のDSLを定義するんじゃなくて、従来のIAM Policyを検査できるところに売りがあります。そのためには、バックエンドのSMTソルバを、Z3に与えられる形式に変換する必要があるんですが、ワイルドカードとCIDRは、Z3が知っている理論ソルバに投げられるかたちに変換できます。

実際にSMTソルバを使って検査すると、反例が探索されます。具体例が探索できるわけです。ガードレールより厳しいことを確認できれば、これはOKだということになります。よろしいでしょうか。

最後にまとめにいきましょう。本日のまとめです。セキュリティ系の設定の検査は、デプロイ前に、実際にデプロイしたらどうなるかというディープな意味、ここでいうLevel3まで考えて検査したいですね。

それをやるために、AWSではSMTソルバを使って、充足可能性を判定しています。具体的にフロントエンドには、検査エンジンのZelkovaがあって、IAM Policyの意味論をSMTソルバに食わせるようにエンコードできるというのを使って、AWSの内部では、Policyの強弱関係について検証しています。

さて、ここでお話ししたような数学的な理論を使って、あなたのAWS環境のセキュリティをProvable、つまり「証明可能」にしてみてはいかがでしょうか。以上、チェシャ猫がお送りしました。ありがとうございました。

参考資料