趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう？ と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。
形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジックに基づいている。その中でも厳密な仕様定義を求める方向と自動検証を求める方向とあるらしいが、Alloy はその後者に位置づけられ、軽量形式手法と呼ばれるもののひとつだということらしい。Alloy はモデリングのための言語および実行環境で、以下のホームページから入手できる。
インターネット上にチュートリアルやマニュアルもあるが、作者による教科書の邦訳が出ていて、これで勉強してみた。
- 作者:Daniel Jackson
- 発売日: 2011/07/15
- メディア: 単行本（ソフトカバー）
Halmos の握手問題
Alloy でどんな風に仕様を記述するのか、簡単な例で紹介する。ちなみにここで全ての重要な機能が解説できているわけではないので注意。
教科書の付録の練習問題として収録されているもの。
5組のカップルが参加したパーティーで、Alice が自分以外の9人に何人と握手したか尋ねると、全員から違う答えが返ってきた。自分自身と握手した人や自分のパートナーと握手した人がいないとすると、Alice のパートナー Bob は何人と握手しただろうか？
という問題。もともとは頭で解くパズルらしいけど、これを Alloy を使って解いてみる。流れとしてはこの状況を表すモデル（オブジェクトと制約）を記述し、それを満たすインスタンスを Alloy に発見してもらう。
全ソースはこちら。
まずは人間を表すシグネチャ Person を定義する。
sig Person {
partner: Person,
shaken: set Person
}
Alloy ではオブジェクトの集合はシグネチャと呼ばれる。シグネチャの宣言は、ある集合と、それにまつわる関係や制約を含む。まずはオブジェクト指向におけるクラスみたいなものだと捉えても問題ない。中括弧の中には Person のフィールドとして partner（パートナー）、shaken（握手をした相手） を宣言している。ある人のパートナーは一人の人間であり、握手をした相手は人間の集合（set）、と定義できる。
このフィールドもまたオブジェクト指向におけるクラスのメンバと考えられるが、面白いのはこれは本質的に Person に属するものではなく、シグネチャ同士の関係として定義される、ということだ。ここでいう関係は、関係データベース（リレーショナルデータベース、RDB）の関係。表とか、タプルの集合をイメージすればよい。フィールドの宣言は関係の宣言であって、partner や shaken は Person に属するわけではないトップレベルの関係として宣言される。
また、partner と shaken はどちらも Person の二項関係であって、shaken における set という多重度キーワードは、ひとつの Person に複数の Person が shaken 関係として対応しうることを表している。RDB で例えるなら、スキーマは同じだがユニーク制約が違うという状況になる。
関係が常に満たす制約は fact キーワードで宣言する。パートナーの関係が対称的であること、自分自身をパートナーにはできないことは、以下のように書ける。
fact partnerProperties {
partner = ~partner
no p: Person | p in p.partner
}
ここで特に ~ という記号は、関係の転置を表している。A shaken B ならば常に B shaken A だ。こんなふうに、partner という関係を Person を介さず直接参照することができる。
続いて、アリスとボブを人間の部分集合として宣言する。one キーワードは、宣言した集合の要素がただ一つであることを示す。
one sig Alice, Bob extends Person {}
fact { Alice -> Bob in partner }
アリスとボブがパートナーであることを宣言するために、partner 関係に Alice と Bob の組が含まれていることを（無名の） fact として記述している。
shaken 関係について、shaken 関係が対称的である（握手をするとき、自分もまた握手されている）こと、自分自身とは握手できないこと、パートナーとは握手しないことを制約として与える。
fact shakenProperties {
shaken = ~shaken
no p: Person | p in p.shaken
no p: Person | p.partner in p.shaken
}
ちなみに制約の書き方はひとつではなく、自分自身と握手できないことは
fact { all p: Person | p not in p.shaken }
とか
fact { no shaken & iden }
とか書ける（iden は恒等関係を表す定数）。
この問題の最後の制約として、Alice 以外の参加者が握手した相手の数は互い異なることを宣言する。# は関係の濃度を返す演算子。
fact numShakenPeopleMutuallyDiffer {
all disj p, p': Person - Alice {
#p.shaken != #p'.shaken
}
}
これでモデルの定義は完了。最後に、参加者が 10 人いる状況下でこのモデルの制約を満たすインスタンスが存在するかどうかをチェックする。
pred show {}
run show for exactly 10 Person
run コマンドは与えられた述語を満たすインスタンスを探しだす。ここで指定している述語 show は本体が空なので、これまでに fact として記述された制約だけが適用される。また、run コマンドはスコープの指定を受けとり、探しだすインスタンスのサイズはこのスコープに限られたものとなる。ここでは Person のインスタンスがちょうど 10 であると指定している。
Alloy は制約を満たすインスタンスを発見すると、それをグラフィカルに提示してくれる。そこで得られるのがこちら。
あとは Bob から生えている shaken 関係の辺の数を数えればよい。答えは 4 である。
仕組み
Alloy 自体には問題を解く（充足例や反例を探しだす）機能は実はない。Alloy はユーザの与えた関係と制約からなるモデルから命題論理の式を生成し、外部の SAT ソルバに渡している。Alloy の仕事は、論理式の生成と最適化だ。
インスタンス発見を現実的にするために、Alloy はスコープとしてインスタンスのサイズに制限を与える。先ほどの例ならちょうど 10 の Person だった。このスコープの外に充足例や反例があればもちろんそれは発見できないわけだが、Alloy の作者は「小スコープ仮説」というものを敷いていて、つまり「ほとんどのバグは小さな反例を持つ」という仮説のもとモデリングと検証を行うという思想だ。リーズナブルなトレードオフなんだろうと感じた。
OAuth 2.0 のフローをモデリングする
で、もともとウェブの認証／認可フローを検証したかったわけなので、馴染みのある OAuth 2.0 のフローをモデリングしてみる。……してみたかったわけだけど、どこまで抽象化するというのが難しい。変に抽象度を高めてしまうとその中に暗黙の仮定が入ってしまい、Alloy によって見つけたかったプロトコルの瑕疵が隠れてしまうことも考えられる。結局今回は Authorization Code Grant （よくあるサーバサイドのフロー）において state パラメータがないと、正しくリソースの認可が行えないことを目標にして、簡単のためにかなりの仮定をおいた。
- OAuth 2.0 の Authorization Code Grant だけを考える
- URL に含まれるパラメータのやり取りはセキュアに行われるものとして、改竄や漏洩はないものとする
- redirect_uri はモデリングしない
- アクセストークンもモデリングしない（リソースオーナと同一視する）
- 認可サーバとリソースサーバを同一視する
- ユーザのログイン／ログアウトフローは取り扱わない
などなど。目指す反例もわかっているので、進めやすくはあった。
全ソースは https://github.com/motemen/alloy-sketches/tree/master/oauth2 にあるので、かいつまんで説明する。
今回は時間にともなう状態の変化があるので、時刻を示すシグネチャを宣言する。
open util/ordering[Time]
sig Time {}
util/ordering という特別に最適化された標準モジュールを使って、Time に全順序を導入している。これで next: Time -> Time といった関係が使えるようになる。また、インスタンスを視覚化した際に時刻ごとに別のグラフとして描画し、順を追って見ていくことができる。
認可サーバ（OAuth プロバイダ）はこんな感じにした。登録済みのクライアント（OAuth コンシューマ）およびログイン中のリソースオーナ（ユーザ）は時刻によって変わらないものとした。クライアントに対して発行したコードは時刻によって変化するので Time を含む関係とする。矢印の前後に one や lone とあるのは関係の多重度を表していて、たとえば knownResourceOwners 関係は、ひとつの UserAgent に高々ひとつの ResourceOwner を対応させる。
sig AuthorizationServer {
knownClients: ClientId one -> one Client, // 登録済みのクライアント
knownResourceOwners: UserAgent -> lone ResourceOwner, // ログイン中のリソースオーナ
issuedCodes: (Code -> lone Client -> ResourceOwner) -> Time, // 発行したコード
}
状態変化をどうモデリングするかだけど、教科書で紹介されていた方法で、イベントをシグネチャとして表すものを採用した。他の方法も試したけど、今回のように変化する状態が複数ある（プロバイダ側、コンシューマ側）場合はこのやり方がシンプルに書けると思う。
イベントにはつねにユーザエージェントが対応するものとして userAgent、イベント発生前と後の時刻に pre、post フィールドを持たせる。OAuth のフローは HTTP リダイレクトによって次のステップへと進むが、この関係を表すため inParams、outParams、initiator を定義する。
abstract sig Token {}
sig ClientId, ClientSecret, Code, State extends Token {}
abstract sig Event {
pre, post: Time,
userAgent: UserAgent, // イベントを引き起こしたユーザエージェント
inParams: set Token, // 前のイベントから受けとったパラメータ
outParams: set Token, // 次のイベントに渡すパラメータ
initiator: lone Event, // 前のイベント
}
詳しく言うと、イベントは
- ユーザが OAuth コンシューマを訪問する UserAgentVisitsClientEvent、
- リダイレクトされたユーザが OAuth プロバイダでコンシューマを認可し、プロバイダが code を発行する AuthorizationServerIssueCodeEvent、
- さらにリダイレクトされたユーザによってもたらされた code でコンシューマがリソースへのアクセス権を得る ClientAuthorizesUserAgentEvent
と進んで完了、ということにしたいので以下のように定義した（抜粋）。シグネチャのフィールド宣言のあとに中括弧を書くと、そのシグネチャにまつわる fact をシンプルに書ける。
sig UserAgentVisitsClientEvent extends Event { ... } {
no initiator // fact { all e: UserAgentVisitsClientEvent { no e.initiator } } と同義
inParams = none
outParams = state + client.id
...
}
sig AuthorizationServerIssueCodeEvent extends Event { ... } {
initiator in UserAgentVisitsClientEvent
inParams = clientId + state
outParams = code + state
...
}
sig ClientAuthorizesUserAgentEvent extends Event { ... } {
initiator in AuthorizationServerIssueCodeEvent
inParams = code + state
outParams = none
....
}
そしてイベント同士の関連を記述する。イベントの initiator が存在するときは、その outParams を inParams として引き継いでいなければならないとすることで、HTTP リダイレクトの改竄がないことを表現したつもり。また userAgent も同じである、とすれば完全なのだけど、それだと面白みがないので、前のイベントが MaliciousUserAgent によって引き起こされたものであれば、その結果を他のユーザエージェントが引き継いでしまうことを許すことにした。これで悪意あるユーザが他のユーザに CSRF を仕掛けることが可能になる。
fact eventsTakeOverInitiatorsParams {
all e: Event {
let e' = e.initiator {
e.inParams = e'.outParams
some e' implies { e.userAgent = e'.userAgent or e'.userAgent in MaliciousUserAgent }
}
}
}
abstract sig UserAgent {}
sig InnocentUserAgent, MaliciousUserAgent extends UserAgent {}
イベントに基づく状態変化のモデリングは、イディオム的に以下のようにする。
まず2つの時刻間における述語を定義する。その間で状態が変化した場合、対応するイベントが存在しているはず……ということを表現している。
pred step(t, t': Time) {
some e: Event {
e.pre = t
e.post = t'
userAgentStates.t != userAgentStates.t' iff e in UserAgentVisitsClientEvent
issuedCodes.t != issuedCodes.t' iff e in AuthorizationServerIssueCodeEvent
obtainedAuthorizations.t != obtainedAuthorizations.t' iff e in ClientAuthorizesUserAgentEvent
}
}
イベントに対応する fact で状態変化を記述する。
sig UserAgentVisitsClientEvent extends Event { ... } {
...
userAgentStates.post = userAgentStates.pre + client -> state -> userAgent
}
で、これが全ステップ間成り立つことを記す。
pred init(t: Time) {
no issuedCodes.t
no obtainedAuthorizations.t
no userAgentStates.t
}
fact trace {
init[first]
all t: Time, t': t.next {
step[t, t']
}
}
これでできた。あとは、ユーザエージェントに対してクライアントが取得したリソースが、認可サーバ（リソースサーバ）においてユーザエージェントが保持しているリソースと一致することを assert してチェックする。
assert userAgentsAreProperlyAuthorized {
all client: Client, userAgent: InnocentUserAgent, resourceOwner: ResourceOwner, t: Time {
resourceOwner in client.obtainedAuthorizations.t[userAgent] implies {
let authServer = client.authServer {
authServer.knownResourceOwners[userAgent] = resourceOwner
client -> resourceOwner in authServer.issuedCodes.t[Code]
}
}
}
}
check userAgentsAreProperlyAuthorized for 6 but exactly 1 AuthorizationServer, exactly 1 Client, 2 UserAgent
で、実際最後にクライアントがリソースの認可を取得するところで state パラメータのチェックを行わないことにする（コメントアウトする）と、以下のような反例が見つかる。
MaliciousUserAgent のために発行された code でもって他のユーザエージェントが OAuth コンシューマにアクセスすると、そのユーザエージェントのものではないリソースへのアクセス権が得られてしまうような状況が発見できている。つかれた……。
まとめ
Alloy でウェブのフローを部分的にモデリングすることができた。今回は出来上がったものだけがあるのだけど、Alloy はモデルを一気に記述してそのバグを発見するのではなく、ボトムアップに組み立てながら小さいアサーションを繰り返し、インクリメンタルに仕様を作っていくのにこそ向いていると感じた。頑張って書いてみたけど、あとから読めないのではないかというおそれもある。書いたり読んだりするのには熟練が必要だと感じた。
調べてみるとけっこう Alloy を紹介したスライドやらエントリはたくさんあって、知らない世界を覗いた気持ちだった。
参考文献
- 作者:Daniel Jackson
- 発売日: 2011/07/15
- メディア: 単行本（ソフトカバー）
- 作者:中島 震
- 発売日: 2012/04/20
- メディア: 単行本（ソフトカバー）
OAuth2 のフローを Alloy Analyzer でモデリングする - 詩と創作・思索のひろばb.hatena.ne.jp ……とのこと。
- [alloy]
参考文献にある形式手法入門は間違いが多いので注意。おすすめできない。
2016/06/30 17:48
体系的に学ぶ 安全なWebアプリケーションの作り方 脆弱性が生まれる原理と対策の実践
- 作者:徳丸 浩
- 発売日: 2011/03/01
- メディア: 単行本
- Alloyまとめ - 西尾泰和のはてなダイアリー
- Alloy勉強日記
- Towards a formal foundation of web security … Alloy でウェブ一般のフローを表現するためのフレームワーク。ちょっと一般化されすぎていて初心者には難しかった。
- Formal verification of OAuth 2.0 using Alloy framework … Knowledge flow analysis という方法で OAuth 2.0 を検証したものらしい。ちゃんと読んではない。
