(解説) はてなブックマークにおけるアクセス制御 - 半環構造に基づくモデル化

こんにちは、シニアアプリケーションエンジニアのid:taraoです。この記事ははてなデベロッパーアドベントカレンダー2015の10日目です。昨日はid:tapir320によるはてなの組織開発についてでした。

先月開催されたWebDB Forum 2015で、「はてなブックマークにおけるアクセス制御: 半環構造に基づくモデル化」というタイトルの発表をしました。

はてなブックマークにおけるアクセス制御 - 半環構造に基づくモデル化 from Lintaro Ina

発表資料には多くの方に興味をもっていただけたようですが、わかりにくい点も多かったのではないでしょうか。スポンサー企業としての技術報告セッションとはいえ学術会議での発表なので理論面と独自の工夫点にフォーカスした内容であったり、口頭での発表のしかたに大きく依存したスライドの遷移方法になっているので、この資料だけで細かいところまで理解しようとするのは無理があるとおもいます。そこでこの記事は、平易に説明できる部分は数式を持ち出さずに、気になる人だけ理論的な部分も追加で読めるように、解説しようとおもいます。

前提

今回の話題は開発中のScala版はてなブックマークでの内容です。Scala版はてなブックマークについては8月のScala関西 Summit 2015で発表した通りで、Scala版を開発中と言ってもこれはコア部分の話で、フロントエンド(サーバ側のビュー部分)はPerlによる実装となる予定です。開発中の実装にもとづく内容なので、実際にリリースされる頃には全くべつの方法をとっている可能性もあるのでご注意ください。

はてなブックマーク in Scala from Lintaro Ina

どういうことをやろうとしているのか

発表資料を見た方の中には「思ったほどたいした話じゃなかった」という人もいた反面、「これを分かるようになるには一体どうすれば…」「これってスラスラ理解できるものなのか」「日本語でOK」など、難しいとおもった人も多かったようです。確かに数学的な部分をきちんと理解するのは容易ではないかもしれません(とはいえ学部レベルの群論あたりの知識さえあれば、あとはウィキペディアかなにかで半環の定義を確認すれば理解できる程度なのでがんばってほしいところではあります)。

実際のところは、全く大した話ではありません。単に、複雑になりがちなアクセス制御をうまいモデルに落とし込んで一貫したコードでメンテナンスしていくにはどうしたらよいか、という話です。これ自体は数学的な知識は一切なくても、勘だけでよいやり方にしていくことは可能でしょう。あるいは、すでによいやり方になっているコードベースを抱えたチームに新たにジョインして、他の人の担当箇所を真似て実装していくという程度であれば、数学的背景を知る必要は一切ないとおもいます。

問題は、そのように「よいやり方」だとチームが信じたやり方が、本当に正しいやり方かどうか、というところです。その正しさを数学的に示すことで、チームの技術的選択に自信を持つことができ、後になって大きな過ちが露呈するということを防げます。あるいは、状況が変わったときに、これまでの「よいやり方」のままでよいのか、もっとよいやり方の検討が必要かどうかの判断材料にもなります。

つまり、チームで(あるいは会社全体で)技術をリードして決断する立場にある人間にとっては、理論的な背景を理解している方が技術的な判断の役に立つということです。しかしこれはアクセス制御の話に限ったことではなく、ごく一般的な、当たり前のことでしょう。「これをメンテできる人を採用しアサインし続ける自信がある会社というのはなかなかすごい」という感想もあったようですが、そのような人材を揃えられなければどのみち基礎のぐらついた開発を強いられるという危機感を持った方がよいのではないでしょうか。

アクセス制御のモデル化

数学的な背景はともかく、実際にアクセス制御を扱うコードを見ながらどういうモデルが適しているか考えてみましょう。ここで考えるアクセス制御は、もちろんはてなブックマークのためのアクセス制御です。他のサービスではたとえばロールベースのアクセス制御など、これまでによく知られた別の方法が適しているかもしれません。

ごく単純なアクセス制御

はてなブックマークはソーシャルブックマークサービスなので、あるユーザがあるURLをブックマークしたことは基本的には他のユーザからも見えます。とはいえ、ソーシャルな機能はとくに必要とせず、ブックマークをインターネット上に保存しておいて複数の端末から共有する目的でのみ利用したいユーザもいて、他のユーザからは見えないようにしたいこともあります。このような場合には、はてなブックマークを完全に非公開で使うことができます。非公開に設定されたユーザのブックマーク一覧ページは本人しか見えなくなり、エントリページにもそのユーザのブックマークは表示されなくなります。

このような機能を実現する単純な方法としては、ブックマークアイテムを表示しうるあらゆる箇所で、ブックマークアイテムの所有者がページの訪問者自身であるかどうかチェックすることになるでしょう。

if (bookmark.owner.isPublic || bookmark.owner == visitor)
  Some(bookmark)
else None

この程度であればまだそこまで非現実的という感じはしませんね。

少し複雑なアクセス制御

はてなブックマークには、非公開設定で利用している場合でも特定のユーザにだけは閲覧を許す機能があります。この機能の使い道の是非は置いておくとして、アクセス制御のしくみを考える上ではだいぶ厄介そうだということはわかるとおもいます。素朴なコードで表すと以下のようになるでしょうか。

if (bookmark.owner.isPublic ||
    bookmark.owner == visitor ||
    bookmark.owner.allowedUsers.contains(visitor))
  Some(bookmark)
else None

条件が複雑になって、いかにも間違えやすそうです。条件をいちいち間違いのないように書くのではなくて、bookmark.ownerとvisitorが決まったらチェックすべき内容が一意に定まるようになっていて欲しい気がします。なにかのメソッドにまとめたらよいでしょうか? まぁそれもよいでしょう。ここでは一歩ふみ込んで、以下のようなインタフェースでチェックするしくみにできないか考えてみましょう。

val r = requestOf(visitor)
val p = permissionOf(bookmark.owner)
if (p allows r) Some(bookmark)
else None

もしこう書くことができれば、アクセス制御のための条件分岐であることが非常にわかりやすくなり、visitorやbookmark.ownerの部分がなにか別の種類のものになっても統一的に扱うことができそうです。ここではrequestOf()の返り値を要求、permissionOf()の返り値を許可と呼ぶことにして、要求や許可およびallowsメソッドがどのようになっていればいいか考えてみましょう。最終的にこの形で書けるようになるのは次の次の節になります。心してかかりましょう。

||で結ばれた3つの条件のうちまずはbookmark.owner.allowedUsers.contains(visitor)の条件について考えてみます。これは閲覧許可されたユーザのうちのいずれかにvisitorが一致すればよいことを表しているので、「または」の条件になっていることがわかります。つまり、以下の疑似コードと同じ意味だということです。

if (bookmark.owner.isPublic ||
    bookmark.owner == visitor ||
    bookmark.owner.allowedUsers(0) == visitor ||
    bookmark.owner.allowedUsers(1) == visitor ||
    ...
    bookmark.owner.allowedUsers.last == visitor)
  Some(bookmark)
else None

こうしてみると、2つ目の条件bookmark.owner == visitorはそれ以降の条件とよく似た形をしていて、以下のようにまとめられることがわかります。

if (bookmark.owner.isPublic ||
    (bookmark.owner +: bookmark.owner.allowedUsers).contains(visitor))
  Some(bookmark)
else None

同じようにして、bookmark.owner.isPublicの条件もまとめられないでしょうか? 実は「すべてのユーザを含むリスト」を作ることができれば可能です。すべてのユーザを含むリストをAllUsersとすると、以下のようにすればすべての条件をcontainsによる比較にまとめることができます。

def allowedUsersOf(bookmarkOwner: UserEntity): Seq[UserEntity] = {
  val allOrNothing = if (bookmarkOwner.isPublic) AllUsers
                     else Seq.empty
  val self = Seq(bookmarkOwner)
  val allowedUsers = bookmarkOwner.allowedUsers
  allOrNothing ++ self ++ allowedUsers
}

if (allowedUsersOf(bookmark.owner).contains(visitor)) Some(bookmark)
else None

「すべてのユーザを含むリスト」を作るのは現実的ではないので、ユーザの包含関係で直接条件をチェックするのではなく、「どういう属性のユーザに許可するか」「どういう属性のユーザからの要求か」という条件でチェックすることにしましょう。両者に共通する属性があれば閲覧を許可するということです。こうすれば、bookmark.owner.isPublicが成り立つときには、誰でも見ていいことを表すPublic属性を付与するということにできます。

sealed trait Attribute
object Attribute {
  case object Public extends Attribute
  case class User(userId: UserId) extends Attribute
}

def permissionAttrsOf(bookmarkOwner: UserEntity): Set[Attribute] = {
  val publicOrNot = if (bookmarkOwner.isPublic) Set(Attribute.Public)
                    else Set.empty
  val self = Set(Attribute.User(bookmarkOwner.id))
  val allowedUsers = bookmarkOwner.allowedUsers.map { u =>
    Attribute.User(u.id)
  }.toSet
  publicOrNot | self | allowedUsers
}

訪問ユーザからの要求の属性には、訪問ユーザ自身の属性の他に、必ずPublicがつくようにします。

def requestAttrsOf(visitor: UserEntity): Set[Attribute] =
  Set(Attribute.Public, Attribute.User(visitor.id))

訪問ユーザは、これらの属性のいずれかが許可されていれば、閲覧が可能だということです。最終的に閲覧可否をチェックするには、両者に共通する属性があるかどうかを確かめるのでした。

if ((permissionAttrsOf(bookmark.owner) & requestAttrsOf(visitor)).nonEmpty)
  Some(bookmark)
else None

ここまできたらpermissionAttrsOf()をpermissionOf()に、requestAttrsOf()をrequestOf()に、(_ & _).nonEmptyを_ allows _に読み替えれば、目的の書き方に合致したものになっていることがわかりますね!

もっと複雑なアクセス制御

はてなブックマークでは、ユーザのブックマーク一覧そのものは公開していても、あるURLのみ非公開でブックマークするということが可能です。ブックマーク一覧が非公開の場合は、閲覧許可ユーザに指定されたユーザであっても個別に非公開にされたブックマークアイテムを見ることはできません。このチェックを素朴に書くと以下のような具合になります。

if (bookmark.owner.isPublic ||
    bookmark.owner == visitor ||
    (bookmark.owner.allowedUsers.contains(visitor) && bookmark.isPublic))
  Some(bookmark)
else None

あるいは、ブックマーク所有者に関する閲覧可否と、ブックマークアイテムそのものに関する閲覧可否に分けて考えると、以下のように書いても同じです。

if ((bookmark.owner.isPublic ||
     bookmark.owner == visitor ||
     bookmark.owner.allowedUsers.contains(visitor)) &&
    (bookmark.isPublic ||
     bookmark.owner == visitor))
  Some(bookmark)
else None

ここまでくれば、どういう属性のユーザにブックマークアイテムの閲覧を許可するかを計算できれば、先程と同様に扱えます。

def permissionAttrsOf(bookmark: BookmarkEntity): Set[Attribute] = {
  val publicOrNot = if (bookmark.isPublic) Set(Attribute.Public)
                  else Set.empty
  val self = Set(Attribute.User(bookmark.id.userId))
  publicOrNot | self
}

val r = requestAttrsOf(visitor)
val p1 = permissionAttrsOf(bookmark.owner)
val p2 = permissionAttrsOf(bookmark)
if ((p1 & r).nonEmpty && (p2 & r).nonEmpty) Some(bookmark)
else None

アクセス制御の合成

ここまででだいぶうまくモデル化できていそうなことはわかりましたが、最終目標であるp allows rでチェックできるようにはなっていません。とくに、最後の例ではけっきょく条件に&&がでてきて、このままだと属性による比較のしかたがどんどん複雑化してしまいそうです。

p1とp2という2つの許可をともに満たせばよい、という形で表現することができたので、あとはこの「ともに」という条件を許可の合成として表現できれば、当初の目論見通りの統一的な表現にできます。

val r = requestOf(visitor)
val p1 = permissionOf(bookmark.owner)
val p2 = permissionOf(bookmark)
val p = p1 & p2 // 許可の合成
if (p allows r) Some(bookmark)
else None

このように書けるようにするには、許可をSet[Attribute]ではなくSeq[Set[Attribute]]で表して、外側のSeqを「かつ」の条件に、内側のSetを「または」の条件に対応させればうまくいきます。

case class Request(attrs: Set[Attribute])

case class Permission(attrsList: Set[Attribute]*) {
  def &(other: Permission): Permission =
    Permission(this.attrsList ++ other.attrsList: _*)
  def allows(request: Request): Boolean =
    attrsList.forall(attrs => (attrs & request.attrs).nonEmpty)
}

def permissionOf(user: UserEntity): Permission =
  Permission(permissionAttrsOf(user))
def permissionOf(bookmark: BookmarkEntity): Permission =
  Permission(permissionAttrsOf(bookmark))

def requestOf(visitor: UserEntity): Request =
  Request(requestAttrsOf(visitor))

Permissionは複数のSet[Attribute]を内部に持っていて、allowsによるチェックの際にはそのすべてに対して(forall)(_ & _).nonEmptyが成り立つことを確認します。

ブックマークアイテムの閲覧可否を確認するときは、アイテム所有者のブックマーク一覧の閲覧可否も同時にチェックする必要があるので、ブックマークアイテム単体での許可は取得できないようにしてしまうとなおよいでしょう。

private def permissionOf(bookmark: BookmarkEntity): Permission = ...
def permissionOf(bookmarkAndOwner: (UserEntity, BookmarkEntity)): Permission =
  permissionOf(bookmarkAndOwner._1) & permissionOf(bookmarkAndOwner._2)

こうしておけば、permissionOf(bookmark)を直接呼び出すことはできず、permissionOf((bookmark.owner, bookmark))とすることを強制できます。ブックマークアイテムの許可を取得したければ自動的にその所有者の許可も取得することになります。つまり、所有ユーザに関するアクセス制御をし忘れることを防げるわけです。

val r = requestOf(visitor)
//val p = permissionOf(bookmark) // コンパイルエラー
val p = permissionOf((bookmark.owner, bookmark))
if (p allows r) Some(bookmark)
else None

許可の合成を表現できるようにした効果が発揮されましたね!

モデルの正しさ

ここまではとくに数学的な話はせずにやってこれました。数学の素養がなくてもこの程度のモデルは気合いで思いつくでしょう。しかし、そうやって思いついたモデルの実装が本当に正しいことをしているか、となると話はべつです。たとえば、Permissionのデータ構造と&やallowsメソッドの実装は本当に正しいですか? 「当たり前だろう」とおもった人のために間違ったPermissionの実装を一つお見せしましょう。

Seq[Set[Attribute]]の外側のSeqは「かつ」の条件を表しているのだから、そもそもSeqにしないで&メソッドが積集合をとるようになっていればいいじゃないか、とおもったとします。

case class IncorrectPermission(attrs: Set[Attribute]) {
  def &(other: IncorrectPermission): IncorrectPermission =
    IncorrectPermission(this.attrs & other.attrs)
  def allows(request: Request): Boolean =
    (this.attrs & request.attrs).nonEmpty
}

なるほど、これでいいならだいぶシンプルになりますね。しかしこれは誤りです。なぜなら、&で合成してallowsで確認したときと、個別にallowsで確認した結果を「かつ」で結んだときとで結果が異なる場合があるからです。

val r = Request(Set(Attribute.Public, Attribute.User(2)))
val p1 = IncorrectPermission(Set(Attribute.Public, Attribute.User(1)))
val p2 = IncorrectPermission(Set(Attribute.User(2)))
(p1 & p2) allows r             // false
(p1 allows r) && (p2 allows r) // true

この例の場合、p1 & p2の結果はIncorrectPermission(Set())になるので、いかなるRequestに対してもallowsはfalseを返します。しかし個別にチェックした場合、p1はAttribute.Publicを、p2はAttribute.User(2)を共通して持つので、それぞれの結果はtrueになり、全体の結果もtrueになります。

モデルが間違っている場合、このように反例を見つけることで間違いを指摘できますが、反例がたまたま見つからないからといって正しいと言えるでしょうか? そういう意味では前の節までで紹介した実装も正しいかどうか確信が持てなくなってきます。確信が持てなくてもかまわない、バグってても知らない、という人はこれ以降は読まなくてよいでしょう。おつかれさまでした。

正しいという確証を得たい場合には、問題を数学的に扱うことで解決することもあります。正しさを文字通り「証明」できる可能性があるからです。さらに、数学的に扱うことでより一般化された問題に対処する糸口がつかめることもあります。たとえば以下のように、モデルを拡張したい場合にも数学的背景の理解は有用です。

(例) 「かつ」の条件(&)だけでなく「または」の条件でも合成したい
(例) 「属性を含まない」という条件を課したい

そもそもモデルを考える際に、ごく限られた表現力のモデルとその数学的な定義を考えて、成り立つべき性質を保ったままモデルを拡張していく、という手法がとれるようになると、もはや数学は正しさを証明するだけのツールではなく、モデリングの方法論にもなりえます。

数学的背景

許可を合成する操作が正しいかどうかを議論するためには、許可 $p$ に対する合成操作が、任意の要求 $r$ について $p \allows r$ した後も保存されることを確かめる必要があります。 $p$ の構造とifの条件式に書けるもの(Boolean)の構造がある意味で一致することを確かめればよいということです。

許可 $p$ には「かつ」や「または」の構造があり、Booleanつまりブール代数(Boolean algebra)における「かつ」や「または」の意味と一致することが期待されます。「かつ」と「または」を持つ構造は半環(semiring)とおもうことができ、「構造がある意味で一致する」というのは「半環上の準同型写像(homomorphism)が存在する」という言葉に言い換えることができます。

属性と要求の定義

許可についての定義の前に、属性と要求を定義しておきます。属性はすべての属性の集合 $A$ の要素で、要求は属性をいくつか含んだ集合です。

定義 (属性 $a$ )
$a \in A$

定義 (要求 $r$ )
$r \in \powerset(A)$

$\powerset(A)$ は $A$ の冪集合(power set)で、 $A$ の部分集合をすべて含むような集合です(つまり集合の集合です)。 $A = \{a_1, a_2, a_3\}$ だとすると、 $\powerset(A) = \{ \emptyset, \{ a_1 \}, \{ a_2 \}, \{ a_3 \}, \{ a_1, a_2 \}, \{ a_2, a_3 \}, \{ a_3, a_1 \}, \{ a_1, a_2, a_3 \} \}$ になります。 $r$ はこのような冪集合の要素なので、 $A$ の要素をいくつか含むような集合ということになります。

許可の半環による一般化

コード例で示したPermissionは「かつ」の条件に相当する&による合成しかサポートしていませんでしたが、ここでは「または」による合成も可能な構造として許可を定義しておきましょう。許可に対する「かつ」の条件の合成を $\otimes$ で、「または」の条件の合成を $\oplus$ で表し、以下のように定義すると、 $\rig<\powerset(\powerset(A)),\oplus,\otimes,\emptyset,\emptysingleton>$ は半環になります。

定義 (許可 $p$ )

$p \in \mathcal{P}(\mathcal{P}(A))$

$p_1 \oplus p_2 \defeq p_1 \cup p_2$

$p_1 \otimes p_2 \defeq p_1 \Cup p_2 \defeq \{ q_1 \cup q_2 \mid q_1 \in p_1 \wedge q_2 \in p_2 \}$

$p$ は冪集合の冪集合の要素なので、属性の集合の集合です。

$p = \permissionset$

と書けて、外側の集合が「または」の条件を表し内側の集合が「かつ」の条件を表す積和形(積の和の形)になっています(これはPermissionの定義とは逆になっていることに注意してください)。つまり、 $\{ \{ a \} \} \in \mathcal{P}(\mathcal{P}(A))$ を単に $a$ と書くことにすると、

$\permissionset = \\ \quad \unfactorized$

となっているということです。

本来はこのように定義した $\rig<\powerset(\powerset(A)),\oplus,\otimes,\emptyset,\emptysingleton>$ が確かに半環になっていることを示す必要がありますが、容易に確かめられるので省略します。半環とは大雑把に言うと、たとえば自然数のように加算と乗算が定義された構造で、自然数上の加算と乗算のように結合律や交換律、分配律を満たし、単位元を持つような構造のことです。今回定義した半環は $\otimes$ が乗算で $\oplus$ が加算です。

これらの定義に基づくと、 $p \allows r$ は以下のように定義できます。(許可の構造が違うのでPermission.allowsの定義とは一致しない点に注意してください。)

定義 ( $\allows$ )
$p \allows r \defeq \exists q \in p.\; q \subseteq r$

準同型性

許可の半環構造がブール代数に一致することは、許可からブール代数への(半環上の)準同型写像が存在することによって示します。いま問題にしているのは $p \allows r$ によって「かつ」や「または」の操作が保存されるかどうかなので、 $f(p) = p \allows r$ が準同型写像になっていることを確かめることになります。

半環上の準同型写像について議論しているので、ブール代数も半環である必要があります。ブール代数は、真( $\top$ )と偽( $\bot$ )の二値の集合 $\mathbb{B} = \{ \top, \bot \}$ 上に定義された、「かつ」の演算 $\wedge$ と「または」の演算 $\vee$ を持つ代数構造です。

補題 (ブール代数は半環)
ブール代数 $\rig<\mathbb{B},\vee,\wedge,\bot,\top>$ は半環をなす。

証明は省略しますが、半環としてのブール代数は、 $\wedge$ が乗算、 $\vee$ が加算になります。

定理 (準同型性)
すべての $r$ について、 $f(p) = p \allows r$ で定義される $f : \mathcal{P}(\mathcal{P}(A)) \to \mathbb{B}$ は半環上の準同型写像である。

半環上の準同型性を示す必要があるので、以下の4つを示すことになります。

$f(p_1 \oplus p_2) = f(p_1) \vee f(p_2)$
$f(p_1 \otimes p_2) = f(p_1) \wedge f(p_2)$
$f(\emptyset) = \bot$
$f(\emptysingleton) = \top$

下2つはほぼ自明なので証明は省略して、上2つについて証明しておきます。

■証明 ( $f(p_1 \oplus p_2) = f(p_1) \vee f(p_2)$ )

許可の定義から $p_1 = \{ q_1, q_2, \ldots, q_n \}$ 、 $p_2 = \{ q_{n+1}, q_{n+2}, \ldots, q_{n+m} \}$ 、 $p_1 \oplus p_2 = \{ q_1, \ldots, q_n, q_{n+1}, \ldots, q_{n+m} \}$ と書ける(重複する要素も並べて書いている)。 $\allows$ の定義より $f(p_1 \oplus p_2) \equiv \exists i.\; q_i \subseteq r$ ( $1 \le i \le n+m$ ) なので、 $i \le n$ なら $f(p_1)$ が成り立ち、 $n < i$ なら $f(p_2)$ が成り立つので、 $f(p_1 \oplus p_2) \equiv f(p_1) \vee f(p_2)$ である。■

■証明 ( $f(p_1 \otimes p_2) = f(p_1) \wedge f(p_2)$ )

$f(p_1 \otimes p_2) \equiv f(p_1) \wedge f(p_2)$ を ( $\Rightarrow$ ) と ( $\Leftarrow$ ) に分けて示す。

( $\Rightarrow$ ) $\allows$ の定義より $\exists q \in p_1 \Cup p_2.\; q \subseteq r$ で、 $\Cup$ の定義より $\exists q_1, q_2.\; q = q_1 \cup q_2 \wedge q_1 \in p_1 \wedge q_2 \in p_2$ が成り立つ。従って、 $q_1 \in p_1$ より $f(p_1)$ 、 $q_2 \in p_2$ より $f(p_2)$ が成り立つ。

( $\Leftarrow$ ) $\allows$ の定義より $q_1 \in p_1$ かつ $q_1 \subseteq r$ 、 $q_2 \in p_2$ かつ $q_2 \subseteq r$ なる $q_1$ と $q_2$ が存在する。 $\otimes$ の定義より $q_1 \cup q_2 \in p_1 \otimes p_2$ なので、 $q_1 \cup q_2 \subseteq r$ により $f(p_1 \otimes p_2)$ が成り立つ。■

準同型性が成り立つので、 $\otimes$ や $\oplus$ で合成された許可をいったんばらばらにしてそれぞれの $\allows r$ を計算した後、 $\wedge$ や $\vee$ (ifの条件としての「かつ」や「または」)で組み合わせても、結果は同じになることが保証されます。

和積形

コードで表現されたPermissionは属性集合のリストであり、外側のリストが積(「かつ」)を、内側の集合が和(「または」)を表すようなものでした。これは数学的に定義した半環構造をもつ許可の言葉で言えば、 $\oplus$ と $\otimes$ に関して和積形(和の積の形)で表せるものに限定したものとおもうことができます。和積形とはつまり因数分解された形のことです。

Permissionの実装の正しさを証明するには、和積形に限定して数学的に定義した許可およびPermission.allowsに相当する関数が、積和形での定義と同値になることを示せばよいことになります。

定義 (和積形 $\var{p}$ )
以下を満たすような $\var{p}$ を $p$ の和積形と呼ぶ。

$\var{p} = \permissionset$

$p = \factorized$

定義 ( $\varallows$ )
$\var{p} \varallows r \defeq \forall q \in \var{p}.\; q \cap r \ne \emptyset$

Permission.allowsの実装はこの $\varallows$ の定義と一致していることがわかります。

あとは $\varallows$ と $\allows$ が一致することを示すだけです。

定理 (和積形と積和形の同値性)
すべての $r$ に対して $\var{p} \varallows r \equiv p \allows r$ が成り立つ。

■証明

積和形の準同型性より、 $\var{p} = \shortpermissionset$ のすべての $\{ a_{i1}, \ldots, a_{im_i} \}$ について、 $\{ \{ a_{i1}, \ldots, a_{im_i} \} \} \varallows r \equiv (a_{i1} \oplus \cdots \oplus a_{im_i}) \allows r$ が成り立てばよい。 $\varallows$ の定義より、 $\{ \{ a_{i1}, \ldots, a_{im_i} \} \} \varallows r \equiv \exists j.\; \{ a_{ij} \} \subseteq r$ が成り立つ。 $a_{i1} \oplus \cdots \oplus a_{im_i} = \{ \{ a_{i1} \}, \ldots, \{ a_{im_i} \} \}$ であるから、 $\exists j.\; \{ a_{ij} \} \subseteq r \equiv (a_{i1} \oplus \cdots \oplus a_{im_i}) \allows r$ である。■

和積形は、「かつ」の条件を加えるのに要素を1つ追加するだけでよい( $\Cup$ を計算する必要がない)ので、「または」の条件を合成しないなら、できる限り和積形で表現しておくと計算が少なくて済みます。その上、積和形における $\allows$ と和積形における $\varallows$ の同値性が成り立つことがわかったので、和積形に関しても準同型性を使うことができ、「かつ」の計算をばらばらにやってもよいことがわかります。

おわりに

アクセス制御には間違いがあってはならない割に、間違えにくいよいモデル化の方法論についての情報はそれほど多くない気がします。ベストプラクティスが確立されていないと感じる場面で独自の方法でやっていくには勇気がいりますが、数学的な正しさを拠り所にすることで自信がもてます。

はてなでは、数学やコンピュータサイエンスをサービス開発に活かせるエンジニアを募集しています。

はてなデベロッパーアドベントカレンダーの明日の担当はid:daiksyです。お楽しみに!

Hatena Developer Blog

(解説) はてなブックマークにおけるアクセス制御 - 半環構造に基づくモデル化

前提

どういうことをやろうとしているのか

アクセス制御のモデル化

ごく単純なアクセス制御

少し複雑なアクセス制御

もっと複雑なアクセス制御

アクセス制御の合成

モデルの正しさ

数学的背景

属性と要求の定義

定義 (属性 $a$ )

定義 (要求 $r$ )

許可の半環による一般化

定義 (許可 $p$ )

定義 ( $\allows$ )

準同型性

補題 (ブール代数は半環)

定理 (準同型性)

■証明 ( $f(p_1 \oplus p_2) = f(p_1) \vee f(p_2)$ )

■証明 ( $f(p_1 \otimes p_2) = f(p_1) \wedge f(p_2)$ )

和積形

定義 (和積形 $\var{p}$ )

定義 ( $\varallows$ )

定理 (和積形と積和形の同値性)

■証明

関連研究

Tuple-Based Access Control: a Provenance-Based Information Flow Control for Relational Data

Semiring-Annotated Data: Queries and Provenance

A lattice model of secure information flow

おわりに

400社以上の技術ブログが
毎日読める

前提

どういうことをやろうとしているのか

アクセス制御のモデル化

ごく単純なアクセス制御

少し複雑なアクセス制御

もっと複雑なアクセス制御

アクセス制御の合成

モデルの正しさ

数学的背景

属性と要求の定義

定義 (属性 )

定義 (要求 )

許可の半環による一般化

定義 (許可 )

定義 ()

準同型性

補題 (ブール代数は半環)

定理 (準同型性)

■証明 ()

■証明 ()

和積形

定義 (和積形 )

定義 ()

定理 (和積形と積和形の同値性)

■証明

関連研究

Tuple-Based Access Control: a Provenance-Based Information Flow Control for Relational Data

Semiring-Annotated Data: Queries and Provenance

A lattice model of secure information flow

おわりに

定義 (属性 $a$ )

定義 (要求 $r$ )

定義 (許可 $p$ )

定義 ( $\allows$ )

■証明 ( $f(p_1 \oplus p_2) = f(p_1) \vee f(p_2)$ )

■証明 ( $f(p_1 \otimes p_2) = f(p_1) \wedge f(p_2)$ )

定義 (和積形 $\var{p}$ )

定義 ( $\varallows$ )