2012 Fiscal Year Annual Research Report
形式言語理論に基づく静的解析法とその安全性検査への応用
| Project/Area Number |
23300008
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
楫 勇一 奈良先端科学技術大学院大学, 情報科学研究科, 准教授 (70263431)
橋本 健二 名古屋大学, 情報科学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2011-04-01 – 2015-03-31
|
| Keywords | ソフトウェア検証 / 形式言語理論 / モデル検査 |
|---|
| Research Abstract |
(1) データベース内に格納されている機密情報の漏えいを防止するため、データベースに対する問合せを許可問合せと禁止問合せに分類するというアクセス制御が一般に用いられる。しかし、許可問合せの結果に基づいて禁止問合せの結果を推論できる場合があり、これを推論攻撃という。本研究では昨年度に引き続き、XML文書を想定したデータベースの推論攻撃耐性を解析する問題について以下の結果を得た。データベースインスタンスtに対する問合せQの結果をQ(t)とかく。データベーススキーマDS、許可問合せQSと禁止問合せQUが与えられたとき、DSを満たすどのようなインスタンスtに対しても、QS(t)から、QU(t)の候補がk個未満に絞り込めないとき、DSはQSとQUに関してk-安全であるという。またQU(t)の候補集合が無限であるとき、∞-安全であるという。本研究では、スキーマDSがXMLスキーマを表現する木オートマトン、QSとQUが決定性線形トップダウン木変換器(LDTT)で与えられたとき、任意のk>1についてk-安全性が決定不能であること、および、∞-安全性はEXPTIME完全であることを示した。また、問合せが先読みつきLDTTで与えられるとき、∞-安全性は2-EXPTIMEで解けることを示した。
(2) 情報保存性に関しては、次の結果を得た。T1とT2を変換器とする。ある部分関数fがあって、T2=f(T1)が成り立つとき、T1はT2を保存するという。また、T1がT2を保存しfがT2と同じ変換器のクラスに属するとき、T1はT2を包摂するという。本研究では、T1が単一線形拡張ボトムアップ木変換器、T2が単一ボトムアップ木変換器で与えられるとき、保存性と包摂性の双方が決定可能であることを示した。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
木言語理論を用いたセキュリティ検証法と情報保存性の解析法の両方について研究が大きく進捗し、前者については昨年度の研究成果を改善した内容が電子情報通信学会論文誌に採択された。また、後者については、形式言語理論分野の著名な国際会議の一つであるLATA 2013に採択された。この内容は本分野の第一人者であるSebastian Manethらからも高く評価され、彼らの研究[BEM13]の契機ともなっている。なお研究代表者らは、後者の国際会議発表を改善した論文を現在海外の専門誌に投稿中である。
これまで情報保存性については、問合せと文書変換の両方を木変換器でモデル化するという問題設定で研究を進めてきた。これは問合せ結果も木構造であることを意味しており、このことから、情報保存性が成り立つためには、木構造も保存しなければならないことを意味する。これに対して年度の後半では、木オートマトンに基づき、入力木からその頂点の部分集合を取り出すような問合せを前提とする情報保存性について考察している。これについても来年度、国際会議発表、学術誌への論文投稿を行う準備が整っている。
[BEM13] M. Benedikt, J. Engelfriet and S. Maneth, Determinacy and Rewriting of Top-Down and MSO Tree Transformations, MFCS 2013, 146-158.
|
| Strategy for Future Research Activity |
(1) XMLデータベースについて、(a) 文書変換に対する情報保存性、(b) 推論攻撃に対するセキュリティ安全性の二つを検討する。
(a)については、文書変換を決定性線形下降型木変換器、問合せを木オートマトンに基づく頂点問合せで与えたときに、情報保存性の決定可能性および決定可能な場合の計算複雑さについても明らかにする。さらに余裕があれば、文書変換のクラスを拡張した場合の決定可能性について考察する。
(b)についてはk-安全性について次の方針で研究を進める。今年度までは与えられたデータベーススキーマを満たすインスタンスがすべてk-安全（もしくは∞-安全）であるかどうかの判定法を検討してきた。今後は問題設定を変えて、与えられた1つのインスタンスがk-安全かどうかを判定するアルゴリズムを考案・開発する。具体的に、木変換器で与えられた問合せをブール式に等価変換し、そのブール式のモデル（ブール式を充足する真偽値割当て）を計数することにより、k-安全かどうかを判定する方法を検討する。
(2) 形式言語理論を用いた解析法の応用として、木文法を用いた構造文書圧縮に関する研究を行う。構造化文書の木表現において、共通の部分構造を一つにまとめることにより圧縮を行うことが可能である。圧縮データに対する問合せを、解凍することなしに行えることは、効率やプライバシーの観点から望ましいと考えられる。そこで、SLCFTGとよばれる木文法を用いて圧縮された構造化文書と、木オートマトンに基づく頂点問合せが与えられたとき、効率よく問合せを評価する方法について考察する。
|
