AWS Summit Tokyo 2016 で形式手法について話してきました
先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。
www.slideshare.net
モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT で、昨年 12 月の NGK2015B でも同じテーマについて話しています。よければ以下の記事も合わせてお読みください。
NGK2015B の発表ではサンプルコードの紹介に比較的時間を割いているのに対して、今回の発表では「動機」の部分によりウェイトを置いた構成になっています。
なぜ形式手法なのか？
今回のテーマを一言でまとめると以下のようになります。
インフラ構成が「秘伝のタレ」と化すのをどう防ぐべきか？
ある程度の規模のインフラを長期間運用していると、どうしても初期の想定が変質してくることは避け得ません。アプリ側の要件が変わったりして、インフラ側がアドホックな対応を迫られるケースも（本来望ましくないですが）一定の割合で生じるものです。また、担当者が代替わりして暗黙知がうまく引き継がれない状況もあるでしょう。
必然的にカオスの縁にいる我々は、どうやってこの状況に対抗すべきでしょう？ アプリ開発であればきっと「単体テスト書こうぜ！」みたいな流れになるわけですが、さてインフラを検証したい場合にどんな手段が取れるのか？
awspec
「AWS + テスト」というキーワードで真っ先に思い出すのはおそらく awspec ではないかと思います。
awspec は servespec に着想を得たツールで、RSpec を利用して AWS リソースをテストできるようになっています。また、人間が直接 spec を記述するだけでなく、現に存在するリソースから awspec generate コマンドを使ってテストケースを自動生成することも可能です。
しかし、すでに存在するリソースをテストするという性質上、設計を考える段階での試行錯誤にはあまり向いていません。また、何かを変更しようとした際にそれをあらかじめ検証するという用途も難しいでしょう。好き好んで Amazon にお布施をしたい人は別として、テストそれ自体に掛かるコスト面も大きな問題です。
IAM Policy Simulator
さて、翻って他の方法を考えてみると、IAM のアクセス権限については、公式がシミュレータを提供してくれています。
実際の操作を行わなくとも dry run で検証できる、というのが大きなメリットで、例えば「削除」の権限をテストするのに実際の削除は発生しません。これがあれば、少なくとも IAM のアクセスポリシーを設定する際には、心ゆくまで試行錯誤ができそうです。
しかし（当たり前ですが）この機能は IAM 限定。となると、以下のような疑問が自然に生じます。
「現物」がなくても検証できる、汎用的な手法はないか？
この疑問への答えとして、現物ではなく形式化したモデルを検証することで有益な結果が得られるのではないか、というのが今回の発表の主題です。
形式手法とその限界
形式手法とは、システムの静的解析の中でも特に
- システムの仕様を数学的に厳密に記述する
- その正しさをやはり数学的に保証する
という特徴を持つ一連の手法を指して使われる用語です。現物と離れたところで堅く検証を行う、という意味では今回の目的にはピッタリです。
しかし如何せん、形式手法はコストがかかります。そもそも形式手法が扱える人間が少ないことに加え、大抵のツールでは従来のテストよりもずっと多くの工数が必要になります。そのため実際の形式手法の導入は、そのコストを支払ってもお釣りがくるほど高信頼性が求められる案件に限られているのが現状です。
今回の場合、どの程度ならコストとメリットが釣り合うのかはよく考える必要があります。形式手法を採用するのは手段であって目的ではないわけで、そこに必要以上に時間をかけるのはどう考えても本末転倒です。
このジレンマをなんとかするために登場するツールが Alloy Analyzer です。
アンチテーゼとしての Alloy
Alloy では関係論理を利用してシステムのモデルを定義し、さらにそこに検査したい制約を加えたものを充足可能性問題に変換することで、SAT ソルバを利用して条件を満たす例・満たさない例を全探索します。モデルの定義や制約の記述にはやや慣れが必要ですが、他のツールと異なり検証作業自体は自動化されており、上で述べたコストの問題はある程度クリアできます。
手軽に使用できる反面、当然ある種の欠点もあります。テストと比較して形式手法を語る際、メリットとしてよく「テストは有限個のケースしか検証できない。形式手法では無限個の入力に対して正しさを保証できる」という言い回しがなされることがありますが、Alloy についてこれは成り立ちません。
全探索を行うことからもわかる通り、Alloy による検証では、モデル中の要素の個数を制限する必要があります。この制限は例えば今回であれば「セキュリティーグループが 3 個以下の場合」のような但し書きとして現れます。
実は Alloy の背景には「仕様バグは小さなモデルで十分再現できる」という哲学があります。つまり、セキュリティグループが 10 個以上の場合に初めて現れる問題はそうそうないだろう、というわけです。この哲学は 小スコープ仮説 (small scope hypothesis) と呼ばれており、ある種の割り切りによって支えられています。
おわりに
今回の発表では、インフラの検証に形式手法が使えること、およびそのためのツールとして Alloy Analyzer を紹介しました。Alloy に興味を持った人は、以前の記事でも紹介していますが、以下の参考書が鉄板です。
ちなみに余談ですが、実は（AWS を利用する側ではなく）AWS そのものの設計にも形式手法が利用されています。しかも、形式手法を導入するにあたって Alloy が検討されていたにもかかわらず、結果的には要件に合わずに TLA+ という別のツールが採用されるという経緯を辿っています。
この辺り、ツールの特性の比較などと絡めて考えると面白い話題でもあるのですが、それはまた別の話。
