2010 Fiscal Year Annual Research Report
| Project/Area Number |
20500034
|
|---|
| Research Institution | Nara Institute of Science and Technology |
|---|
Principal Investigator |
関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
|
|---|
| Keywords | アクセス制御 / 情報流解 / セキュリティ / 実行履歴 / スタック検査 / 自動生成 / 静的解析 |
|---|
| Research Abstract |
「言語組込みアクセス制御」と呼ばれる機構に着目し,ソフトウェアがセキュリティ要求仕様を満たして動作することを保証するため自動生成技術について以下の研究を行った
1.昨年度までに,アクセス制御モデルとしてHistory-based Access Control(実行履歴に基づくアクセス制御)を仮定し,情報流の概念を用いて仕様記述言語を定義した.また,再帰プログラムPとセキュリティ仕様Sに対し,Sにおける機密度を型とみなすことでSの下でのPの型安全性を定義した.前年度までの理論的検討に引き続き,PがSの下で型安全ならば,PはSに対して非干渉性を満たすこと(型安全性は非干渉性の十分条件であること)の証明を完成させた
2.プッシュダウンシステム(PDS)のモデル検査法を利用して自動生成問題を解くアルゴリズムを昨年度提案したが,今年度はそのアルゴリズムを改良した,PDSは再帰プログラム型の簡潔な計算モデルである.提案手法ではまず,与えられたプログラムPにおいて変数値をその機密度(型)に抽象化することによりPをPDS Mに変換する.Mに対してモデル検査を実行し,もし型安全性に反する実行列が発見されれば,その実行列が強制終了されるようMにアクセス検査文を挿入する
3.提案手法に基づいて自動生成システムを実装し,いくつかの例題に対して実験を行った結果,実用的な時間で自動生成が行えることを実証した.具体的に,「互いにセキュリティレベルの異なるk個の入力変数から一つを非決定的に選択して内部変数にその値を代入し,次に,互いにセキュリティレベルの異なるk個の出力変数のいずれか一つにその内部変数の値を書き出す」というプログラムをベンチマークとして実験を行った結果,k=200でも20秒以内で自動生成が可能であることを実証した
|
Research Products
(4 results)
