2008 Fiscal Year Annual Research Report
| Project/Area Number |
20500034
|
|---|
| Research Institution | Nara Institute of Science and Technology |
|---|
Principal Investigator |
関 浩之 Nara Institute of Science and Technology, 情報科学研究科, 教授 (80196948)
|
|---|
| Keywords | アクセス制御 / 情報流解析 / セキュリティ / 実行履歴 / スタック検査 / 自動生成 / 静的解析 |
|---|
| Research Abstract |
「言語組込みアクセス制御」と呼ばれる機構に着目し,ソフトウェアがセキュリティ要求を満たして動作することを保証するための解析・自動生成技術について以下の研究を行った.(1)言組込みアクセス制御モデルの表現能力の比較:AbadiとFournetらによる実行履歴に基づくアクセス制御(HBAC),正則パターンに基づくスタック検査(R-SI),Fongの狭履歴オートマトンの3つの形式モデルについて,そのどの2つの組合せを考えても一方が他方よりも表現能力が大きくないことを証明した.またHBACを拡張し,R-SIより表現能力が大きいモデルを提案した.
(2)情報流仕様からの言語組込みアクセス制御文の自動挿入:プログラムを実行することにより望ましくない情報漏洩が生じる可能性がある.各データをtopsecret,confidential,normal等の機密度によってあらかじめ分類し,プログラムの実行によってどの変数や記憶域にどのような機密度のデータが流れ込んでよいかを規定したものを情報流仕様と呼ぶ.本研究ではプログラムPと情報流仕様Sが与えられたとき,PにHBACで用いられるアクセス検査文を自動的に挿入することによってSを満たすプログラムに変換する手法を考察した.提案手法ではまず,プッシュダウンシステム(PDS)モデル検査法を応用してPを情報流の観点から型推論する.その結果,型エラーを含む代入文が検出されれば,そのような代入文のそれぞれについて次の変換を行う:その代入文前方で最も近いアクセス検査文C(複数あればそれらすべて)において「型エラーの原因となるメソッド呼出しが行われたかどうかを検査し,もし実行された可能性があるならばプログラムを停止する」ようCのパラメタを調整する.
|
