情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

1. は じ め に論理プログラミングを基礎とした認可ポリシ記述言語

近年の情報システムは大規模・複雑化しているため，脆弱性のないシステムを構成するのが困難である．そのため，現実的なセキュリティ対策としては，脆弱性の存在を前提とした

橋 本 正 樹†1
金
†1,†2
辻
秀 典
田

美 羅†1
中 英 彦†1

システム設計を行い，多層防御戦略1) をとることが有効である．多層防御は，情報システムを厳密に区画化しておくことで，仮にマルウェアやウィルスなどによるゼロデイ攻撃が実行され，システムへの侵入を許した場合にも，重要な情報資産への攻撃を遅延したり，被害範

近年の情報システムでは脆弱性を完全に排除するのが難しいため，多層防御によってセキュリティ・インシデントの発生に備える必要がある．多層防御を効果的に実現するためには，細粒度の強制アクセス制御を行うための膨大なアクセス制御規則をポリシとして記述する必要があるが，既存の記述方式は可読性や保守性に問題がある．
本研究では，論理プログラムとしてアクセス制御規則を記述することで，属性の継承や頻出する認可手順のサブルーチン化をサポートするポリシ記述言語を提案し，この問題を解決する．本稿では，認可判定の妥当性と表現力を評価して，本言語の有用性を実証し，期待される効果を考察する．

囲を局所化したりすることができる．
多層防御は，細粒度の強制アクセス制御によってシステム内を細かく区画化するほど有効性が高まるが，そのためには膨大なアクセス制御規則をポリシとして記述する必要がある．
一方で，区画の粒度を粗くしてアクセス制御規則の記述量を低減させた場合は，セキュリ
ティインシデント発生時の直接的な被害範囲が拡大するうえ，被害伝播の遅延効果も薄くなるため，多層防御の有効性を相殺してしまう．そのため，多層防御を効果的に適用するためには，膨大なポリシを簡潔に記述する工夫が必要となるが，SELinux 2) をはじめとした多層防御の既存実装例では，アクセス制御規則を個々に直接記述する手法が主であるため，

Policy Description Language for Authorization
Using Logic-based Programming
Masaki Hashimoto,†1 Mira Kim,†1 Hidenori Tsuji†1,†2
and Hidehiko Tanaka†1

その粒度を細かくするほどに記述量が膨大になる傾向があり，ポリシ全体としての動作は，専用の検証用ツールを用いないことには把握が困難である．
本研究は，論理プログラムとしてアクセス制御規則を表現することで，属性の継承やサブルーチンとして構造化された記述が可能なポリシ記述言語を提案し，この問題の解決を図るものである．本言語は，個々のアクセス制御規則を記述するための宣言文と，宣言文の集合として構成されたポリシに問合せを行うための認可判定文を，構文規則とその形式

Recently, with the impossibility of eradicating the vulnerabilities of information systems, we must prepare for the occurrence of the security incident by themulti-layer defense called Defense-in-Depth strategy. In the multi-layer defense,
it is important to authorize accesses in ﬁne-grained granularity to compose eachlayer eﬀectively and many access control models are proposed to follow them.
However, policy description languages proposed so far cannot express the models appropriately in proper granularity. In this paper, we propose a policy
description language which can designate many kinds of conditions for access
control like dynamic status of application process as an element of decision data,and implement it in Datalog. Using the proposed language, we compose thepolicy of SELinux which is a major implementation achieving the multi-layer
defense, and we conﬁrm the advantages of the proposed language by evaluating
the validity and the expressiveness.

1682

的な意味，推論規則を定めることで基本設計を行い，これを Prolog 3) のサブセットである

Datalog 4) を用いて実装している．また，本稿では，本言語を用いて具体的なアクセス制御
モデルを構造的に記述する手法を示したうえで，SELinux のポリシを実際に記述した実験システムを構成し，認可判定の妥当性と表現力の評価を行った．
以下に，本稿の構成を示す．はじめに，2 章では，脆弱性の存在を前提とした戦略としての多層防御について説明し，関連研究として多層防御の実装例である SELinux とポリシ記述†1 情報セキュリティ大学院大学
Institute of Information Security†2 株式会社情報技研
Advanced Institute of Information Technologyc 2010 Information Processing Society of Japan


1683

論理プログラミングを基礎とした認可ポリシ記述言語に関する近年の研究動向を説明した後に，本研究の目的を説明する．次に，3 章では，本言応じてアクセス制御モデルを決定する必要がある．アクセス制御モデルが決まると，次に必語の基本設計として，文法と意味，推論規則を示し，Datalog を用いた実装方法を説明する．

要になるのは，その方針に従ってアクセス制御規則を具体的に記述することで，これはポリ

続いて，4 章では，本言語を用いてアクセス制御モデルを記述する具体的な手法を説明し，

シ記述言語により実現する．ポリシ記述言語は，アクセス制御モデルを過不足なく表現で5 章では，本言語の評価実験とその考察について述べる．最後に，6 章で，本稿をまとめる．

きることが必要で，記述する人間にとって直感的に理解できるものであることが望ましい．

2. 本研究の背景と目的

最後に必要となるのは，強制アクセス制御機構で，これは参照モニタとも呼ばれる．強制ア

本章では，はじめに，研究の背景として，情報システムの保護手法である多層防御につい執行するために，全アクセスを補足して仲介する．近年では，プロセスがリソースアクセス

クセス制御機構は，ポリシ記述言語によって記述されたアクセス制御規則を漏れなく確実にて，脆弱性との関連性に着目して説明する．また，その実装例として SELinux を取り上げ，をする場合に迂回不可能なパスとして OS を利用し，これを実現するセキュア OS が実装さ

細粒度の強制アクセス制御を用いて多層防御を実現する方式と，その際に課題となるポリシ

れている．

記述について説明する．その後，ポリシ記述に関する近年の研究を示し，最後に本研究の目

2.2 関 連 研 究的を説明する．

本節では，はじめに，多層防御を実現した実装として SELinux について説明し，これを2.1 脆弱性と多層防御

例にポリシ記述に関する課題を示す．次に，ポリシ記述に関する近年の研究動向を説明し，近年の情報システムは大規模・複雑化しているため，脆弱性のないシステムを構成するの本研究との関連を述べる．

が困難である．ソフトウェアの解析技術や開発手法の発展などによって，その混入を防ぐ仕2.2.1 SELinux における多層防御の実現方式とその課題

組みが洗練されてきているが，情報システムへの攻撃では，最も弱い部分を能動的に探し出

SELinux は米国家安全保障局を中心としたオープンソースコミュニティによって活発にし，そのパスを意図的にたどって実行することが多いため，通常の運用では無視できるほど開発が進められているセキュア OS の代表格である．SELinux は，Flask セキュリティアーの微細な脆弱性であっても，システムを致命的な状態に陥らせる可能性がある．そのため，

キテクチャ8) の Linux に対する実装で，セキュリティサーバとオブジェクトマネージャ，アセキュリティの観点からすると，脆弱性を根絶できない限りは，たとえ可能性が低くても，

クセスベクタキャッシュから構成される．Linux における実装では，システムコールをフッ攻撃が成功する事態を考慮する必要がある．したがって，これを考慮した現実的なセキュリ

クすることでアクセス制御に関連するカーネル内制御を奪い，独自のポリシによるアクセス

ティ対策としては，脆弱性の存在を前提としたシステム設計を行い，多層防御戦略をとるこ

制御を SELinux が強制する．

とが有効である．多層防御戦略は，情報システムを厳密に区画化しておくことで，仮にマSELinux は，原理的にすべてのシステムコールに対してアクセス制御の判定を行えるた

ルウェアやウィルスなどによるゼロデイ攻撃が実行され，システムへの侵入を許した場合にめ，RBAC モデルや DTE モデルをシステムコールレベルの粒度で実現することが可能でも，重要な情報資産への攻撃を遅延したり，被害範囲を局所化したりするものである．

ある．しかし一方で，細粒度のアクセス制御を行うためには当然その制御規則となるポリシ

今後は，クラウドコンピューティングや Web サービス，Grid コンピューティングによっについても細粒度に記述する必要があるが，これは人間にとって非常に困難な仕事である．

て，情報システムが従来以上に大規模・複雑化していくことが予想されるため，結果としたとえば，SELinux では以下のようなアクセス制御規則を並べてポリシを構成する．

て，システムから脆弱性を根絶するのはさらに困難となっていく．したがって，真に信頼でallow acct t unconf ined t:f d use;

きるコンピューティング環境を構築するためには，脆弱性の存在を前提としたシステムを構

allow acct t init t:process sigchld;

築することが現実的で，そのために，多層防御戦略の実現が望まれる．

allow acct t init t:process signull;

多層防御を実現するためには，はじめに，層の構成方針を定めるアクセス制御モデルを決定する．アクセス制御モデルには，たとえば，RBAC

5)

6)

allow acct t rpm t:f d use;など様々な

この例では，各行が 1 つのアクセス制御規則を表現しており，たとえば 1 行目では，最初モデルが提案されており，それぞれに利害得失があるため，実現を目指すシステムの特性にの項目 allow によって，当該行が許可される規則であることを示す．2 つ目の項目は，この情報処理学会論文誌

Vol. 51

No. 9

や DTE ，HBAC

7)

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan


1684

論理プログラミングを基礎とした認可ポリシ記述言語

規則を適用するサブジェクトの情報で，3 つ目以降はオブジェクトの情報と操作内容を示す．

が，前者は特に，比較的大規模なシステムにおいて，ポリシを管理領域ごとにモジュール化

SELinux では，上記文法によるアクセス制御規則が，デフォルト・インストールされる

して構成することを前提とし，分散管理された領域間で権限の委譲を柔軟に行うための記述

個人ユーザ用の簡易版ポリシでも 40,000 行近く羅列されている．そのため，たとえ 1 行 1

方法に主眼をあてた研究で，後者は論理的な否定を形式的に正しく推論することに注力して行の各アクセス制御規則を理解できたとしても，その総体として構成されるポリシで実際にいる．本研究は，認可判定規則に対する記述の抽象度を高めることで記述方法そのものの効

何が起こるのかを判断するのは難しい．さらに近年では，SELinux による強制アクセス制

率化を目指した点がこれらの研究と異なる．

御規則の適用範囲を OS 階層の資源から，アプリケーション層の要素や他システムの要素にまで拡大する実装が提案されているため

9),10)，適切なポリシ記述がますます困難になることが推測できる．

本研究の目的は，論理プログラムとしてアクセス制御規則を記述することで，属性の継承や認可手順のサブルーチン化をサポートするポリシ記述言語を提案し．これによって，ポリ2.2.2 ポリシ記述言語に関わる近年の研究状況

従来のポリシ記述手法は，2.2 節で例にあげた SELinux や XACML 17) のように，個々の信頼性を評価するためのフレームワークである．SDSI は “speaks-for” という述語を利用のアクセス制御規則をそれぞれ独立に記述し，また，その各要素を直接指定するため，可読して論理の構築を行い，SPKI では宣言内で述語をタグとしてエンコードすることができる．

性や保守性に問題があった．この問題は，多層防御の有効性を向上させようとシステム内をSDSI と SPKI 双方ともに，ポリシを英文に類似した構文規則によって表現できるという特細かく区画化するほどに，必要となるアクセス制御規則の粒度も細かくなるため，より大と SPKI

12)

シ記述の複雑性の問題を，柔軟な構造化記述手法によって解決することである．

は，アクセス制御を行う際に証明書の交換を行うことでシステム間

SDSI

11)

2.3 本研究の目的徴を持つが，SDSI は “speaks-for” のみを述語として利用するため，応用に応じた述語を定きな問題となる．その一方で，アクセス制御規則の粒度を粗くすると記述量を低減させる

義できないという制限がある．また，SPKI は複数の述語を利用可能であるが，あらかじめことができるが，この場合はセキュリティインシデント発生時の直接的な被害範囲が拡大す定義されたタグに制約されるため，変数を扱うことができないので，こちらもやはり適切な

るうえ，被害伝播の遅延効果も薄くなるため，多層防御の有効性を相殺してしまう．また，述語を定義するのが難しいという課題がある．同様に，PolicyMaker 13) と KeyNote 14) に今後クラウドや Grid の普及により，複数システムの連携処理が一般化し，個々のシステム

おいても，認可判定に必要となる様々な状態を定義することができるという特徴を持つフで任意にアクセス制御規則を定めるのではなく，ポリシによって全体を制御するような場合

レームワークであるが，述語の定義に厳しい制限があるため，応用に応じた述語を利用すには，記述量が爆発することが容易に想像できる．

ることはできない．これらの言語は領域間の信頼性管理に主眼をおいているため，述語をそこで，これらの問題に対抗するために，近年では 2.2.2 項で示したようなポリシ記述にある程度絞り込んでいても有効であるが，これを認可判定言語として用いた場合，現実に関する様々な研究が行われているものの，既存研究ではポリシの記述量そのものを低減さ利用されている様々なアクセス制御モデルに対応するのが難しい．そのため，本研究では，せるような記述手法について検討が不十分であるため，本研究では，特にこの点に着目し，ユーザ定義の操作内容を述部の一部として指定する構文規則を定めることで，任意の意味をポリシ記述の抽象度を高めて効率的に記述する手法を検討する．また同時に，プログラムと持つ述部を記述可能な方式を検討した．

して記述したポリシが論理的に正しく動作して認可判定を行えることと，記述量を低減させ

SecPAL

15)

は，制約論理言語によるポリシ記述言語で，認可要求は節の集合に対するクエリが成功したときに承認される．SecPAL の文法は自然言語に近く，意味付けは 3 つの推ることができていることを，実際に利用されているポリシを提案手法で記述する実験によって定量的に評価し，確認する．

論ルールから構成されており，否定的なクエリや再帰的な述語，回数を指定可能な権限委譲

ポリシを論理プログラムとして構造的に記述することで，数理論理学的な裏付けを自然にやその他様々な制限をサポートすることで，多くのアクセス制御モデルを汎用的に表現可

ポリシ記述に適用できることを期待でき，これにより，たとえば，通常は別の独立した応用能である．また，Lithium 16) も SecPAL 同様に，一階述語論理を基礎に推論を用いてポリプログラムとして実現されているポリシの検証機能を記述方式そのものに組み込み，検証結シを記述する言語で，再帰的な表現を制限することにより，否定を含んだ推論を実現してい果をアクセス制御の条件とすることでアクセス権限の競合をあらかじめ排除したり，他シスる．これらの言語は，論理型言語と推論によってポリシを表現する点が本研究と共通である

テムから依頼された仕事を処理する代理プロセスに対して，仕事の内容に応じた最小限の権

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan


1685

論理プログラミングを基礎とした認可ポリシ記述言語

限セットを付与したりすることなどを期待できる．また，補助的な規則によって新規則の追ているとする．イタリック書式の小文字で示されたものは変数項を示し，変数項への項の代加方法や既存規則の変更を制御する機能や，認可判定に利用する引数を認可判定機構が状

入は，変数項とその項の領域が一致したときのみ許される．また，f acti は f act と同種の況に応じて変更する機能なども考えられる．さらには，アクセス制御対象が特定の属性をものであるが，それぞれを区別するために接尾辞を付したものである．S はアクセス主体や保持しているかどうかを検証することで，たとえば「停止中である」や「汚染されている」

対象に属性を付したもので，本言語では S を主部としたものに述部となる V を与えることといった動的に遷移しうる情報に基づいたアクセス制御を行い，意図しない情報流を未然にでアクセス制御規則を表現する．I はもう 1 つの述部となりうる要素で，この場合，主部は防ぐことなどが期待される．

A のみとなる．各述部の直感的な意味は，“is permitted to” と “is forbidden to” に

3. ポリシ記述言語の設計と実装
本言語は，アクセス制御規則を設定するためのポリシ宣言文と，ポリシに対してアクセス

よって，主部 S1 がある対象 S2 に対して O を許可/拒否することを示し，また，“moves

to” によって，主部 S1 が O を契機に S2 に遷移することを示す．
3.1.2 構文の形式的な意味と推論規則

可否の問合せを行うための認可判定文から構成される．本章では，はじめに，それぞれの構

本言語では，宣言文の集合であるポリシ DS に対して認可判定文 Q が与えられたときに，

文規則とその意味を形式的に定義し，これに適用する推論規則を述べることで本言語の設計

以下に示す DS, θ  Q の関係によって，認可判定文の解釈を決定する．Q の真偽はそれぞを説明する．その後，Prolog のサブセットである Datalog を用いた本言語の実装について

れ認可判定時の許可と拒否として解釈されるが，Q が変数項を含む場合は Q を真とするよ

説明する．

うなすべての応答が返される．θ は，変数項を別の変数項や定数項に対応付けする写像で，3.1 ポリシ記述言語の設計

f actθ は，θ を f act に適用したものである．また，θ− x は，dom(θ) − {x} を領域とする写

本節では，ポリシ記述言語の設計として，はじめに，ポリシ宣言文と認可判定文の構文規像を示し，vars(X) は，節 X に存在する変数項を示す．

則を定義し，次に，その形式的な意味と推論規則を説明する．本言語は，英語に類似した構
文規則と意味，単純な推論規則によって，理解しやすいものとなるように工夫した．

3.1.1 ポリシ宣言文と認可判定文の構文規則
本言語は，ポリシを以下の構文規則で記述された宣言文の集合（DS: Declarative State-ments ）として構成し，アクセス制御の際にはポリシに対して，認可判定文（Q: Authorization
Query ）によってアクセス可否を問い合わせる．

DS, θ  Policy specifies f act iﬀ DS |= Policy specifies f actθ,and dom(θ) ⊇ vars(Policy specifies f act)DS, θ− x  ∃x(Q) iﬀ DS, θ  Q
次に，宣言文と認可判定文に適用する推論規則を以下のように定義する．推論規則は，特定の構文構成に対して自動的に適用することで別の新しい構文を導くもので，宣言文の記述量を軽減することができる．推論規則 (a) は，条件節のある宣言文と，その条件節の各 f act

DS ::= Policy specifies f act if f act1 ,..., f actn (n ≥ 0)

を vars(f actθ) = 0 とするような θ があった場合に，自動的に変数項のない f actθ を導く．

Q ::= Policy specifies f act | ∃x(Q)なお，vars(f actθ) = 0 は，f actθ に変数項が存在しないことを示すものである．また，推S ::= E tagged A

論規則 (b) は，属性 A2 が属性 A1 を継承するような構文と，属性 A1 を付された変数 x に

V ::= is permitted to O S | is forbidden to O S | moves to S with O

対して V1 を宣言する構文があった場合に，自動的に属性 A2 を付された変数 x に対しても

I ::= inherits A

V1 を宣言する構文を導く．

f act ::= S V | A I | S

推論規則 (a)礎的な要素である述語を表す．E ，O，A は，それぞれアクセス主体とその対象，操作内容，(Policy specifies f act if f act1 , ..., f actk ) ∈ DS
DS |= Policy specifies f acti θ for all i ∈ {1..k}vars(f actθ)=0

属性を示す項である．すべての項にはそれぞれその項が属する 1 つの領域が関連づけられ

DS |= Policy specifies f actθ

本言語は述語論理を基礎とし，上記のうち，ボールド書式で示されたものは構文規則の基

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan


1686

論理プログラミングを基礎とした認可ポリシ記述言語

推論規則 (b)係する用語は以下のように定義する．リテラル P は，述語の名前と一連の引数を持つ．引

DS |= Policy specifies A2 inherits A1
DS |= Policy specifies x tagged A1 V1
DS |= Policy specifies x tagged A2 V1

数は，定数項か変数項をとる．節は，P0 ← P1 , ..., Pn として書き，“←” の左辺にある 1 つの頭部リテラルと右辺にある本体リテラルのリストから構成される．
本実装では，構文規則で定義した各述語を以下のように Datalog リテラルへ変換する．

3.2 ポリシ記述言語の実装“→” の左辺は，本言語による記述で，右辺は変換後の Datalog リテラルである．本変換で本節では，Datalog を基礎とした本言語の実装を説明する．Datalog は Prolog のサブセッ

は，宣言文と認可判定文の f act 内にある述語を Datalog リテラルの述語とし，その目的語トとなる論理プログラミング言語で，本言語は宣言文と認可判定文を Datalog プログラム

を Datalog リテラルの引数として変換する．また，if 以降にある f act についても，上記手に翻訳することで実現する．本言語は，アクセス制御規則を論理プログラミングを用いて表法によって Datalog リテラルした変換後，Datalog 節の条件節として用いる．

現することにより，ポリシ記述に数理論理学的な裏付けを与えながら，宣言的な記述を行う

Policy specifies E tagged A → tagged(E,A)
Policy specifies A1 inherits A2 → inherits(A1 ,A2 )ことができる．

Policy specifies E1 tagged A1 is permitted to O E2 tagged A2

3.2.1 Datalog とその拡張実装 XSB の概要→ permitted(E1 ,A1 ,O,E2 ,A2 )Datalog は論理プログラミングを基礎とした言語で，特に大規模データベースと情報を交換するために設計されたルールベースの言語である．すなわち，データへ直接アクセスする

Policy specifies E1 tagged A1 is forbidden to O E2 tagged A2→ forbidden(E1 ,A1 ,O,E2 ,A2 )インタフェースを用意してルールベースによる情報の交換をサポートする．また，Datalog
は構文的観点から Prolog のサブセットであり，Datalog プログラムは Prolog インタプリ

Policy specifies E1 tagged A1 moves to E2 tagged A2 with O→ moves(E1 ,A1 ,O,E2 ,A2 )タによって構文解析して実行することができる．

XSB

18)

は Datalog の一実装で，ISO 標準に準拠した完全な Prolog システムとなってお4. アクセス制御モデルの表現手法

り，そのうえでさらに，テーブル型述語と非テーブル型述語の統合をサポートする．XSB
は Prolog を含む通常の論理プログラミングシステムにはない以下のような特徴を持つ．

• SLG 導出19)

により整礎的意味論に従った完全な解導出が可能

数やサブルーチンを用いたプログラムとして表現することで，要素間の関係や頻出する認可• 高階論理プログラミング言語 HiLog 20) の実装• Uniﬁcation Factoring

21)

をはじめとした様々な索引付け制御技術• 移植性と拡張性のためのソースコード利用可能性
XSB のコンポーネントの多くは PSB-Prolog22)に基づいているが，SLG 導出と HiLog

表現の処理のために Prolog システムと一部異なっている．たとえば，Prolog の SLD 導出23)

本章では，広く利用されている種々のアクセス制御モデルを本言語を用いて表現する手法を示す．はじめに，従来のように個々のアクセス制御規則を直接に記述するのではなく，変は深さ優先探索に基づくため無限ループに陥りやすいが，XSB の SLG 導出はほぼす

べての論理プログラムを正しく評価できる．

手順を簡潔に記述できることを説明し，その後，この表現手法を用いた具体的なアクセス制
御規則の記述例を示す．

4.1 要素の階層化と認可手順の構造化
本節では，アクセス制御に利用する要素を階層化し，要素間の関係をサブルーチンとして構造化することで，ポリシ記述を簡略化する手法を示す．
要素の階層化は，様々なアクセス制御モデルに出現するポリシ記述の簡略化手法で，RBAC

3.2.2 Datalog プログラムへの変換規則

や DTE，Chinese Wall 24) などもアクセス制御要素をグループ化し，階層化する一方式と本言語では，3.1 節で示した構文規則に基づく各宣言文が，Datalog プログラムの節としして見ることができる．たとえば，RBAC は，アクセス制御規則を役割ごとに与えることて変換され，認可判定文は，このプログラムに対する問合せとして評価する．Datalog に関でアクセス制御規則のグループ化を行い，さらに役割間の階層構造を定義することでアクセス制御規則群をまとめて継承する方法を定めるモデルである．同様に，DTE は，アクセス

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan


1687

論理プログラミングを基礎とした認可ポリシ記述言語

主体とアクセス対象をそれぞれドメイン，タイプとしてグループ化し，その間にアクセス制
御規則を定義することで柔軟にアクセス制御の粒度を制御するモデルである．

加えて，本言語では上記のようにグループ化された属性間の遷移条件を述語 “moves to”
を用いて下記のように定めることにより，特定の認可手順を抽象的に構造化する．

また，要素間の関係の構造化は，特定の認可手順をあらかじめサブルーチン化して簡潔に

Policy specifies x tagged p moves to x tagged A5 with O3
if x tagged A4(8)

記述する手法で，たとえば，TBAC 7) や Ahmed らによる CSCW システム向けのアクセス制御モデル25) は，それぞれ Authorization Step や Activity Template として特定の認

Policy specifies x tagged A5 is permitted to O4 E5 tagged A6(9)可手順を抽象的に構造化している．これにより，サブルーチン化された認可手順をトランザ(8) は，アクセス主体 x に属性 A4 が付されていたとき，O3 を契機にその属性が A5 に遷クション処理などで繰り返し利用することで，ポリシの記述量を低減させ，見通しを向上さ移する規則を示す．この遷移により，アクセス主体 x の属性は，属性 A5 に変わる．(9) は，
属性 A5 を付されたアクセス主体に，属性 A6 を付されたアクセス対象 E5 に対して O4 をせている．
本言語では，下記に示すように，アクセス主体とその属性を変数項に，それ以外の項を定許可する規則を定める．これらにより，A4 によってグループ化されたアクセス規則が，さ数項として固定したうえで，条件節を用いてアクセス主体を指定することで，当該アクセス

らに (8) によって (9) に遷移することで，(1)，(2)，(3) から (9) へ続く認可手順を抽象的

制御規則を適用するアクセス主体をまとめて指定することができる．

に構造化している．また，遷移規則は複数連続させることでトランザクション処理のような

Policy specifies x tagged p is permitted to O1 E1 tagged A1
if x tagged A4(1)

Policy specifies x tagged p is permitted to O2 E2 tagged A2
if x tagged A4(2)

Policy specifies x tagged p is permitted to O3 E3 tagged A3
if x tagged A4(3)

複雑な認可手順も簡潔に表現できる．

4.2 アクセス制御規則の記述例
本節では，前節で示した記述手法を用いて，広く利用されている種々のアクセス制御モデ
ルを実際に表現する記述例を示す．ここでは階層化の例として RBAC を，認可手順のサブルーチン化の例として TBAC を取り上げる．

RBAC RBAC は，役割として抽象化された属性に複数のアクセス制御規則を関連付ける(1) は，属性 A1 を付された対象 E1 に操作内容 O1 を許可する規則を，付された属性がことでポリシを記述するモデルで，企業などの組織形態に自然に適用しやすいため，広A4 であることを条件にアクセス主体 x に与えている．同様に (2)，(3) では，属性 A2 を付く一般的に利用されている．下記の例では，(10) によって Manager の役割を付されされた対象 E2 に操作内容 O2 を許可する規則と属性 A3 を付された対象 E3 に操作内容 O3

たアクセス主体に Billing Information を付されたアクセス対象を Read する権限を許可する規則を，付された属性が A4 であることを条件にアクセス主体 x に与えている．

を与え，(11) によって Floor Leader の役割を付されたアクセス主体に Account-

これら (1)，(2)，(3) によって複数のアクセス制御規則を属性 A4 にグループ化した後に，ing Information を付されたアクセス対象を Read する権限を与えている．また，(12)下記 (4) のように属性 A4 を特定のアクセス主体 E4 に付することにより，グループ化されによって，Manager は，Floor Leader に与えられた権限を継承する．これらの規た (1)，(2)，(3) が改めて具体化されたアクセス主体に (5)，(6)，(7) として展開される．

則により，仮に同じアクセス主体であっても付された役割によって与えられる権限を変Policy specifies E4 tagged A4(4)

Policy specifies E4 tagged A4 is permitted to O1 E1 tagged A1(5)

Policy specifies E4 tagged A4 is permitted to O2 E2 tagged A2(6)

Policy specifies E4 tagged A4 is permitted to O3 E3 tagged A3(7)

このとき，(5)，(6)，(7) は，直接記述された規則ではなく，グループ化された規則を付与，展開することで新たに生成された規則であり，(4) のように具体的なアクセス主体に属性 A4 を付すことで新たな規則を繰り返し生成することが可能である．

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

更することができる．

Policy specifies x tagged p is permitted to Read y tagged q
if x tagged Manager,y tagged Billing Information(10)

Policy specifies x tagged p is permitted to Read y tagged q
if x tagged Floor Leader,y tagged Accounting Information(11)c 2010 Information Processing Society of Japan


1688

論理プログラミングを基礎とした認可ポリシ記述言語

Policy specifies Manager inherits Floor Leader(12)

TBAC TBAC は，Authorization Step（AS）として認可手順をまとめたうえで，アクソフトウェアのバージョンは，libselinux1(2.0.65-5)，selinux-basics(0.3.5)，selinux-policy-

default(2:0.0.20080702-6) である．実験システムでは，カーネル空間に存在する sidtab とセス主体，アクセス対象，操作内容に加えて，AS 名と AS 内のどの工程にいるか，と

avtab のアドレスを取得し，そのハッシュ配列のポインタを利用してテーブルの内容をすべいう情報を指定して認可判定を決定するモデルである．本モデルでは，トランザクショて取得する．同時に，取得した avtab に並んでいる全要素の情報を本言語によって表現しン処理中の各要素について，多様な関係を指定することができる．下記の例では，(13)たうえで，Datalog に読み込ませた認可判定機構を用意し，ソースコンテキスト，ターゲッ

によって Prepare Phase にあるアクセス主体に，Not Prepared にある DB1 に対トコンテキスト，セキュリティクラスの組合せによる問合せに備える．計測プログラムは C

して Request to Prepare する権限を与え，(14) によって Commit Phase にある言語で記述し，結果はコンテキストやクラスの情報を名前の文字列に変換し，テキストファ

アクセス主体に，Prepared にある DB1 を Commit する権限を与えている．また，イルとして記録した．

(15) によって，Prepare Phase にあるアクセス主体は，DB1 Prepared を契機に
Commit Phase に遷移するように指定している．これらの規則により，トランザクショ

5.2 応答内容の比較による妥当性の評価実験
本節では，SELinux のポリシと，同ポリシを本言語で構成したもので，応答内容の同一性を評価した結果を示す．実験は，sidtab の全要素を用いて，セキュリティクラスに対すン処理の工程に応じて与えられる権限を変更することができる．

Policy specifies x tagged p is permitted toRequest to Prepare DB1 tagged q
if x tagged Prepare Phase,
DB1 tagged Not Prepared(13)

Policy specifies x tagged p is permitted to Commit DB1 tagged q
if x tagged Commit Phase,
DB1 tagged Prepared(14)

Policy specifies x tagged Prepare Phase moves tox tagged Commit Phase with DB1 Prepared(15)

る総当りで context struct compute av() を呼び出して AV（Access Vector）を取得した
うえで，同じソースコンテキスト，ターゲットコンテキスト，セキュリティクラスの組合せ
で Datalog に問合せを行い，得られた AV が context struct compute av() が返したものと一致するか否かを評価した．
この実験では，sidtab の全要素と全セキュリティクラスの組合せを用いた合計 15,100,162
個の問合せが生成されて評価され，そのうち，双方が同じ AV によって応答したものが875,644 個，何の AV も返さないという意味で応答内容が一致したものが 14,216,639 個あった．結果として，合わせて 99%以上，15,092,283 個の問合せにおいて，応答内容が SELinux
と本言語で同一であった．また，残りの約 0.05%，7,879 個の問合せは応答内容が一致して

5. ポリシ記述言語の評価いなかった．

本章では，本言語の有用性を評価するために行った実験の結果とその考察を示す．はじめ

5.3 記述量の比較による表現力の評価実験に，本言語の妥当性を確認するために，SELinux で利用されているポリシを本言語を用い本節では，SELinux のポリシを本言語で表現する場合に必要となる記述量を，ポリシをて実際に構成し，認可判定時の応答内容の同一性を確認することで，本言語が論理的に正し構成するために必要となるソースコードの行数とリスティングした場合のページ数によってく動作していることを実証した．その後，本言語の表現力を評価するために，同内容のポ比較した結果を示す（表 1）．

リシを構成するために必要な記述量を SELinux のポリシ記述手法と本言語で複数の観点か

本言語においては 4 章で示した表現手法を用いることで，同内容のアクセス制御規則で

ら定量的に比較し，本言語の表現手法が実際のポリシを簡潔に表現できることを確認した．

あっても多様な表現を許容するため，本実験では特に 2 種類の方式で記述を行った．1 つ目

最後に，これらの結果をふまえて本言語の利害得失について考察する．

は，ケイパビリティリスト（C-List）26) のようにアクセス主体の属性としてのソースコンテ

5.1 実験システムの構成

キストを定数項として指定し，アクセス対象の属性としてのターゲットコンテキストとセ，メモリ 1 GB の計算機上に実装したもので，OS 環
実験システムは，Pentium4（3.0 GHz）

キュリティクラス，操作内容としての AV を変数項として指定したうえで，条件節内でそれ境は，Debian/GNU Linux に SELinux 関連のパッケージを追加したものを利用する．主要なら変数項の内容を具体的に特定する記述方式で，2 つ目は，アクセス制御リスト（ACL）27)

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan


1689

論理プログラミングを基礎とした認可ポリシ記述言語
表 1 ソースコード行数とリスティングページ数の比較
Table 1 SLOC comparison of policy expressions.

`````` 評価指標 ソースコード行数
```
評価対象
`
SELinux ポリシソース
提案言語記述方式（C-List）
提案言語記述方式（ACL）

表現力の評価実験では，本言語による記述方式により SELinux のポリシを少ない記述量で構成できることを示したが，これは，アクセス制御規則を定めるのに必要な多くの指定

リスティングページ数

を条件節にまとめたからであり，結果として，各規則に対する条件節の内容が多くなってい

133
95
96

る．そのため，必要な要素を直接指定している SELinux の記述手法の方が，各々の規則を

6,524
335
356

個別に見た場合には内容を直感的に把握しやすい．一方で，本言語の記述手法では，アクセス制御規則を階層化やサブルーチン化によってある程度まとめて記述するため，各々の規則を見た場合の可読性はそれほどよくないが，ポリシ全体としての見通しは向上している．

のようにアクセス対象の属性としてのターゲットコンテキストを定数項として指定し，アク

したがって，SELinux のポリシ記述手法のような直接要素を指定する表現と，本言語のよ

セス主体の属性としてのソースコンテキストとセキュリティクラス，操作内容としての AV

うな変数項と条件節を用いた表現は，双方に異なる特徴があるため，利害得失は利用フェーを変数項として指定したうえで，条件節内でそれら変数項の内容を具体的に特定する記述方

ズに依存すると考えられる．たとえば，他の規則と関連性を持たないような少数のアクセス式である．

制御規則を厳密に記述していきたいような場合は前者の記述手法が適しているし，様々な認

この実験では，SELinux の記述手法によってソースコード行数 6,524 行で記述されたポ可判定で共有されるアクセス手順が多く存在し，それをまとめて指定したい場合や，アクリシが，本言語を利用した C-List 式の記述方式では 335 行，ACL 式の記述方式では 356

セス制御規則の総数が膨大になるため，柔軟な構造化が必要な場合には後者の方が適して行で記述された．また，リスティングしたページ数としては，SELinux ポリシのソースファいる．

イルで 133 ページあったものが，本言語で記述した場合に C-List 式，ACL 式それぞれで95 ページ，96 ページになった．
5.4 実験結果の考察

6. ま と め
本稿では，論理プログラムとしてアクセス制御規則を表現することで，属性の継承やサブ妥当性の評価実験では，アクセス可として判定された問合せとアクセス不可として判定さルーチンとして構造化された記述が可能なポリシ記述言語を提案し，多層防御を効果的に適れた問合せで計 99%以上の応答内容が一致したが，一部応答内容が一致しないケースが確用する際に課題となるポリシ記述に係る複雑性を解決する手法を示した．本言語は，個々の認された．この原因は，システム運用時に動的に生成されるコンテキストに対して問合せ

アクセス制御規則を記述するための宣言文と，宣言文の集合として構成されたポリシに問合を行ったことによるもので，これについては認可判定時の引数の渡し方に依存するものでせを行うための認可判定文を，構文規則とその形式的な意味，推論規則を定めることで基本ある．そのため，この解決は認可判定機構の外部で工夫する必要があるが，一方で，元々の設計を行い，これを Prolog のサブセットである Datalog を用いて実装している．また，本SELinux の認可判定がポリシの記述に対して妥当であることを前提としたとき，本言語に稿では，本言語を用いて具体的なアクセス制御モデルを構造的に記述する手法を示したうえよるポリシ記述とそれに基づいた認可判定自体も妥当であったといえる．したがって，こので，SELinux のポリシを実際に記述した実験システムを構成し，認可判定の妥当性と表現

実験結果により，論理プログラミングを基礎とした本言語が，現実のポリシを論理的に正し力の評価を行った．妥当性の評価実験では，SELinux の認可判定が妥当であることを前提とく記述することができることを示した．

したときに，本言語による認可判定が論理的に正しい応答を示し，妥当であることを実証しこの応用としては，論理プログラミングの持つ特徴をアクセス制御に適用することで，たた．さらに，表現力の評価実験では，本言語を用いた記述手法が SELinux のポリシを少なとえば，変数を用いた問合せによりポリシの検証を柔軟に行い，その検証結果をアクセス制

い記述量で構成できることを示し，両実験結果から本言語の有用性について考察を行った．

御の条件として記述すること，メタな規則によって新規則の追加方法や既存規則の変更を制

今後は，まず，2.3 節で期待される効果として示したような本言語の応用について，実際御すること，認可判定に利用する引数を認可判定機構が状況に応じて変更することなどが考に実現する方式について検討する．また，本言語を用いて実際のシステムのアクセス制御をえられる．

行うような認可判定機構を構成し，OS などのアクセス制御機構と連携させる方式について

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan


1690

論理プログラミングを基礎とした認可ポリシ記述言語も検討する．その際には，認可判定機構そのものをセキュアに構成するため，また，性能を向上させるという観点からも，Datalog の処理系をカーネルに埋め込むことを計画している．
謝辞 貴重なご助言をいただいた編集委員と匿名査読者の方々に感謝いたします．

参

考

文

献

1) Bass, T. and Robichaux, R.: Defense-in-depth revisited: Qualitative risk analysis methodology for complex network-centric operations, Military Communications
Conference, 2001. MILCOM 2001. Communications for Network-Centric Operations: Creating the Information Force. IEEE, Vol.1, pp.64–70 (2001).
2) Loscocco, P. and Smalley, S.: Integrating Flexible Support for Security Policies
into the Linux Operating System, Proc. FREENIX Track: 2001 USENIX Annual
Technical Conference, Berkeley, CA, USA, USENIX Association, pp.29–42 (2001).
3) Warren, D.H.D., Pereira, L.M. and Pereira, F.: Prolog – the language and its implementation compared with Lisp, Proc. 1977 Symposium on Artificial Intelligenceand Programming Languages, New York, NY, USA, ACM, pp.109–115 (1977).
4) Ceri, S., Gottlob, G. and Tanca, L.: What you always wanted to know about Datalog (and never dared to ask), IEEE Trans. Knowledge and Data Engineering, Vol.1,
No.1, pp.146–166 (1989).
5) Ferraiolo, D.F. and Kuhn, D.R.: Role-Based Access Control, 15th National Computer Security Conference, Baltimore, MD, pp.13–16 (1992).
6) Tidswell, J. and Potter, J.: An approach to dynamic domain and type enforcement,
Lecture Notes in Computer Science, Vol.1270, pp.26–37 (1997).
7) Banerjee, A. and Naumann, D.: History-based access control and secure information ﬂow, Lecture Notes in Computer Science, Vol.3362, pp.27–48 (2005).
8) Spencer, R., Corporation, S.C., Smalley, S., Loscocco, P., Agency, N.S. andAndersen, M.H.D.: The Flask Security Architecture: System Support for Diverse
Security Policies, Proc. 8th USENIX Security Symposium, pp.123–139 (1999).
9) KaiGai, K.: Security Enhanced PostgreSQL (2006).
http://code.google.com/p/sepgsql/10) Macmillan, K., Brindle, J., Mayer, F., Caplan, D. and Tang, J.: Design and implementation of the SELinux policy management server, Proc. Security Enhanced
Linux Symposium, pp.1–6 (2006).
11) Abadi, M.: On SDSI’s linked local name spaces, J. Comput. Secur., Vol.6, No.1-2,
pp.3–21 (1998).
12) Ellison, C., Frantz, B., Lampson, B., Rivest, R., Thomas, B. and Ylonen, T.: SPKI
Certificate Theory, chapter 2693, RFC Editor (1999).
13) Blaze, M., Feigenbaum, J. and Strauss, M.: Compliance Checking in the Policy-

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

Maker Trust Management System, FC ’98: Proc. 2nd International Conference on
Financial Cryptography, London, UK, pp.254–274, Springer-Verlag (1998).
14) Blaze, M., Feigenbaum, J. and Keromytis, A.D.: KeyNote: Trust Management for
Public-Key Infrastructures (Position Paper), Proc. 6th International Workshop on
Security Protocols, London, UK, pp.59–63, Springer-Verlag (1999).
15) Becker, M., Fournet, C. and Gordon, A.: Design and Semantics of a Decentralized
Authorization Language, CSF ’07: Proc. 20th IEEE Computer Security Foundations Symposium, Washington, DC, USA, IEEE Computer Society, pp.3–15 (2007).
16) Halpern, J.Y. and Weissman, V.: Using First-Order Logic to Reason about Policies, ACM Trans. Inf. Syst. Secur., Vol.11, No.4, pp.1–41 (2008).
17) OASIS: eXtensible Access Control Markup Language (XACML) Version 2.0 core
speciﬁcation (2005).
http://www.oasis-open.org/committees/xacml/
18) Rao, P., Sagonas, K.F., Swift, T., Warren, D.S. and Freire, J.: XSB: A System
for Eﬀciently Computing WFS, LPNMR ’97: Proc. 4th International Conference
on Logic Programming and Nonmonotonic Reasoning, London, UK, pp.431–441,
Springer-Verlag (1997).
19) Chen, W. and Warren, D.S.: Tabled evaluation with delaying for general logic
programs, J. ACM, Vol.43, No.1, pp.20–74 (1996).
20) Chen, W., Kifer, M. and Warren, D.S.: HiLog as a platform for database languages, Proc. 2nd international workshop on Database programming languages, San
Francisco, CA, USA, pp.315–329, Morgan Kaufmann Publishers Inc. (1989).
21) Dawson, S., Ramakrishnan, C.R., Ramakrishnan, I.V., Sagonas, K., Skiena, S.,
Swift, T. and Warren, D.S.: Uniﬁcation factoring for eﬃcient execution of logic
programs, POPL ’95: Proc. 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA, ACM, pp.247–258 (1995).
22) Wielemaker, J., Huang, Z. and Van der meij, L.: Swi-prolog and the web, Theory
Pract. Log. Program., Vol.8, No.3, pp.363–392 (2008).
23) Apt, K.R.: Introduction to Logic Programming, Technical report, Austin, TX,
USA (1988).
24) Brewer, D. and Nash, M.: The Chinese Wall security policy, Proc. IEEE Symposium on Security and Privacy, pp.206–214 (1989).
25) Ahmed, T. and Tripathi, A.R.: Speciﬁcation and veriﬁcation of security requirements in a programming model for decentralized CSCW systems, ACM Trans. Inf.
Syst. Secur., Vol.10, No.2, p.7 (2007).
26) Fabry, R.S.: Capability-based addressing, Comm. ACM, Vol.17, No.7, pp.403–412(1974).
27) Saltzer, J. and Schroeder, M.: The protection of information in computer systems,

c 2010 Information Processing Society of Japan


1691

論理プログラミングを基礎とした認可ポリシ記述言語

辻Proc. IEEE, Vol.63, No.9, pp.1278–1308 (1975).

秀典（正会員）(平成 21 年 11 月 30 日受付)

1996 年東京工業大学工学部情報工学科卒業．2001 年東京大学大学院(平成 22 年 6 月 3 日採録)

工学系研究科情報工学専攻修了，博士（工学）．株式会社インターネット
総合研究所を経て，2002 年株式会社情報技研を設立．同代表取締役社長．

橋本 正樹（正会員）

2004 年情報セキュリティ大学院大学客員准教授兼任，現在に至る．IEEE，2001 年立命館大学文学部人文総合科学インスティテュート卒業．同在

ACM，USENIX 各会員．電子情報通信学会 HCG，料理メディア研究会

学中に有限会社ワイプ設立・取締役情報システム担当就任．2010 年情報セ専門委員．主な著書は『できる PRO Linux/Fedora』シリーズ（インプレスジャパン）．

キュリティ大学院大学情報セキュリティ研究科修了，博士（情報学）．2010
年 4 月より情報セキュリティ大学院大学情報セキュリティ研究科助教．同

田中 英彦（名誉会員）

研究科にて，主に OS によるアクセス制御の研究と教育に従事．電子情報

1970 年東京大学大学院工学系研究科電気工学専門課程修了，工学博士．

通信学会，IEEE 各会員．電子情報通信学会 ISS・情報通信システムセキュリティ研究会専

東京大学にて計算機アーキテクチャ，並列処理，人工知能，自然言語処理，

門委員．

分散処理，メディア処理等の教育・研究に従事．東京大学工学部教授，同大学院情報理工学系研究科長を経て，2004 年情報セキュリティ大学院大金美羅（正会員）学情報セキュリティ研究科長・教授．情報処理学会名誉員，人工知能学会

1996 年釜慶大学自然科学部電子計算学科卒業．1998 年同大学院修士課

論文賞，ACM SIGGRAPH’99 Impact Paper Award，人工知能学会功績賞，東京都科学程修了．2003 年東京大学大学院情報理工学系研究科電子情報学専攻博士

技術功労者表彰，経済産業大臣表彰等受賞．情報・システム研究機構教育研究評議会評議課程修了，博士（情報理工学）．同年東京大学生産技術研究所研究員．2004

員，日本学術会議会員，IEEE Fellow，東京大学名誉教授．

年情報セキュリティ大学院大学助教．セキュアシステムの研究開発に従事．

2009 年情報セキュリティ大学院大学客員研究員．電子情報通信学会会員．

情報処理学会論文誌

Vol. 51

No. 9

1682–1691 (Sep. 2010)

c 2010 Information Processing Society of Japan