事前に問題を検出できる仕組み　SATソルバとSMTソルバによる充足可能性判定

SATソルバについて

チェシャ猫氏：そのために出てくる要素技術が、SATソルバとSMTソルバです。SATソルバとSMTソルバの一般論について、VPC Reachability Analyzerからいったん離れて、理論的なというか、ソルバとはなにかという話を少しします。知っている方はおさらいだと思って、聞き流してもらえればけっこうです。

SATソルバのSATはSATisfiability、充足可能性を意味しています。どういうものかというと、命題論理の充足可能性を検査します、ということです。

充足可能性が何かというと、何か変数がある時に、それぞれに真または偽を割り当てます。その時に、全体として見て真になるかどうか、そういう割り当てがあるかどうかを当ててくれるのがSATソルバです。

（スライドを示して）例を2つ挙げたので、見てみましょう。まず例1は、PまたはQと、PまたはnotQと、notPまたはnotQを「且つ」で結んでいるものです。こういう論理式をSATソルバに投げると、答えは「充足可能です」と返ってきます。

実際にどういう割り当てがあるかというと、PはTrueでQはFalseとすると、式全体は真になります。しかも、これが唯一の解であることがわかります。

例2として、もう少し長く、もう1つ「且つ」をつけたものを考えましょう。これを投げると、SATソルバは「充足不可能です」「どうやってP、Qとの真偽を決めても、全体としては成り立ちません」と返してくるわけです。これがSATソルバです。もう1つのSMTソルバは、これの発展形みたいなものです。

どういうものかというと、SATソルバはいわゆる命題論理しか扱えません。ただ、実際の世の中の問題を解きたい時、工学的な問題は必ずしも命題論理で書けないし、あるいは直接翻訳すると、問題のサイズが非常に大きく、式のサイズがメチャクチャ大きくなりがちです。

さらに、解くのもとても非効率になります。なぜなら、もともとの問題が持っているドメイン知識を使えないからです。（スライドを示して）ここで例に挙げたのは、不等式の推移性です。どういうことかというと、例えばBがAより大きくて、CがBより大きい。つまり、ABCの順番で大小が並んでいたとします。

そうすると、整数の不等式について意味を知っている人やドメイン知識を持っている人であれば、両側の不等号から、「Aは一番小さいからAはCよりも小さい」というのがわかるはずです。

ただ、命題論理はこれを使えないので、問題を解くこと自体がものすごく手間になり、実際には解けないものが多く、効率的ではないのがSATソルバです。

SMTソルバについて

ここを克服するのがSMTソルバで、特定ドメインの理論ソルバ、ドメイン知識を持っているソルバを別途実装して組み合わせます。

組み合わせるものは何かというと、今までで出てきたのは整数の線形算術、つまりプラス、マイナス、不等号みたいなものです。その他にも、例えば文字列の理論があります。あるいはビットベクトル、つまり、ビット列のビットワイズの演算について特定の知識を持っていて、そこの計算ができるとか、ビット同士の不等号なり演算ができるようなソルバもあります。

SMTソルバはいくつかありますが、それぞれによって何を理論ソルバとして知っているかは違っていて、それぞれ自分が好きなものを組み込んであるのを、SATソルバと組み合わせて問題を解きます。

特定のドメインの部分は理論ソルバが解いて、「且つ」または「not」のような論理の部分はSATソルバが担当する、という全体の仕組みがSMTソルバです。

“組み合わせ”といっていますが、これがどのように動いているのかを図解してみます。（スライドを示して）まず、整数の算術の例を1つ挙げます。ここでいっているのはX、Y、Zの間に関係式が3つ成り立つというものです。

SATソルバは、整数の計算について知らないので解けないわけですが、SMTソルバは中に理論ソルバを持っていて「充足可能です。例えばX、Y、Z、こうやって置いたら式は成り立ちます」という答えを返してきます。

文字列の理論でも同じことです。何かstrに後ろからbをつけたものと、前からaをつけたようなものが一致する、そのようなstrというのは可能性があるかどうかと聞くと、SMTソルバは「可能性ないです」「これはどうやって取っても充足不可能です」と返してきます。

人間が見ると、この式はほぼ自明です。なぜならば、strの先頭にaがいくつかあるということを考えると、必ず右辺のaが1個増えるので、絶対に合わないわけです。ただこれは我々が文字列の性質を知っているからで、それを理論ソルバとして組み込んであるのがSMTソルバだという話です。

どうやって組み合わせるのか？

もう少し具体的に組み合わせの動かし方、作動の機序について見ていきましょう。（スライドを指して）さて、こんな問題があったとします。先ほど算術の話をしましたが、その一種です。算術式が論理式の中に含まれてるようなものです。

元の問題をSMTソルバに食わせる時に、個別の数式の部分だけ論理命題に置き換えます。原子（アトム）というのですが、このBooleanの変数に置き換えます。これをBoolean Abstractionといいます。置き換えをするとP、Q、R、Sの式になるわけです。これで論理だけの話になったので、SATソルバで解くことができます。

複数P、Q、R、Sの真偽の組み合わせはあり得ますが、例えばSATソルバが「充足可能です。例えばこれ」と言って、全部Trueのものを返してきたとします。

そうすると、Refinementと言いますが、これを理論ソルバ側に戻します。この式をじっと見るとわかるのですが、実は充足不可能です。不可能だというのは、P、Q、R、SはただのBooleanなので、SATソルバは知らなかったわけです。理論ソルバのほうにきて初めて、数式、算術について知るので「これは駄目だ」ということがわかります。

駄目だとわかったら「その割り当ては駄目です」ということをSAT側に戻します。これを学習、Learningといいます。P、Q、R、Sが全部真では駄目だとわかった。

それを「notの且つ」ということを制約としてもう1回追加してSATソルバに解かせると、今度は解けて、先ほどのものは駄目なので、新しい解としてPがFalseになったやつが返ってきます。

もう1回Refinementすると、今度は、X、Y、Zは全部ゼロだということで、もともと解きたい問題が解けます。この組み合わせ、この流れ、回転が、SMTソルバのSATソルバ部分と理論ソルバ部分の連携の大まかな仕組みです。

Lazy SMT（Online Instergration）

今話したのは、SATソルバが解いて、True／Falseを全部決めてからRefinementで理論ソルバに投げるように解説しましたが、実際のモダンなソルバはそうではなくて、もう少し最適化が入っています。

いわゆるLazyとか、あるいはオンラインインテグレーションと呼ばれるもので、SATソルバの動作の途中でも、理論ソルバを呼ぶような仕組みが入っています。

具体的にどんなところで最適化が入っているかというと、ここでは大きく2つ挙げましたが、1つは制約の伝播です。Propagationというもので、理論ソルバの知識も使って、SAT側の論理式を単純化できます。

例えば、先ほど言った「整数の不等号には推移性があります」のようなものです。そうすると、もともとなかった新しい式、「AはCより小さい」という大小関係が手に入るので、それを使うことで、あらかじめあり得ない選択肢が素早く枝刈りできるわけです。

もう1つは節学習で、先ほどは充足不可能だった時にP、Q、R、Sの全部の「not」をとりあえず追加しましょうという話をしましたが、例えばPとQだけですでに矛盾することがわかっていれば、それを学習させるともっと効率がいいわけです。

もっとピンポイントな情報が手に入るので、SMTソルバの理論部分を使って、SATソルバにアルゴリズムを最適化することが実際には行われます。

SMTソルバはAWSのどこで使われているのか？

さて、ここまでSMTソルバについて話してきましたが、AWSのどこで使われているのかを、ここでは例を2つ挙げます。

1つ目は、今回お話しするもので、Tirosです。これはネットワークの設定に関するクエリに答えるためのエンジンです。例えば、最初に図として挙げていたサンプルで、「EC2インスタンスにAからBにSSH接続できますか」というようなクエリをTirosに与えると「現在の設定だと無理です」というのが返ってくるわけです。

VPC Reachability Analyzerの話をした時に「実際のパケットは送出せず」と言いましたが、それはTirosの持っているこの性質からきています。Tirosも実際のパケットを送出することなく、設定のみから推論できます。

これには2点うれしいところがあります。1点目は、ヘビーに使っても帯域を食い潰さないところです。つまり、ネットワークに実際にアプライすることなく、手元でオフラインソルバのように使えるので、実際のプロダクション環境において影響を与えません。

もう1つはシフトレフトといわれるもので、テストをできるだけ手前の段階でやろう、という考え方です。特にTiros、ネットワークの場合はセキュリティの問題があって、例えば不用意にインターネットからサーバーが到達可能になってしまうというのは、一瞬であっても避けたいわけです。

そういうことを考えると、実際にデプロイしてみてから「穴が空いてました」というのはまずいので「デプロイする前に設定から推論したい」というのが動機としてあります。

実際にいくつかのサービスのバックエンドとして、AWSの中でTirosは稼働しています。1つは、今回話しているVPC Reachability Analyzerです。もう1つは、先ほどセキュリティの話をしましたが、Amazon Inspectorのバックエンドとしても使われています。つまり、外部からのネットワーク的な危殆化を検出できる仕組みです。（補足：本講演の後、2021年12月にVPC Network Access Analyzerの提供も開始されました）

一般のユーザーに対して提供されているのは、こういうサービスを介してしかアクセスできません。しかしTirosそのものは、実は一部の特殊なユーザーにはAPIを直接提供していて、Tirosそのものとインテグレーションされたようなソリューションを提供している会社についても知られています。これが1つ目です。

もう1つは、Zelkovaというエンジンです。どういうものかというと、アクセス制御に関するクエリに答えられます。例えばS3オブジェクトがあって、実はリソースポリシーの書き方がおかしくて「外部の他のAWSアカウントから読める状態になっていました」「実は全世界公開でした」という状態になっているとまずいです。

これもTirosと同じように、Zelkovaは実際のアクセスは行わず、設定のみから推論を行えます。なぜかというと、先ほどもセキュリティの話をしましたがこれも同じで、デプロイしてみて読み取り可能かどうか確認したら「読み取り可能でした」というのはまずい。そうなる前、デプロイする前に設定のみから推論したいというのが動機としてあります。

こちらのZelkovaも、Tirosと同じようにセキュリティ系のサービスにすでに統合されていて、実はかなりいろいろなところに統合されています。例えばIAM Access AnalyzerやAWS Config、Macieなど、他にもいくつかあります。GuardDutyもそうです。

こちらについても論文が出ていますが、それによると、内部的にはLambda Functionとして稼働しています。（スライドを示して）ここに挙げたような、例えばIAMなどからZelkovaのLambda Functionを叩いて、S3のパブリックブロックが効いてるかどうかを自動的に確認してくれるわけです。

これが2つ目のZelkovaです。今日はTirosについて話すので、Zelkovaについては詳しくやりません。

Zelkovaについては「CI/CD Conference 2021」で詳しく論文まで含めて解説しました。あまりふだん表に見ることはない、日本語で見ることはない情報だと思うので、もしよろしければ興味のある方はご覧ください。

セクション2のまとめ

さて、セクション2のまとめです。セクション2では、SATソルバとSMTソルバの仕組みについて簡単に解説しました。SMTソルバは充足可能性を判定してくれます。SATソルバと何が違うかというと、現実の問題に対してSATソルバは命題論理しか扱えない。つまり、論理演算子しか扱えないので、表現力が足りないわけです。

例えば、不等号が2つあったとしても、それを組み合わせて新しい事実を推論することはできません。ぜんぜん中身を知らないわけです。

それを強引に、具体的な問題に対して使おうとすると明らかに遅いので、SMTソルバは個別のドメイン専用に理論ソルバを作って、それを組み合わせてお互いに呼び合うことを通して推論を効率化します。

例えば、整数の不等号や文字列、ビットベクトルなど、そういう個々の理論ソルバがある、という話をしました。AWSでもSMTソルバベースの検査機能を提供しています。具体的には今回話すTirosで、これはネットワークに関する検査を行えるものです。もう1つはZelkovaで、これはアクセス制御に関する検査を行えます。

いずれも、実際にアクセスしてみるのではなく、あくまで設定の情報から推論して結果を導くところに動作の特徴があり、それはセキュリティ的に、事前に問題があれば検出できるのがうれしい、というものです。これがセクション2で話したことです。

（次回に続く）