SpiceDBとProlog
弊社は PocketSign Platform というサービスを開発しており、これに登録することで弊社の Verify API を誰でも試用することができます。
PocketSign Platform には、ポケットサイン開発環境・テスト環境・本番環境の3つの環境が存在し、以下のように利用が制限されています。
- ポケットサイン開発環境は誰でも利用可能
- テスト環境は弊社と利用契約を締結した組織のメンバーのみ利用可能
- 本番環境はSP事業者となった組織のメンバーのみ利用可能
これらの制御に、Fine-Grained Authorization（細粒度認可）の概念を元に開発された SpiceDB というシステムを利用しています。
認可判断をするSpiceDBを最初に見たときに、これは、特定の質問の真偽値を判定するシステムである「Prolog」と似ているのでは？と思ったのがこのブログを書くきっかけとなりました。
これから、SpiceDBとPrologの関連性を例を出しつつ紹介していきます。
Fine-Grained Authorizationの具体例
みなさん、Fine-Grained Authorization（細粒度認可） を知っていますか？僕は PocketSign Platform に関わることになって初めて知りました。
これはGoogle Driveなどで利用されている認可手法です。
例えば、Google Driveでは、自分が作成したスプレッドシートは自分のみ閲覧・編集が可能です。そして、他者が明示的に閲覧・編集権限を与えて共有することによって、自分はそのファイルだけ閲覧・編集が可能になります。
このように、Google Driveでは、
- 「自分」は「自分のファイル」の「編集者」である
- 「自分」は「共有ファイル」の「閲覧者」である
- 「ファイル」の「編集者」は「編集できる」
- 「ファイル」の「閲覧者と編集者」は「閲覧できる」
といったアクセス制御が行われています。
このような
- 「〇〇（誰）」は「□□（何）」の「☓☓（役割）」である
- 「□□（何）」の「☓☓（役割）」は「△△（どう）できる」
といった権限を管理する手法が、Fine-Grained Authorizationです。
この概念を元にして、Google は Zanzibar というシステムを作成しました。Google DriveなどのGoogleのサービスは、このZanzibarが内部でアクセス制御を行っています。
また、これは論文として公開されており、この論文をもとに実装されたオープンソースの権限管理ソフトウェアにSpiceDB という認可システムがあります。
SpiceDB
SpiceDBの機能
SpiceDBの主な機能の一つは、
- （誰）が（何）を（どう）できるか？
という質問への回答（Yes/No）を提供することです。
事前にSpiceDBに「（誰）が（何）を（どう）できる」というルールとデータを保存しておきます。そして、アクセス制御のタイミングでSpiceDBに問い合わせることで、適切な認可を行います。
この機能について今回紹介していきます。
このほかにも、
- 「□□に△△できる〇〇一覧は？」
などといった問い合わせも可能ですが、今回はこれらの詳細には触れません。興味のある方は、SpiceDBの紹介スライド や、ドキュメント を参考にしてください。
SpiceDBの利用例
では、SpiceDBの例として、非常に簡素な共有ドライブのアクセス制御の実装例を見てみましょう。
ユーザ、ディレクトリ機能のみが存在する共有ドライブを考えます。
直感的には、ディレクトリが閲覧可能なユーザは、そのディレクトリの以下のサブディレクトリも閲覧可能であってほしいので、そのようなルールを定義します。
以下がこれをSpiceDBのルールで記述したもので、Schemaと呼ばれます。
/* ディレクトリを閲覧可能なユーザを定義 */
definition user {}
/*
ディレクトリの定義
自身の「親」と自身が閲覧可能なユーザを要素として持つ
そのユーザが閲覧可能とは＝閲覧可能なユーザ自身 もしくは 親ディレクトリを閲覧可能なユーザ
*/
definition directory {
relation parent: directory
relation viewer: user
permission view = viewer + parent->view
}
事前に与えるデータとして以下のようなものを考えます。
directory:dir1#parent@directory:dir2 directory:dir2#viewer@user:user2 directory:dir1#viewer@user:user1
左辺#relation@右辺 というフォーマットで、3項関係を定義しています。
これは、
/dir2/dir1というディレクトリ構成- dir2はuser2が閲覧可能
- dir1はuser1が閲覧可能
という意味のデータです。
これらのデータをSpiceDBに与えておくことで、実際にユーザがディレクトリを閲覧しようとしたときに「user◯はdir□を閲覧可能か？」という質問をSpiceDBに問い合わせて結果（Yes/No）を得、それによって表示する/しないを制御する、といったことが可能になります。
以下でこの例を実際のSpiceDBとして動かすことができます。興味があったら試してみてください。
Assertionsタブで「dir1はuser2が閲覧可能か？」や「dir2はuser1が閲覧可能か？」という命題を表現しています。
assertTrue: - directory:dir1#view@user:user2 assertFalse: - directory:dir2#view@user:user1
「RUN」ボタンを押して評価することで、前者は真となり、後者は偽となることが確認できます。
SpiceDBとProlog
僕は、SpiceDBのこの機能を始めてみたとき、「認可されている/いない」を「True/False」と読み替えることで「特定の命題の真偽値を判定するシステム」と考えられるじゃないか、と思いました。
もちろん、SpiceDBができること、得意なことはこれ以外にもありますが、自分が数理論理学を学んでいたこともあり、SpiceDBが「命題の真偽値判定システム」であることに強い関心を覚えました。
そして、SpiceDBを見てすぐにPrologというプログラミング言語を思い出しました。これは「命題の真偽判定システム」として作成されたプログラミング言語で、SpiceDB以上に様々な命題の真偽判定ができます。
Prologで上記の例を記述してみましょう。
Prologに与える定義や具体例は、すべて「（a かつ b かつ …） ならば p(A,B,…)」という形式になっています。 p(A,B,…) のpを述語といい、A,B,…は引数です。a,b,…は0個以上の述語で、A,B,…をa,b,…の引数に使用することができます。数理論理学っぽいですね。
「（a かつ b かつ …） ならば p(A,B,…)」は以下のようにコード化されます。
p(A, B, …) :- a, b, …, z. p(A,B, …). % 右辺（前提）がない場合。これは常に p(A,B, …). が真であることを示す
「そのユーザが閲覧可能とは＝閲覧可能なユーザ自身 もしくは 親ディレクトリを閲覧可能なユーザ」をコードにすると、以下のようになります。
view(Dir, User) :- parent(Dir, X), view(X, User). /* 「parent(Dir, X), view(X, User)」は 「parent(Dir, X) かつ view(X, User)」となるXが存在する場合、真となる。 */
事前に与えるデータとして以下の述語を考えます。
parent("dir1", "dir2"). % /dir2/dir1 というディレクトリ構成 view("dir2", "user2"). % dir2はuser2が閲覧可能 view("dir1", "user1"). % dir1はuser1が閲覧可能
これらをPrologに事前に与えておき、view("dir2", "user1") の真偽をPrologに判定させれば、SpiceDBと同じことができます。
オンラインエディタ https://swish.swi-prolog.org/ などで試してみると、以下の結果となりました。
Prologの完全なソースコード
parent("dir1", "dir2"). % /dir2/dir1 というディレクトリ構成 view(Dir, User) :- parent(Dir, X), view(X, User). view("dir2", "user2"). % dir2はuser2が閲覧可能 view("dir1", "user1"). % dir1はuser1が閲覧可能 % 質問 view("dir2", "user1"). % False view("dir1", "user2"). % True
最後に
このように、SpiceDBを「命題の真偽判定システム」としてみたとき、論理プログラミング言語のPrologとよく似ているなぁと思い、同意や共感を得ようと思って同僚に片っ端からこのことを尋ねてみたのですが、Prologを知っている人が少ない、または知っていてもそう思わない人が多数で、同意してくれた人はごく少数でした…。
この記事では「SpiceDBやPrologが似てるよね〜」という話をするためにごく一部の機能しか紹介しておらず、またサンプルコードも少ないため、これを読んでも「似てるなぁ」と思ってくれる人は少ないかもしれません。
それでも、この記事を読んで、世の中には権限管理をするためのソフトでSpiceDBというものがあるんだなぁ、プログラミング言語の一つで論理式をあつかうPrologという言語があるんだなぁ、と、少しでも頭の片隅に残ってくれれば幸いです。
もしも興味が出たら、上記のオンラインエディタで簡単に遊べますし、prolog入門（ https://nw.tsuda.ac.jp/lec/prolog/intro/ ）を読んだりして学んでみてください。
最後まで読んでいただきありがとうございました。
おまけ
SpiceDBとPrologの練習のために、「サザエさん一家」を定義して、「タラちゃんは波平さんの子孫か？」という命題の真偽判定を行ってみました。
波平さん→サザエさん→タラちゃんの親子関係と上記の命題をSpiceDBで表現したサンプルです。
https://play.authzed.com/s/TVB-IiCUhOdK/schema
「Assertions」タブ（https://play.authzed.com/s/TVB-IiCUhOdK/assertions）で「タラちゃんは波平さんの子孫か？」はTrueに、「イクラちゃんは波平さんの子孫か？」はFalseになることが確認できると思います。
そして、上記の例を少し拡張して、「磯野家へ入れるのは、波平・フネ夫妻とその子孫のみである」という権限管理を作成してみました。
https://play.authzed.com/s/-56j4SdYvGT2/schema
また、Prologでも、波平さん→サザエさん→タラちゃんの親子関係を表現し、真偽判定を行ってみました。
offspring(X, Y) :- child(X, Y). % X が Y の子孫であるとは、X が Y の子であること offspring(X, Z) :- child(Y, Z), offspring(X, Y). % X が Z の 子孫であるとは、ある Y が存在し、Y が Z の子であり、かつ、X が Y の子孫であること child("sazae", "namihei"). % サザエさんは波平の子 child("sazae", "fune"). % サザエさんはフネの子 child("tara", "sazae"). % タラちゃんはサザエさんの子 child("tara", "masuo"). % タラちゃんはマスオさんの子 % 質問 offspring("tara", "namihei"). % True offspring("ikura", "namihei"). % False
