2009 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.アクセス制御モデルとしてHistory-based Access Control(実行履歴に基づくアクセス制御)を仮定し,情報流の概念を用いて仕様記述言語を定義した.さて,情報流に基づくセキュリティ基準として非干渉性(noninterference)が知られている.しかし,非干渉性は一般の再帰プログラムに対しては決定不能である.そこでまず,再帰プログラムPとセキュリティ仕様Sに対し,Sにおける機密度を型とみなすことでSの下でのPの型安全性を定義した.そして,PがSの下で型安全ならば,PはSに対して非干渉性を満たすこと(型安全性は非干渉性の十分条件であること)を証明した.
2.自動生成問題を「再帰プログラムPとセキュリティ仕様Sが与えられたとき,PがSの下で型安全となるようPにアクセス検査文を挿入する問題」と定義し,自動生成問題がco-NP困難であることを証明した.
3.プッシュダウンシステム(PDS)のモデル検査法を利用して自動生成問題を解くアルゴリズムを提案した.PDSは再帰プログラム型の簡潔な計算モデルである.提案手法ではまず,与えられたプログラムPにおいて変数値をその機密度(型)に抽象化することによりPをPDS Mに変換する.Mに対してモデル検査を実行し,もし型安全性に反する実行列が発見されれば,その実行列が強制終了されるようMにアクセス検査文を挿入する.
4.提案手法に基づいて自動生成システムを実装し,いくつかの例題に対して実験を行った結果,実用的な時間で自動生成が行えることを実証した.
|
