2026/08/17AIauthorization-policy-compliance-by-types

型システムで「認可ポリシーを守るコード」を検証する研究

認可を型で扱う研究には、「EditableDocument のような型を付ける」というより強い形として、実装コード全体が論理的な authorization policy に従っていることを型検査で証明する系譜がある。

Fournet, Gordon, Maffeis の A Type Discipline for Authorization Policies は、Datalog で authorization policy を表し、その policy と distributed implementation の対応を process calculus 上で定式化したうえで、dependent type system によって implementation code の policy compliance を検証する。

ここで型が担うのは単なるデータ分類ではない。

logical authorization policy
        ↓
implementation code
        ↓ type checking
policy に違反する実行をしないことを検証

という関係である。

Fine はこの方向を dynamic / stateful policy へ広げる。Swamy, Chen, Chugh は dependent、refinement、affine types を組み合わせ、access control や information flow を含む動的な security policy の enforcement を source level で検査する言語を提案した。後続の F* では refinement properties を logical proof terms や cryptographic evidence と組み合わせて扱い、authorization properties を検証した browser extensions や verified reference monitor を例として報告している。

したがって、「認可をコードの型に反映できるか」という問いへの学術的な答えは明確に yes である。ただし、その代表例が Authorized<Resource> のような一般的 wrapper API を推奨しているわけではない。policy proposition と program values の関係を dependent/refinement type で表し、型検査器に proof obligation を負わせる方が直接の研究内容である。

この違いは「認可済みリソース型」は既存研究の直訳ではなく設計上の合成で重要になる。Go のような dependent/refinement type を持たない言語で認可済み wrapper を作ることは、これらの研究をそのまま移植することではなく、より弱い近似として解釈すべきである。

型システムで「認可ポリシーを守るコード」を検証する研究

出典

🔗 リンクされているノート