ある組織に所属する利用者だけが、その組織へ新しいメンバーを追加できるとする。組織に所属していない利用者が、自分自身をメンバーとして追加しようとした場合、現在の所属関係を調べれば操作は拒否される。ところが、追加予定の所属情報を認可判定の前に反映すると、その利用者は自分を追加した後の所属関係によって、追加操作を許可できてしまう。許可規則も操作する利用者も変わっていない。判定材料として使う所属情報の時点が変わっただけで、拒否されるべき操作が許可されるのである。
この現象には、二つの処理が関係している。第一は、現在の権限関係を調べ、利用者が操作を実行できるか判断する処理である。第二は、許可された操作によって所属情報を変更し、新しい権限関係を成立させる処理である。通常は前者の結果を受けて後者が実行される。しかし、後者によって初めて成立する所属関係を前者の判断材料に含めると、操作の結果が操作の許可理由になる。権限を獲得するために必要な許可を、獲得予定の権限によって満たすという循環が発生する。
認可の安全性は、許可条件の真偽だけでは決まらない。操作前の権限状態、操作で提案される変更、操作後の状態を区別し、その順序を保存した状態遷移として定義する必要がある。ただし、操作後の情報をすべて判定から排除すればよいわけでもない。新しい文書を作成する操作では、その文書が所属する組織や、作成時に設定される属性を確認する必要がある。利用者が現在持っている権限と、作成予定の対象が持つ属性には異なる役割がある。両者を区別したうえで、どの情報が操作前から成立していなければならないかを定めることが、状態を変更する認可の基本条件になる。
既稿「安全判定の揺らぎを入力・構造・評価方法に分けて測る」では、同じ操作の判定結果が変わったとき、入力条件と判定機構の変更を分けて原因を追う方法を整理した[1]。本稿で固定するのは許可規則であり、比較するのは判定材料となる権限状態の時点である。属性に基づくアクセス制御では、主体、対象、操作、環境に関する属性を規則と照合して許可を判断する[2]。Cedar の認可要求も、主体、操作、対象、文脈を指定して許可または拒否を求める構成を採る[3]。このような認可方式では、同じ属性名であっても、現在の事実を表す値と、操作によって成立する予定の値を区別する必要がある。認可判定と状態遷移を独立した関数として定義し、両者の関係から自己承認が成立する条件を明らかにする。
1. 許可条件が正しくても、許可されない操作が実行される
組織 G に所属する利用者だけが、G のメンバーを追加できるという規則を考える。利用者 A は G に所属し、利用者 B と C は所属していない。規則は「操作する利用者が G の既存メンバーであれば、メンバー追加を許可する」と定義する。A が B を追加する操作は許可される。一方、B が自分自身を追加する操作と、B が C を追加する操作は、どちらも拒否される。この規則が確認するのは追加される利用者の所属ではなく、追加操作を実行する利用者の所属である。
実際の認可処理では、所属関係を記録したデータベースの行から、利用者がどの組織に属するかを計算する場合がある。例えば、所属情報を利用者と組織の組として保存しているとする。A が G に所属していることは、利用者 A と組織 G を結び付ける所属行が存在することで表される。B について同じ行が存在しなければ、B は G のメンバーではない。許可規則は、操作する利用者に対応する所属行が存在するかを判断すればよい。
ここで、メンバー追加の処理が、新しい所属行を作成する前に認可判定を行うとする。A が B を追加する場合、追加予定の行には B と G の関係が記録されるが、操作主体である A の所属は既に成立している。このため、現在の所属関係を使っても、追加予定の行を含む所属関係を使っても、A が既存メンバーであるという判定は変わらない。追加操作はどちらの場合も許可される。
B が自分自身を追加する場合には、事情が異なる。操作前のデータベースには、B が G に所属することを示す行が存在しない。しかし、追加予定の行を仮に加えて所属関係を計算すると、B と G を結び付ける行が存在する状態になる。この状態から操作主体 B の所属を評価すれば、B は G のメンバーと判定される。許可条件の「操作する利用者が既存メンバーである」が、操作によって作成される予定の行を根拠に満たされてしまう。
この時点で、データベースへの追加が確定している必要はない。認可エンジンに渡す判定材料の中で、追加予定の行が既存の所属関係と同じように扱われれば、許可判定は反転する。直接の原因は、所属を計算する処理が提案された行を参照することにある。その背後には、判定材料を組み立てる段階で、操作前の権限と操作後に成立する権限を区別していないという構造がある。
| 判定対象 | 操作前の所属を使う場合 | 提案した所属を含める場合 |
|---|---|---|
| A が B を追加 | A は既存メンバーなので許可される。 | A は既存メンバーなので許可される。 |
| B が B を追加 | B は未所属なので拒否される。 | 追加予定の行によって B が所属済みと扱われ、許可される。 |
| B が C を追加 | B は未所属なので拒否される。 | B 自身の所属を変更しなければ、依然として拒否される。 |
三つの操作では、許可規則を固定している。A が B を追加する場合、A の既存権限によって許可が成立する。B が C を追加する場合、追加されるのは C の所属であるため、操作主体 B の権限は変化せず、拒否が維持される。B が B を追加する場合だけ、追加予定の行が操作主体自身の所属関係を変える。その結果、操作前には成立していなかった許可条件が、提案内容を反映した判定材料の中で成立する。
この反例から、許可規則の正しさと、規則へ渡す判定材料の正しさを区別できる。既存メンバーだけに追加を許可する規則は、操作前の所属を参照する限り、定められた権限境界を表している。同じ規則に操作後の所属を渡すと、追加操作によって初めて成立する権限まで許可理由に含まれる。規則の内容を固定した比較によって、判定結果の差が所属情報の構成方法に由来することを特定できる。
この失敗は、複数の利用者が同時に操作する競合状態がなくても成立する。一件の追加要求に対し、候補となる所属行を判定材料へ反映する順序だけで生じる。認可エンジンが与えられた所属関係に対して正しく規則を評価したとしても、その所属関係が操作前の権限を表しているとは限らない。権限を変更する操作の安全性を定義するには、許可判定が参照する権限と、許可後に変更される権限の関係を状態遷移として明示する必要がある。
2. 認可と状態遷移を別々に定義する
メンバー追加の例では、操作前に成立している所属関係と、追加が成功した場合に成立する所属関係を区別する必要がある。前者は操作主体が現在持つ権限を決め、後者は操作によって変更される情報を表す。両者が同じデータベースに記録されていても、認可判定における役割は異なる。操作を順に実行するシステムは、状態とその変化を分けて記述できる。Lamport の『Specifying Systems』は、システムの振る舞いを状態と遷移の関係として記述し、その性質を検証する方法を体系化している[4]。
時点 \(t\) の状態を \(S_t\)、操作主体を \(u\)、操作の種類を \(a\)、操作が提案する値を \(x\) とする。ここで \(t\) は物理時計の秒数ではなく、一つの操作が評価・確定される順序を表す添字である。状態 \(S_t\) には、現在の利用者、所属関係、リソースとその属性が含まれる。例えば、利用者 B が組織 G に所属しているかどうかは、状態 \(S_t\) に記録された所属関係によって決まる。
許可される場合を 1、拒否される場合を 0 とする認可関数 \(P\) を、次のように定義する。
\[ P(S_t,u,a,x)\in\{0,1\}. \]
この式は、状態 \(S_t\) の下で、利用者 \(u\) が操作 \(a\) を提案値 \(x\) に従って実行することを許可するかどうかを表す。メンバー追加の場合、\(u\) は追加を要求する利用者、\(a\) はメンバー追加という操作、\(x\) は追加対象の利用者と所属先の組織を指定する情報である。\(P\) が 1 を返すことは許可条件が成立したことを意味するが、データベースへの変更が完了したことまでは意味しない。
操作を実行した場合に得られる候補状態は、別の関数 \(T\) で記述する。
\[ S’=T(S_t,a,x). \]
\(T(S_t,a,x)\) は、現在の状態に操作内容を適用した場合の状態を表す。例えば、メンバー追加なら、現在の所属関係に新しい所属行を加えた状態である。この候補状態は、操作の結果を評価するために計算できるが、その計算によって実際の変更が確定するわけではない。操作が許可されても、一意制約違反や参照整合性違反、並行する操作との競合によって更新が成立しない場合がある。
必要な制約検査と実行処理が成功し、変更全体が一つの原子的な操作として確定する場合、状態遷移は次のように表せる。
\[ S_{t+1}=\begin{cases} T(S_t,a,x), & P(S_t,u,a,x)=1\ \land\ \text{実行成功},\\ S_t, & \text{拒否または変更の不成立}. \end{cases} \]
この式では、認可判定が許可を返し、実際の更新処理も成功した場合に限って、次の状態 \(S_{t+1}\) が候補状態へ変化する。それ以外の場合は、元の状態 \(S_t\) を維持する。ここでは、更新処理が成功すれば変更全体が確定し、失敗すれば変更全体が取り消されると仮定している。認可判定と変更の確定を分離することで、操作が許可されたかという判断と、操作によって状態が変化したかという結果を別々に検証できる。
組織 G に所属していない利用者 B が自分自身を追加しようとするとき、操作前の所属関係を正しく評価すれば \(P(S_t,u,a,x)=0\) となる。一方、候補状態 \(T(S_t,a,x)\) には、B が G に所属することを示す行が含まれる。候補状態に所属行が存在することは、追加後に成立する関係を表しているにすぎない。許可判定が拒否を返す限り、その候補状態への遷移は確定せず、\(S_{t+1}=S_t\) が維持される。
2.1 候補状態と判定時点の状態
認可関数が候補状態を調べること自体は、誤りを意味しない。例えば、新しい文書を作成する場合、文書の公開範囲や所属プロジェクトは、作成前には提案内容としてしか存在しない。あるプロジェクトへの文書作成が許可されているかを判断するには、作成予定の文書がどのプロジェクトに属するかを調べる必要がある。候補状態の情報を参照する理由は、作成する対象が許可条件を満たしているかを評価するためである。
一方、文書を作成する利用者がそのプロジェクトへ書き込む権限を持つかどうかは、操作前に成立している所属関係から判断する必要がある。文書の提案属性を評価することと、操作主体の権限を作成後の状態から計算することには違いがある。前者は操作の対象についての条件を確認し、後者は操作を要求する主体についての条件を確認する。両者を候補状態の同じ複製から無条件に計算すると、作成予定の情報が操作主体自身の権限を変更した場合、その変更後の権限まで許可判定に使用される。
メンバー追加の例では、この違いが判定結果に直接現れる。組織 G の既存メンバーである A が B を追加する場合、追加対象が B であるという情報は提案値として評価できる。しかし、追加を実行する A の権限は、現在の所属関係から導かなければならない。B が自分自身を追加する場合も、提案値には B を追加するという情報を含められるが、操作主体 B が既存メンバーであるかどうかは、追加前の所属関係から判断する。提案値を受け付けることと、提案値に記載された権限を既に獲得したものとして扱うことは、別の処理である。
| 判定材料 | 参照する情報 | 認可における役割 |
|---|---|---|
| 操作主体の既存権限 | 操作前の状態 \(S_t\) に成立している所属関係や権限を参照する。 | 操作を要求する利用者が、現在その操作を実行できるか判断する。 |
| 作成対象の提案属性 | 提案値 \(x\) に指定された所属先、公開範囲などを参照する。 | 作成予定の対象が、許可された属性や所属先の条件を満たすか判断する。 |
| 操作後の権限状態 | 候補状態 \(T(S_t,a,x)\) によって新たに成立する所属関係や権限を表す。 | 操作が成功した場合の結果を示す。操作前から必要な権限を証明する根拠には使用できない。 |
表の第一行と第二行は、同じ認可判定の中で必要になる情報である。ただし、情報の成立時点が異なる。操作主体の権限には、操作前から有効であることが要求される。一方、作成対象の属性は、提案された値を使って条件を評価できる。第三行の操作後の権限状態は、変更が許可されて確定した場合に成立する結果であり、操作前に必要な権限を証明するために先取りすると自己承認が発生する。
この区別によって、認可関数 \(P\) と状態遷移関数 \(T\) の役割が明確になる。\(T\) は提案された変更によって何が成立するかを表し、\(P\) は現在の権限と提案内容から、その変更を許可できるかを判断する。ただし、\(P\) の引数に \(S_t\) を指定しただけでは、内部で候補状態を使って主体の権限を再計算する実装まで排除できない。認可の安全性を検証するには、判定関数の入出力に加えて、主体の権限がどの状態から導出されるかを定義する必要がある。
3. 操作後の権限を使うと自己承認が成立する
操作後の権限を認可判定に使用すると、どのような条件で自己承認が成立するのかを集合で表す。利用者の集合を \(U\)、組織の集合を \(H\) とし、時点 \(t\) の所属関係を \(M_t\subseteq U\times H\) とする。\((u,g)\in M_t\) は、利用者 \(u\) が組織 \(g\) に所属していることを意味する。例えば、組織 G に所属する利用者が A だけであれば、所属関係には A と G の組が含まれ、未所属の利用者 B と G の組は含まれない。
既存メンバーだけが同じ組織へ新しいメンバーを追加できるという規則を考える。操作主体を \(u\)、追加される利用者を \(v\)、追加先の組織を \(g\) とする。この規則では、追加される利用者 \(v\) の所属状況にかかわらず、操作主体 \(u\) が既に組織 \(g\) に所属していることを要求する。操作前の所属関係を使う許可判定は、次のように定義できる。
\[ P_{\mathrm{pre}}(M_t,u,v,g)=\mathbf{1}\!\left[(u,g)\in M_t\right]. \]
\(\mathbf{1}[Q]\) は、条件 \(Q\) が真なら 1、偽なら 0 を返す関数である。添字の \(\mathrm{pre}\) は、操作前の所属関係を評価することを示す。この式では、操作主体 \(u\) が組織 \(g\) の既存メンバーなら許可を返す。追加対象 \(v\) が誰であるかは、この許可規則の真偽を変えない。追加対象の存在や所属行の重複といった制約は、認可とは別に検査されるものとする。
組織 \(g\) に所属していない利用者 \(b\) が、自分自身を追加する操作を要求したとする。操作前には \((b,g)\notin M_t\) が成立しているため、正しい許可判定は次のようになる。
\[ P_{\mathrm{pre}}(M_t,b,b,g)=0. \]
一方、追加操作を適用した場合の候補状態では、利用者 \(b\) と組織 \(g\) の所属関係が新しく作られる。候補となる所属関係を \(M’\) とすると、次の集合になる。
\[ M’=M_t\cup\{(b,g)\}. \]
誤った実装では、操作前の所属関係 \(M_t\) の代わりに、この候補状態 \(M’\) を認可判定へ渡す。この場合、追加予定の所属行が存在するという情報から、操作主体 \(b\) が組織 \(g\) のメンバーであると判定される。
\[ \begin{aligned} P_{\mathrm{post}}(M_t,b,b,g) &=\mathbf{1}\!\left[(b,g)\in M’\right]\\ &=\mathbf{1}\!\left[(b,g)\in M_t\cup\{(b,g)\}\right]\\ &=1. \end{aligned} \]
操作前には存在しなかった所属関係が、操作の候補状態に含まれたことで、許可条件を満たしている。直接の原因は、所属行を追加した候補状態を使って、操作主体の権限を再計算したことである。その結果、まだ許可されていない操作によって成立するはずの所属関係が、その操作を許可する根拠になった。許可判定と状態遷移の順序が、判定材料の構成を通じて逆転している。
この現象は、自分自身を追加する場合に特有の条件として一般化できる。追加される利用者を \(v\) として、候補状態から操作主体の所属を判定する関数を次のように定義する。
\[ P_{\mathrm{post}}(M_t,u,v,g)=\mathbf{1}\!\left[(u,g)\in M_t\cup\{(v,g)\}\right]. \]
集合に \((v,g)\) を追加したとき、\((u,g)\) が含まれる条件は二つある。一つは、操作主体 \(u\) が元から組織 \(g\) に所属している場合である。もう一つは、操作主体 \(u\) と追加対象 \(v\) が同一である場合である。この関係は次の同値式で表せる。
\[ P_{\mathrm{post}}(M_t,u,v,g)=1\iff (u,g)\in M_t\ \lor\ u=v. \]
右辺の \(\lor\) は、いずれか一方の条件が成立すれば真になることを意味する。本来の許可規則が要求するのは左側の既存所属だけである。しかし、候補状態を使った判定では、右側の \(u=v\) という条件が新たに加わっている。これにより、操作主体が既存メンバーかどうかに関係なく、自分自身を追加する操作が許可される。
| 操作前の所属 | 操作主体と追加対象 | 操作前の判定 | 候補状態を使った判定 |
|---|---|---|---|
| \((u,g)\in M_t\) | \(u=v\) または \(u\neq v\) | 既存メンバーなので許可される。 | 既存の所属関係によって許可される。 |
| \((u,g)\notin M_t\) | \(u\neq v\) | 未所属なので拒否される。 | 追加対象が別人なので、操作主体の所属は変わらず拒否される。 |
| \((u,g)\notin M_t\) | \(u=v\) | 未所属なので拒否される。 | 追加予定の所属行によって操作主体自身の所属が成立し、許可される。 |
表の第三行では、操作主体と追加対象が同一であるという条件だけで判定が反転する。操作前の所属関係にどのような別のメンバーが存在していても、追加予定の行に \((u,g)\) が含まれれば、候補状態に対する所属判定は必ず真になる。元の許可規則には存在しなかった「自分自身を追加するなら許可する」という条件が、判定材料の組み立て方によって事実上追加されたことになる。
この反例は、一つの追加要求だけで成立する。二つの要求の競合、非同期処理、ネットワークの遅延はいずれも必要ない。所属関係を組み立てる時点で提案行を含め、その所属関係を操作主体の権限判定へ渡すだけで発生する。認可規則を評価する処理が与えられた集合について正しく動いていても、その集合が操作前の権限を表していなければ、意図された許可条件とは異なる結果が生じる。
3.1 権限を変更する操作には別の許可根拠が要る
メンバー追加は、所属行を作成するデータ操作であると同時に、その利用者が実行できる操作の範囲を変更する権限管理でもある。例えば、組織 G の文書を編集できる条件が G への所属である場合、新しい所属行を作成すると、その利用者には文書を編集する権限も生じる。所属行の作成を許可することは、所属後に認められる一連の操作を可能にする判断でもある。
このため、権限を変更する操作には、変更後の権限とは独立した許可根拠を定める必要がある。例えば「組織の管理者だけがメンバーを追加できる」という規則なら、操作主体が追加前から管理者権限を持っていることを確認する。Cedar の公式設計指針も、通常のリソース操作に加え、権限そのものを変更する操作への許可を認可モデルに含める考え方を示している[5]。権限変更を実行できる主体と、その変更によって権限を得る主体を分けて考えることで、変更結果を許可根拠として先取りする循環を防げる。
自己追加が業務上認められる場合には、別の許可条件を設けられる。例えば、組織が発行した招待リンクによる登録なら、招待の有効期限、対象組織、利用回数などを確認し、条件を満たした利用者の登録を許可する設計が考えられる。これらの条件は、登録操作によって新たに獲得する所属権限とは独立して検証できる。自己登録を許可することと、自己登録によって成立する権限を使って登録を正当化することは、異なる認可規則である。
集合による反例から、自己承認の成立条件を具体的に特定できる。所属関係を変更する提案が、操作主体自身の所属判定に反映されると、既存メンバーだけに操作を許可する規則へ、自己追加を無条件に許可する条件が混入する。権限の変更を安全に扱うには、操作前に成立している許可根拠と、操作によって新たに成立する権限を分離しなければならない。この区別は、所属行の追加に限らず、管理者への昇格、役割の付与、アクセス権限の変更にも適用できる。
4. 既存権限と提案属性を分離する
自己承認を防ぐには、操作前の権限を使って許可を判断する必要がある。しかし、認可判定に使用するすべての情報を操作前の状態に限定すると、新しいリソースを作成する操作を適切に評価できなくなる。例えば、文書を作成する場合、その文書が所属するプロジェクトや公開範囲は、作成前のデータベースには存在しない。これらの情報は利用者が提出した提案内容に含まれており、作成を許可するか判断するために必要となる。Cedar の公式資料でも、リソースの作成を既存リソースの読み取りや更新とは異なる認可パターンとして扱っている[6]。
組織 G に所属する利用者だけが、G に文書を作成できるという規則を考える。利用者 A が G に所属しているかどうかは、操作前の所属関係から判断できる。一方、作成予定の文書が G に属するかどうかは、提出された文書の属性を確認しなければ分からない。前者は操作主体が現在持っている権限の情報であり、後者は作成しようとしている対象の情報である。両者は同じ許可判定に必要だが、その成立時点と役割が異なる。
この違いを数理モデルで表す。現在の状態 \(S_t\) から利用者 \(u\) の権限関係を計算する関数を \(G(S_t,u)\) とし、現在の状態、操作 \(a\)、提案値 \(x\) から審査対象のリソースを構成する関数を \(R(S_t,a,x)\) とする。これらを入力として許可を決める関数を \(F\) とすると、認可判定は次のように記述できる。
\[ P^*(S_t,u,a,x)=F\!\left(G(S_t,u),a,R(S_t,a,x),x\right). \]
この式で \(G(S_t,u)\) は、操作前の状態から導出される主体の権限を表す。\(R(S_t,a,x)\) は、作成対象の属性など、操作の提案内容を反映したリソースの表現である。\(F\) は、主体の権限、操作の種類、対象の属性、提案値を照合して許可を判断する。許可判定に異なる時点の情報を使用していても、それぞれが何を表し、どの条件を評価するために使用されるかが明確であれば、認可規則を定義できる。
文書作成の例を具体化する。利用者 \(u\) が組織 \(g\) に所属していることを \((u,g)\in M_t\) で表し、提案値 \(x\) に指定された文書の所属先を \(g(x)\) とする。また、公開範囲などの提案属性が作成条件を満たす場合に 1 を返す関数を \(C(x)\) とする。このとき、文書作成の許可条件は次のように表せる。
\[ P_{\mathrm{create}}(M_t,u,x)=\mathbf{1}\!\left[(u,g(x))\in M_t\right]\cdot C(x). \]
右辺の第一項は、利用者 \(u\) が文書の作成先として指定された組織に既に所属しているかを評価する。第二項は、提案された文書の属性が作成条件を満たしているかを評価する。二つの値はそれぞれ 0 または 1 なので、積が 1 になるのは両方の条件が成立した場合だけである。利用者が組織に所属していても、許可されていない公開範囲の文書を作ろうとすれば拒否される。また、提案された文書の属性が適切でも、利用者が作成先の組織に所属していなければ拒否される。
この判定では、作成予定の文書が組織 G に属するという提案を評価しているが、その提案によって利用者自身が G のメンバーになったとは扱っていない。提案属性は作成対象の条件を確かめるために使用され、操作主体の権限は既存の所属関係から導出される。提案された値を認可に利用することと、提案によって生じる権限を既存権限として利用することの違いが、この構造に現れる。
メンバー追加の場合も、追加対象の利用者と所属先の組織は提案値から判断できる。例えば、利用者 A が B を組織 G に追加する要求では、B と G の組を作成対象として認可エンジンへ渡せる。A が B を追加する場合、提案行によって A 自身の所属は変化しない。一方、未所属の B が B 自身を追加する場合、提案行を反映した所属関係から B の権限を再計算すると、B が既存メンバーであると判定される。第 3 章の反例では、追加予定の所属行を含む集合から操作主体の所属を評価した結果、既存メンバーであるという条件が提案内容だけで成立した。
| 判定材料 | 参照する情報 | 許可判定における役割 |
|---|---|---|
| 操作主体の所属 | 操作前の状態 \(S_t\) に確定している所属関係を参照する。 | 操作主体が現在その組織に対する権限を持っているか判断する。 |
| 作成予定の文書 | 提案値 \(x\) に指定された所属先や公開範囲を参照する。 | 作成対象の属性が、許可された条件を満たしているか判断する。 |
| 追加予定のメンバー | 提案値 \(x\) に指定された利用者と所属先の組織を参照する。 | 誰をどの組織へ追加する要求なのかを特定し、対象に関する条件を評価する。 |
| 追加によって生じる所属 | 許可された変更が確定した後の状態 \(S_{t+1}\) に成立する所属関係を参照する。 | 変更確定後の要求について、新たな権限を計算する材料となる。 |
表の第一行と第四行は、いずれも利用者の所属を表すが、認可に使用できる時点が異なる。操作主体の既存所属は、変更を許可するための根拠となる。一方、追加によって生じる所属は、変更が確定した後の権限関係を表す。例えば、利用者 B が正当な権限を持つ管理者によって G に追加されれば、確定後の要求では B の所属を権限計算に利用できる。しかし、B を追加する操作そのものを許可する際には、その結果として成立する所属を既存の許可根拠として使えない。
この時間的な区別は、認可要求の情報を役割ごとに整理することとも関係する。Cedar の設計指針では、主体、操作、対象に属する情報と、個別の要求に固有の文脈情報を区別することが推奨されている[7]。ただし、情報を異なる項目へ配置するだけで、その成立時点まで保証されるわけではない。所属行から主体の権限を組み立てる実装では、どの状態の所属行を参照するかによって、同じ主体に対する判定結果が変わる。
例えば、認可エンジンへ渡す判定材料を作る際、追加予定の所属行を含む状態からすべての利用者の所属関係を再計算すると、操作主体が追加対象と一致する場合に権限が先取りされる。これを避ける実現方法の一つは、提案された行を作成対象の情報として反映しながら、操作主体の既存権限を操作前の所属関係から計算することである。作成対象の情報を評価する経路と、主体の権限を評価する経路を分離すれば、提案属性を使った認可と自己承認の防止を両立できる。
ただし、関数の入力を分離しただけで、業務上要求される許可条件が自動的に成立するわけではない。どの利用者に権限変更を認めるか、どの提案属性を許可するかは、業務仕様として定義する必要がある。数理モデルの役割は、現在の権限に基づく条件と、作成対象の提案内容に基づく条件を区別し、それぞれがどの状態から導出されるかを明示することにある。
5. 認可の安全性を状態遷移の性質として定義する
操作前の権限と提案属性を分離すると、自己承認が発生する経路を制限できる。しかし、判定材料を適切に分離したことと、認可の安全性が成立することは同じではない。例えば、現在の所属関係を正しく参照していても、業務仕様では管理者だけに認められる操作を一般メンバーにも許可する規則であれば、権限外の操作が実行される。認可の安全性を検証するには、どの操作が許可されるべきかという要求仕様を、実装された判定から独立して定義する必要がある。
要求仕様に基づく許可条件を \(A(S,u,a,x)\)、実装された認可関数を \(P_{\mathrm{impl}}(S,u,a,x)\) とする。\(S\) は判定時点の状態、\(u\) は操作主体、\(a\) は操作の種類、\(x\) は提案内容である。どちらの関数も、許可する場合に 1、拒否する場合に 0 を返す。ただし、二つの関数は異なる役割を持つ。\(A\) は業務上許可すべき操作の範囲を定義し、\(P_{\mathrm{impl}}\) は実際のシステムがどのように判断するかを表す。
例えば、組織 G の既存メンバーだけが新しいメンバーを追加できるという要求仕様なら、操作前の所属関係に操作主体が含まれることを許可条件として定義する。一方、実装された判定関数が追加予定の所属行を反映した状態を参照する場合、要求仕様と実装の間に差が生じる。二つの関数を独立して定義することで、同じ要求に対する判断が一致するかを検証できる。
権限外の操作を許可しないための安全性条件は、次の含意で表せる。
\[ \forall S,u,a,x,\quad P_{\mathrm{impl}}(S,u,a,x)=1 \;\Longrightarrow\; A(S,u,a,x)=1. \]
記号 \(\forall\) は、指定したすべての状態、利用者、操作、提案内容について条件が成立することを表す。\(\Longrightarrow\) は、左側が成立した場合に右側も成立しなければならないという含意である。この式では、実装が許可を返したすべての要求について、要求仕様も許可を認めていることを求める。実装が許可した操作の集合が、要求仕様の許容範囲に含まれるという条件である。
第 3 章の自己承認を、この安全性条件に当てはめる。組織 \(g\) に所属していない利用者 \(b\) が自分自身を追加する場合、操作前の所属関係 \(M_t\) には \((b,g)\) が存在しない。要求仕様が既存メンバーだけに追加を認めるなら、許可条件は次のようになる。
\[ A(M_t,b,\mathrm{addMember},(b,g))=0. \]
しかし、実装が追加予定の所属行を含む候補状態から操作主体の所属を計算すると、実装の判定結果は次のようになる。
\[ P_{\mathrm{impl}}(M_t,b,\mathrm{addMember},(b,g))=1. \]
同じ状態、利用者、操作、提案内容について、実装は 1 を返すが、要求仕様は 0 を返している。安全性条件の左側が真、右側が偽になるため、含意は成立しない。この一つの反例によって、すべての入力について安全性が成立するという主張を否定できる。反例が示しているのは、認可規則の評価に失敗したことではなく、実装が許可の根拠として使用した所属関係が、要求仕様の定める操作前の所属関係と異なることである。
ここで、要求仕様を実装された認可関数から独立して定義する必要性が明確になる。仮に \(A=P_{\mathrm{impl}}\) と定義すると、安全性条件は次の式に変わる。
\[ P_{\mathrm{impl}}(S,u,a,x)=1 \;\Longrightarrow\; P_{\mathrm{impl}}(S,u,a,x)=1. \]
この式は、実装がどのような許可判定を行っていても成立する恒真式である。操作後の所属を先取りして自己承認を許可する実装についても、同じ式が成立する。形式的な証明が正しくても、証明対象の許可条件を実装の振る舞いと同一に定義していれば、業務上の権限境界を守っているかは判定できない。証明に使用する許可条件が、要求仕様として独立に定義されていることが必要になる。
なお、この安全性条件は、許可された操作の範囲が要求仕様を超えないことを表している。要求仕様で許可される操作を、実装も必ず許可するという条件は別に定義できる。
\[ \forall S,u,a,x,\quad A(S,u,a,x)=1 \;\Longrightarrow\; P_{\mathrm{impl}}(S,u,a,x)=1. \]
前者は権限外の操作を許可する誤りを排除する条件であり、後者は許可されるべき操作を不必要に拒否する誤りを排除する条件である。例えば、すべての操作を拒否する実装は前者を満たすが、後者を満たすとは限らない。二つの条件を分けることで、権限境界の保護と、正当な操作の受理を個別に評価できる。
5.1 状態遷移へ適用する安全性条件
実際のシステムでは、一つの要求に対して認可判定が行われ、その結果に応じてデータベースの読み取りや変更が実行層へ発行される。認可関数が許可を返したという事実と、操作が実行層へ発行されたという事実は区別できる。例えば、認可後の制約検査で変更が拒否される場合、許可判定は成立していても、変更操作は発行されない場合がある。反対に、認可処理を迂回する経路が存在すれば、認可関数の返り値とは無関係に操作が発行される可能性もある。
そこで、状態 \(S\) において利用者 \(u\) の操作 \(a\) と提案値 \(x\) に対応する操作が実行層へ発行されたことを、述語 \(\operatorname{Issued}(S,u,a,x)\) で表す。述語とは、指定された条件が成立するときに真となる論理式である。ここでは、操作が実行層へ渡されたことを表し、変更がデータベースへ正常に確定したかどうかは別の結果として扱う。
発行された操作が要求仕様の許容範囲を超えないための条件は、次のようになる。
\[ \forall S,u,a,x,\quad \operatorname{Issued}(S,u,a,x) \;\Longrightarrow\; A(S,u,a,x)=1. \]
この式は、実行層へ発行されたすべての操作について、発行時点の状態を用いた要求仕様の許可条件が成立していることを要求する。認可関数自体の正しさを確認するだけでなく、実際に発行される操作が認可の対象から漏れていないことも検証する条件である。認可関数が正しくても、実行層へ到達する別の経路があれば、この性質は破られる可能性がある。
複数の操作を順に処理する場合、各操作の許可は、その操作の直前に成立している状態について評価する。状態列を \(S_0,S_1,\ldots,S_n\)、各段階で発行される操作を \(a_t\)、操作主体を \(u_t\)、提案値を \(x_t\) とすると、要求される条件は次のように記述できる。
\[ \forall t,\quad \operatorname{Issued}(S_t,u_t,a_t,x_t) \;\Longrightarrow\; A(S_t,u_t,a_t,x_t)=1. \]
例えば、管理者 A が利用者 B を組織 G に追加する操作を正当に実行し、その変更が確定したとする。最初の操作では、B が所属する前の状態 \(S_t\) を使って A の追加権限を評価する。追加が確定した後、B が G の文書を編集する操作では、新しい所属を反映した状態 \(S_{t+1}\) を使って B の編集権限を評価できる。この二つの判定は異なる時点の状態を参照するが、各操作の直前に確定した情報を使用するという条件は共通している。
一方、A による追加が拒否された場合や、制約違反によって確定しなかった場合には、B の所属は成立していない。後続の編集要求でも、B をメンバーとして扱う根拠は存在しない。権限変更が許可されたこと、権限変更が確定したこと、その結果を後続の認可に使用できることは、それぞれ異なる条件である。
| 検証対象 | 成立させる条件 | 検出する誤り |
|---|---|---|
| 認可判定の安全性 | 実装が許可したすべての操作を、独立した要求仕様も許可している。 | 候補状態の権限を先取りするなど、要求仕様の許容範囲を超えた許可を検出する。 |
| 認可判定の完全性 | 要求仕様が許可する操作を、実装も許可する。 | 正当な利用者や操作を不必要に拒否する判定を検出する。 |
| 発行操作の安全性 | 実行層へ発行されたすべての操作が、発行直前の状態について要求仕様を満たす。 | 認可処理の迂回や、許可された操作と実際に発行された操作の不一致を検出する。 |
| 状態遷移の整合性 | 許可され正常に確定した変更だけが次の状態へ反映され、拒否または失敗した変更は状態に残らない。 | 拒否された変更の反映や、変更確定前の権限を後続操作へ使用する誤りを検出する。 |
表の各条件は、互いに異なる性質を評価している。認可判定が要求仕様に一致していても、実行層が認可されていない操作を発行すれば、発行操作の安全性は成立しない。また、正当に発行された操作であっても、変更の確定に失敗した場合、その結果を後続の状態へ反映すれば状態遷移の整合性が破られる。認可関数、操作の発行、変更の確定を分離して検証する理由は、それぞれ異なる経路で権限境界が破られる可能性があるためである。
これらの条件は、権限外の操作が発行されることを防ぐための性質を中心としている。実行層へ発行された操作が外部データベースで意図どおり実行されること、承認された操作が必ず成功すること、拒否結果や応答時間から情報が漏えいしないこと、外部サービスへ送信した情報にも同じ保護が及ぶことは、それぞれ追加の仕様と検証を必要とする。状態遷移モデルが表現する範囲と、現実の実行環境が保証する範囲を対応付けることで、証明済みの性質を具体的な安全性要求として評価できる。
自己承認の反例が示すのは、許可条件を評価する処理が正しくても、その条件がどの状態を参照するかによって、要求仕様との一致が失われるという事実である。認可の安全性を証明するには、操作前の権限を用いるという要求を独立した許可条件として定義し、実装の判定と発行された操作がその条件を満たすことを示す必要がある。形式的な証明が成立しているかという判断と、証明された性質が要求された権限境界を表しているかという判断は、このように区別できる。
6. Nyxis の認可判定は、どの状態を参照していたか
第 3 章で導いた自己承認は、操作によって新たに成立する所属関係を、その操作自身の許可判定に使用することで発生する。集合モデルでは、操作前の所属関係 \(M_t\) と、提案された行を含む候補状態 \(M’\) を区別することで、この違いを表現した。実際の認可フレームワークでは、データベースの行から認可エンジンが参照するエンティティを構成するため、その構成処理がどの状態を参照しているかを調べる必要がある。
Lean 4 で実装された Nyxis は、Cedar のポリシー評価を使用するバックエンドフレームワークである。Cedar に渡す認可要求には、操作主体、操作、対象、文脈が含まれる。一方、判定に使用するエンティティには、利用者やリソースの属性と、それらの間に成立する所属関係が含まれる。Nyxis はデータベースの行からこれらの情報を組み立て、Cedar による許可判定へ渡す。
Nyxis/Authz.lean の judgementEntities は、認可判定に使用するエンティティ全体を構成する関数である。PR #3 が対象とした修正前の実装では、挿入対象の行が存在せず、その対象が操作主体自身のエンティティと異なる場合、store.put によって提案行を加えた状態からエンティティを構成する[8]。この処理によって、まだデータベースへ保存されていない作成対象についても、提案された属性を用いて許可条件を評価できる。
例えば、新しい文書を作成する場合、文書の所属プロジェクトや公開範囲は提案内容から取得する必要がある。そのため、提案された文書を判定対象のエンティティとして構成することには合理性がある。しかし、メンバーの追加では、作成予定の行が別の意味も持つ。所属行は追加対象を表すと同時に、利用者がどの組織やチームに所属するかを決める情報でもある。提案された所属行をエンティティの構成に反映すると、その行によって操作主体の権限関係まで変化する可能性が生じる。
この関係を構成するのが、Nyxis/Materials.lean の membershipRefs である。この関数は、指定されたエンティティに対応する所属行を検索し、その行が参照する組織やチームを祖先関係として取り出す。ここでいう祖先関係は、Cedar の所属判定に使用するエンティティ間の関係である。例えば、利用者が特定のチームに所属していれば、そのチームが利用者の祖先として表現され、ポリシーの所属条件を評価する材料になる[9]。
judgementEntities が提案行を加えた状態を構成し、その状態を membershipRefs が参照すると、作成予定の所属行も検索対象に含まれる。所属行に操作主体自身の識別子が指定されていれば、その行から操作主体の新しい祖先関係が導出される。直接の原因は、所属関係を計算する時点で追加予定の行が存在することである。その背後には、作成対象の提案属性と、操作主体が既に持っている権限を、同じ候補状態から構成しているという設計上の関係がある。
judgementEntities には、挿入対象が操作主体自身のエンティティである場合に、提案行の反映を避ける条件が設けられている。しかし、所属行は利用者自身のエンティティとは別の行として保存される。挿入対象の識別子が操作主体の識別子と異なっていても、その行が操作主体の所属関係を変更することはある。エンティティ自身への直接的な変更を制限する条件だけでは、別の行を介して生じる権限変更まで制限できない。
6.1 提案行が主体の所属へ回り込む経路
Nyxis の PR #3 では、所属行の追加によって自己承認が成立する再現例と、その修正方法が示されている[10]。再現例では、利用者 Bob は acme-vw と zen-ed というチームに所属しているが、acme-ed には所属していない。この状態で、Bob が自分自身を acme-ed のメンバーとして追加する操作を要求する。提案された所属行には、利用者 Bob、チーム acme-ed、組織 acme を表す識別子が含まれる。
対象となる許可条件は、操作主体が追加先のチームに所属している場合に、メンバー追加を認めるものである。Cedar では principal in resource.team という条件によって表現される。principal は操作を要求する利用者、resource.team は作成対象の所属行が指定するチームを表す。Bob は操作前に acme-ed のメンバーではないため、現在の所属関係を使って評価すれば、この条件は偽になる。
ところが、追加予定の所属行を含む状態からエンティティを構成すると、Bob の祖先関係に acme-ed が含まれる。membershipRefs が参照する所属行の集合に、Bob 自身を acme-ed へ追加する提案が含まれるためである。その結果、principal in resource.team は真となり、既存メンバーだけにメンバー追加を許可する規則の下で、未所属の Bob による自己追加が認められる。
この経路は、第 3 章の集合モデルに対応している。操作前の状態では \((b,g)\notin M_t\) が成立する。一方、提案された所属行を反映した候補状態は \(M’=M_t\cup\{(b,g)\}\) であり、そこから所属を計算すると \((b,g)\in M’\) が成立する。Cedar の評価器は、与えられたエンティティの所属関係に従って条件を評価している。許可判定が意図した結果と異なる原因は、評価器へ渡す所属関係の構成にある。
PR #3 の報告では、この所属関係の変化によって Bob の自己追加が許可され、追加後には acme の文書に対する編集操作も可能になることが示されている。所属行の追加は、一件のデータ作成操作として現れる。しかし、所属関係を参照する別の許可規則が存在する場合、その操作は後続の読み取りや変更の権限にも影響する。追加される行の内容だけでなく、その行から導出される権限の範囲まで確認する必要がある。
6.2 作成対象の属性と主体の権限を別の状態から構成する
PR #3 で提示された修正方法は、作成予定の所属行を判定材料から除外するものではない。作成対象のエンティティには提案行の属性を反映しながら、所属行から導出される祖先関係には操作前の状態を使用する。具体的には、エンティティの行データを構成するための状態と、所属関係を計算するための状態を別々に受け取れるようにする。これにより、作成対象の情報と既存主体の権限を、それぞれ適切な時点から取得できる。
この構成では、作成予定の所属行がどの利用者をどのチームへ追加するかを判定できる。一方、その行が実際に作成される前から、操作主体が追加先のチームに所属しているものとして扱うことは避けられる。対象の属性を評価するために必要な提案内容を維持しながら、操作主体の権限に関しては操作前の所属関係を保持する方法である。
| 判定材料 | 提案行を所属関係にも反映する構成 | 所属関係を操作前に固定する構成 |
|---|---|---|
| 作成対象のエンティティ | 提案された所属行を含む状態から構成し、作成対象の属性を評価する。 | 提案された所属行を含む状態から構成し、作成対象の属性を引き続き評価する。 |
| 操作主体の所属関係 | 提案行を反映した状態から計算するため、操作主体自身の新しい所属が含まれる場合がある。 | 操作前の状態から計算し、既存の所属関係を許可判定の根拠とする。 |
| 未所属の利用者による自己追加 | 追加予定の所属行によって主体の所属条件が成立し、操作が許可される。 | 既存メンバーに限定するポリシーでは、操作前の所属条件が成立せず拒否される。 |
| 既存メンバーによる追加 | 操作前から成立している所属関係によって許可条件を満たす。 | 操作前から成立している所属関係によって許可条件を満たす。 |
表の第一行では、両方の構成が提案された所属行を作成対象として評価している。一方、第二行では、操作主体の所属関係をどの状態から導出するかが異なる。この差によって、第三行の自己追加に対する判定が変わる。第四行のように操作主体が既に権限を持っている場合には、提案行を使って権限を獲得する必要がないため、既存の所属関係だけで許可条件を満たせる。
この違いは、第 4 章で定義した \(G(S_t,u)\) と \(R(S_t,a,x)\) の分離によって説明できる。操作主体の権限を表す \(G\) には操作前の状態を使用する。一方、作成対象を表す \(R\) には、認可に必要な範囲で提案値を反映する。二つの情報は同じ認可判定で使用されるが、異なる状態から構成される。判定材料の生成過程でこの区別を維持することが、自己承認を排除する条件になる。
PR #3 には、自己追加が拒否され、操作が発行されず、状態も変更されないことを確認する回帰テストが含まれている。修正前の実装では追加したテストの一部が失敗し、修正後には成功したと報告されている。また、判定材料の構成方法を変更したことに伴い、エンティティの整合性や認可判定に関係する証明も調整されている。これらの検証は、提案行の扱いを変更しても作成対象の属性を評価できることと、操作主体の所属関係が提案行によって変化しないことを確認するためのものである。
公開された再現例と修正内容から、自己承認を生む条件と、その条件を取り除く方法を具体的に確認できる。ただし、報告された回帰テストの成功は、そのテストで評価した条件についての結果である。外部データベースとの接続や実行環境を含めた安全性については、それらの境界に対応する検証が別途必要になる。認可判定の内部で成立する性質と、実際のシステム全体で成立する性質は、保証の対象を区別して評価する必要がある。
Nyxis の事例で確認できるのは、操作主体自身のエンティティを直接変更しなくても、別の所属行を通じてその主体の権限関係が変化するという構造である。権限が複数のデータから導出される場合、操作対象の行と操作主体のエンティティが異なることだけでは、主体の権限が変化しないことを保証できない。判定材料を構成する際には、提案された変更がどのエンティティの属性や所属関係へ影響するかを確認し、操作前から成立している権限と操作後に生じる権限を分離する必要がある。
7. 形式証明が成立しても、要求した安全性が成立するとは限らない
認可の安全性を形式的に証明するには、システムが満たすべき性質を論理式として定義し、その性質がすべての対象となる実行について成立することを示す必要がある。例えば、発行されたデータベース操作が必ず許可済みであるという性質を証明できれば、認可処理を経由せずに操作が発行される経路を、証明対象のモデル内で排除できる。しかし、ここでいう「許可済み」が何を意味するかは、証明に使用する定義によって決まる。許可の定義が業務上要求される権限境界と異なっていれば、定理が成立していても、要求された安全性を満たしているとは限らない。
Nyxis の Runtime.authorization_safety は、この違いを考えるための具体例となる。この定理は、純粋なランタイムモデルにおける任意のアプリケーション、初期状態、認証済み要求列について、発行された操作が認可された効果の範囲内にあることや、状態遷移が操作の記録と整合することなどを証明している[11]。ここでいう純粋モデルは、要求の処理、認可判定、操作の発行、状態の変化を Lean 上の定義として記述したものである。実際のデータベースや外部サービスの動作を直接観測して証明するのではなく、定義された処理の性質を論理的に検証する。
発行された操作が許可済みであるという性質は、Nyxis.Authz.Authorized によって表される。この述語は、操作に対応する効果がスキーマで宣言されていること、発行された操作がその効果の範囲内にあること、Cedar の認可判定が許可を返すことを要求する。つまり、操作が単に Cedar のポリシーで許可されるだけでなく、宣言された効果の種類にも適合していることを確認する。
ただし、Authorized が使用する Cedar の判定材料は、Nyxis.Authz.judgementEntities によって構成される。第 6 章で確認した所属行の自己追加では、この構成処理が提案行を含む状態から操作主体の所属関係を導出した。その結果、まだ成立していない所属が既存の権限として評価され、Cedar の判定は許可を返した。Authorized は同じ判定材料を使用するため、この許可結果も定義上は正当な権限の範囲に含まれる。
この構造では、ランタイムが Authorized を満たす操作だけを発行するという定理と、業務上は拒否されるべき自己追加が許可されるという現象が両立する。定理が誤った結論を導いているわけではない。証明に使用された許可の定義が、操作後の所属を判定材料へ含める構成になっていたためである。証明が成立していることと、その証明が意図された権限境界を表していることは、別々に確認する必要がある。
形式的に検証された認可言語は、このような問題を考えるうえでも有用である。Cedar の研究では、認可言語の意味論とポリシー解析の性質を形式的に扱い、許可判定や静的検証を数学的に分析している[12]。また、Cedar の開発過程を扱った研究では、形式仕様についての証明と、実装がその仕様に一致することを確認する差分テストなどを組み合わせている[13]。これらの方法は、評価器が定義された意味論に従うことを検証するために役立つ。一方、アプリケーションが評価器へ渡すエンティティの構成と、業務上の許可条件との対応は、そのアプリケーションの仕様に照らして確認する必要がある。
7.1 モデルが証明する許可と、要求仕様の許可
この違いを、第 5 章で導入した安全性条件に対応させる。モデルで定義された許可条件を \(A_{\mathrm{model}}(S,u,a,x)\)、業務上要求される許可条件を \(A_{\mathrm{req}}(S,u,a,x)\) とする。\(S\) は操作直前の状態、\(u\) は操作主体、\(a\) は操作の種類、\(x\) は提案内容である。どちらも許可される場合に 1、拒否される場合に 0 を返すが、前者は検証対象のモデルに定義された条件、後者はモデルの実装方法とは独立に定めた要求仕様を表す。
実行層へ操作が発行されたことを \(\operatorname{Issued}(S,u,a,x)\) と表す。発行された操作がモデル上の許可条件を満たすという性質は、次のようになる。
\[ \forall S,u,a,x,\quad \operatorname{Issued}(S,u,a,x)\Longrightarrow A_{\mathrm{model}}(S,u,a,x)=1. \]
この式は、モデルに従って発行される操作が、モデル自身の許可条件から逸脱しないことを要求する。Nyxis の Runtime.authorization_safety が保証する認可済み操作の発行は、この関係に対応する。ただし、実際の定理には、操作主体と要求主体の一致、宣言された効果への適合、状態遷移の整合性なども含まれる。ここでは、要求仕様との関係を考えるため、発行操作の許可に関する部分を抽出している。
業務上の権限境界を守っていると結論付けるには、もう一つの条件が必要になる。モデルが許可した操作は、要求仕様でも許可されるという条件である。
\[ \forall S,u,a,x,\quad A_{\mathrm{model}}(S,u,a,x)=1\Longrightarrow A_{\mathrm{req}}(S,u,a,x)=1. \]
この含意が成立すれば、モデル上で許可される操作の範囲は、要求仕様が許容する範囲に含まれる。さらに、発行された操作が必ずモデル上の許可条件を満たすことが証明されていれば、二つの含意をつなげられる。
\[ \operatorname{Issued}(S,u,a,x)\Longrightarrow A_{\mathrm{model}}(S,u,a,x)=1\Longrightarrow A_{\mathrm{req}}(S,u,a,x)=1. \]
この式の左側から中央までは、発行操作とモデルの整合性を表す。中央から右側までは、モデルの許可条件と要求仕様の整合性を表す。両方が成立して初めて、発行された操作が業務上の権限境界を超えないという結論を導ける。前者を形式的に証明できても、後者が未検証であれば、モデルで許可された操作が業務上も許可されるとは判断できない。
自己承認の反例では、後者の含意が破れる。組織 \(g\) に所属していない利用者 \(b\) が、自分自身を追加する操作を考える。業務仕様は既存メンバーだけに追加を許可するため、操作前の所属関係を使った要求仕様の判定は 0 になる。一方、提案行を含む状態から主体の所属を計算するモデルでは、許可判定が 1 になる。
\[ \begin{aligned} A_{\mathrm{model}}(M_t,b,\mathrm{addMember},(b,g))&=1,\\ A_{\mathrm{req}}(M_t,b,\mathrm{addMember},(b,g))&=0. \end{aligned} \]
この反例により、モデル上の許可が要求仕様上の許可を含意するという性質は成立しないことが分かる。実装がモデルに忠実であっても、モデルの許可条件が操作後の所属を先取りしている限り、自己追加を許可する判断が再現される。形式証明の対象となる定義そのものに、要求仕様との差が存在しているのである。
既稿「証明はいつ数学的知識になるのか」では、命題が形式的に検証されたことと、その成果を理解し、適切な対象へ適用できることを異なる条件として整理した[14]。認可の安全性では、この違いをモデルと要求仕様の間の含意として具体化できる。証明された命題の正しさは維持されるが、その命題を業務上の安全性へ適用するには、許可条件の意味が一致していることを示す必要がある。
7.2 証明の保証範囲をどこで区切るか
モデルの許可条件と要求仕様が一致していても、実際のシステムで同じ安全性が成立するには、さらに確認すべき関係がある。モデルが扱う状態と実際のデータベースの状態が対応していること、認証によって決まった利用者が正しくモデルへ渡されること、モデルが発行した操作だけが実行環境で実行されることなどである。これらは認可規則の意味とは異なるが、証明された性質を実行環境へ適用するために必要な条件となる。
Nyxis は、証明の外側で信頼する仮定を公開文書「ASSUMPTIONS」に整理している[15]。そこでは、純粋なランタイムモデルについて証明された性質と、HTTP や JWT の処理、データベース接続、外部サービスの動作、開発・運用者が管理する設定などを区別している。これらの一部には Lean 上で検証された接続コードの性質も含まれるが、外部のデータベースや通信経路そのものの動作には別の前提が必要になる。
また、Nyxis の証明目録では、各定理について何が成立することを示しているかと、何を保証していないかが整理されている[16]。これは証明が不足しているという一括した評価を意味するものではない。証明対象と実際のシステムとの境界を明示することで、どの性質が数学的に成立しており、どの部分をテストや外部環境への仮定によって支えているかを確認できる。
| 検証する関係 | 確認する内容 | 不一致が生じた場合 |
|---|---|---|
| 要求仕様と認可モデル | モデルが許可する操作の範囲が、業務上許可すべき操作の範囲に含まれることを確認する。 | モデルに従った許可判定でも、業務上は権限外となる操作を認める可能性がある。 |
| 認可モデルと操作の発行 | 発行された操作が、モデルで定義された許可条件と宣言された効果を満たすことを確認する。 | モデルの許可条件が正しくても、認可されていない操作が実行層へ到達する可能性がある。 |
| モデルの状態と実行環境 | 認可判定に使用する状態、主体、操作が、実際のデータベースや認証結果と対応していることを確認する。 | モデル上の判定が正しくても、実行環境では異なる主体や状態に基づいて操作が実行される可能性がある。 |
| 実行環境と外部の効果 | データベースの変更や外部サービスへの送信が、許可された操作の範囲に従って行われることを確認する。 | モデルで制限した範囲を超える変更や情報の送信が、外部の処理経路で発生する可能性がある。 |
Nyxis の自己承認の事例が直接示しているのは、表の第一行に相当する問題である。発行された操作がモデル上の Authorized を満たすという性質が成立していても、その Authorized が参照する所属関係に提案行が先取りされていれば、業務上要求される許可条件とは異なる結果になる。実際のデータベースとの接続や外部サービスの信頼性を改善しても、認可モデルが使用する所属関係の意味を修正しなければ、この不一致は解消されない。
一方、認可モデルと要求仕様の対応を修正しても、外部の処理経路まで自動的に保証されるわけではない。認可判定に使用した状態と実際の更新対象が一致することや、発行された操作が想定どおり実行されることは、それぞれの境界で確認する必要がある。これらの条件を分けて評価することで、形式証明が成立させた性質と、システム全体について要求する安全性の間に、どのような追加条件が必要かを特定できる。
形式証明の価値は、定義された性質を曖昧さなく記述し、その成立を検証できることにある。Nyxis の事例では、発行操作が認可された効果に限られるという定理が成立する一方、認可の定義に用いる判定材料が操作後の所属を含んでいた。この差を把握することで、証明の成立と要求仕様への適合を別々に検証できる。認可の安全性を評価する際には、定理が存在することに加え、その定理で使用される許可の定義をたどり、どの状態から導出した権限を正当なものとして扱っているかを確認する必要がある。
8. 許可判定と状態変更の時点を整合させる
認可判定に使用する権限を操作前の状態から正しく導出しても、その状態と実際の更新が整合していなければ、安全性は維持できない。例えば、利用者 A が組織 G の管理者であることを確認し、メンバー追加を許可したとする。その直後に別の操作によって A の管理者権限が取り消された場合、追加処理がどの状態を基準に確定するかによって結果が変わる。権限の確認とデータベースの更新が別々に処理される設計では、許可判定に使用した状態が更新時点でも有効であることを保証する仕組みが必要になる。
この問題は、第 3 章で扱った自己承認とは発生条件が異なる。自己承認では、操作によって新たに成立する権限を、その操作自身の許可判定へ取り込んでいた。これに対して、認可後に別の操作が権限を変更する場合、判定材料は確認した時点では正しくても、更新を確定するまでに前提となる状態が変化する可能性がある。前者は判定材料を構成する方法に起因し、後者は判定と実行の間に成立する状態の整合性に関係する。
既稿「参照実装は設計判断を保存する」でも、認可、状態遷移、同時実行制御、トランザクションを異なる責務として整理している[17]。認可は操作を許可できるか判断し、状態遷移は操作によって何が変化するかを定義する。同時実行制御は、複数の操作が並行するときに状態の整合性を維持するための仕組みである。これらを一つの業務操作として結び付けるには、認可判定が参照した状態と、変更を確定する際の状態との関係を定義する必要がある。
PostgreSQL の Serializable 分離レベルは、並行して実行されたトランザクションの結果が、それらを何らかの順序で一つずつ実行した場合と同等になることを保証する。直列化できない競合が検出されると、トランザクションは失敗し、必要に応じてアプリケーションが処理を再試行する[18]。認可判定に必要な所属情報の読み取りと、許可された変更の実行を同じトランザクション内で行えば、両者を一貫した逐次実行順序に位置付けることができる。
ただし、直列化可能性が保証するのは、ある逐次実行順序と同等の結果になることである。管理者権限の取り消しとメンバー追加が並行する場合、メンバー追加が先に実行されたものとして直列化できれば、その後に管理者権限が取り消されても、追加操作が成立する場合がある。これは直列化可能性に反する動作ではない。取り消しが確定した後に行われる追加操作を必ず拒否するという要件があるなら、操作間の順序や認可情報の鮮度について、より具体的な条件を設ける必要がある。
また、認可判定をトランザクションの外側で済ませ、その結果だけを使って後から更新する構成では、更新側のトランザクションを Serializable にしても、外側で確認した権限の有効性まで保証されるわけではない。判定に必要な情報を同じトランザクションで読み取る方法や、権限情報のバージョンを更新時に照合する方法など、判定と確定を結び付ける仕組みが必要になる。採用する方法は、権限の変更をどの時点から後続の操作へ反映させるかという業務要件によって決まる。
分散した認可基盤では、権限情報と保護対象のデータが異なるシステムで管理される場合がある。この構成では、権限の変更と対象データの変更について、どの順序で処理された事実を認可判定へ反映するかが課題となる。Zanzibar は、アクセス制御情報と対象データの変更に対して、利用者の操作の因果順序を尊重する認可判断を提供する設計を採っている[19]。例えば、ある文書へのアクセス権限を取り消した後に文書を更新した場合、更新された文書の認可判定が古い権限関係に基づいて行われると、取り消しの意図と異なるアクセスが成立する可能性がある。複数のシステムにまたがる認可では、権限情報の新しさだけでなく、対象データの変更との因果関係を保存することが必要になる。
判定と使用の間に対象の状態が変化し、判定結果が無効になる競合条件は、TOCTOU と呼ばれる。MITRE の CWE-367 は、対象の状態を確認した後、実際に使用するまでの間に状態が変更され、確認結果が無効になる問題として定義している[20]。管理者権限を確認してからメンバーを追加するまでに、その権限が取り消される場合は、判定と使用の時点が分離していることによる問題として説明できる。
| 観点 | 自己承認 | 判定後の状態変更による競合 |
|---|---|---|
| 発生条件 | 操作によって新たに成立する権限を、同じ操作の許可判定へ反映する。 | 許可判定の後、操作を実行するまでに別の処理が判定の前提となる状態を変更する。 |
| 直接原因 | 操作前の権限と操作後の権限を同じ判定材料として扱う。 | 判定時点の状態と実行時点の状態が、要求された整合性条件を満たしていない。 |
| 並行処理の必要性 | 単一の操作でも成立する。 | 判定と実行の間に状態を変更する別の処理が関係する。 |
| 対処の対象 | 主体の既存権限を操作前の状態から導出し、作成対象の提案属性と分離する。 | 判定と更新のトランザクション境界、実行順序、権限情報の鮮度を整合させる。 |
| 形式的な検証条件 | 発行された操作が、操作前の権限に基づく要求仕様を満たすことを確認する。 | 判定に使用した状態と変更を確定する状態が、定められた同時実行の順序に従うことを確認する。 |
表の二つの問題は、どちらも認可判定に使用する状態の時点に関係するが、対処する場所が異なる。自己承認では、候補状態から操作主体の権限を導出しないように判定材料の構成を修正する必要がある。一方、判定後の状態変更による競合では、正しく構成した判定材料をどの状態の更新に対応付けるかが問われる。トランザクション分離レベルを変更しても、自己承認を生む認可モデルの定義は修正されない。また、認可モデルを修正しても、判定と実行の間に生じる競合を自動的に解消できるわけではない。
認可を安全な状態遷移として定義するには、三つの条件が対応していなければならない。第一に、操作を許可する権限が、要求仕様の定める状態から導出されていること。第二に、作成対象の提案属性が対象の評価に使用される一方、操作後に成立する権限が既存権限として先取りされないこと。第三に、認可判定に使用した状態と、操作を確定する際の状態との関係が、並行する操作を含めて定義されていることである。
この三つは、それぞれ異なる失敗を排除するための条件である。第一の条件が欠ければ、要求仕様が許可していない操作を認可モデルが許可する可能性がある。第二の条件が欠ければ、メンバー追加によって初めて成立する所属関係を、その追加操作自身の許可理由として使用できてしまう。第三の条件が欠ければ、判定時には有効だった権限が変更確定時の要求条件を満たさなくなる可能性がある。これらを区別することで、権限の定義、判定材料の構成、実行時の整合性を個別に検証できる。
利用者が自分自身を組織へ追加する最小の例では、操作前の所属関係を使用すると \(P_{\mathrm{pre}}=0\) となるが、追加予定の所属行を含む候補状態を使用すると \(P_{\mathrm{post}}=1\) となった。この反転は、認可規則の評価方法を変更しなくても、判定材料の時点だけで権限境界が変化することを示している。さらに、正しい判定材料を使用したとしても、実際の更新と整合する状態を定めなければ、複数の操作を通じた安全性は説明できない。
認可規則を形式化する際には、どの主体に何を許可するかに加えて、その権限がどの状態で成立し、どの状態遷移を許可する根拠になるかまで定義する必要がある。形式証明によって確認すべき性質も、許可された操作の集合だけでなく、許可に使用した権限の由来と、変更が確定する順序を含めて決まる。認可の安全性は、許可条件、判定材料、状態遷移の三者が要求仕様に対して整合していることによって成立する。
参考文献
- id774, 安全判定の揺らぎを入力・構造・評価方法に分けて測る（2026-10-21）. https://blog.id774.net/entry/2026/10/21/5796/
- Vincent C. Hu et al., Guide to Attribute Based Access Control (ABAC) Definition and Considerations（2014-01）. https://csrc.nist.gov/pubs/sp/800/162/upd2/final
- Cedar Policy Language, How Cedar authorization works. https://docs.cedarpolicy.com/auth/authorization.html
- Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers（2002-06）. https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/
- Cedar Policy Language, Design: Implement meta-permissions as policies. https://docs.cedarpolicy.com/bestpractices/bp-meta-permissions.html
- Cedar Policy Language, Best practice: Identify your authorization patterns. https://docs.cedarpolicy.com/bestpractices/bp-authorization-patterns.html
- Cedar Policy Language, Best practice: Don’t use the context field to hold information about the principal, action, and resource. https://docs.cedarpolicy.com/bestpractices/bp-using-the-context.html
- NyxFoundation, Nyxis.Authz. https://github.com/NyxFoundation/nyxis/blob/785c11a6285fe92901e871e1fc0f7064eda93941/Nyxis/Authz.lean
- NyxFoundation, Nyxis.Materials. https://github.com/NyxFoundation/nyxis/blob/785c11a6285fe92901e871e1fc0f7064eda93941/Nyxis/Materials.lean
- NyxFoundation, fix(authz): judge membership inserts against pre-insert memberships（2026-10-26）. https://github.com/NyxFoundation/nyxis/pull/3
- NyxFoundation, Nyxis.Runtime. https://github.com/NyxFoundation/nyxis/blob/785c11a6285fe92901e871e1fc0f7064eda93941/Nyxis/Runtime.lean
- Joseph W. Cutler et al., Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)（2024-03-07）. https://arxiv.org/abs/2403.04651
- Craig Disselkoen et al., How We Built Cedar: A Verification-Guided Approach（2024-07-01）. https://arxiv.org/abs/2407.01688
- id774, 証明はいつ数学的知識になるのか（2026-10-09）. https://blog.id774.net/entry/2026/10/09/5760/
- NyxFoundation, ASSUMPTIONS — 証明の外側で信頼する仮定. https://github.com/NyxFoundation/nyxis/blob/785c11a6285fe92901e871e1fc0f7064eda93941/ASSUMPTIONS.ja.md
- NyxFoundation, 証明の目録. https://github.com/NyxFoundation/nyxis/blob/785c11a6285fe92901e871e1fc0f7064eda93941/docs/proofs.md
- id774, 参照実装は設計判断を保存する（2026-10-05）. https://blog.id774.net/entry/2026/10/05/5751/
- PostgreSQL Global Development Group, Transaction Isolation. https://www.postgresql.org/docs/current/transaction-iso.html
- Ruoming Pang et al., Zanzibar: Google’s Consistent, Global Authorization System（2019-07）. https://www.usenix.org/conference/atc19/presentation/pang
- MITRE, CWE-367: Time-of-check Time-of-use (TOCTOU) Race Condition. https://cwe.mitre.org/data/definitions/367.html