2014 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 – 2016-03-31
|
| Keywords | ソフトウェア検証 / 形式言語理論 / モデル検査 / XML / 情報保存性 / 木オートマトン / 木変換器 / 圧縮 |
|---|
| Outline of Annual Research Achievements |
(1)T1とT2を木変換器とする。ある部分関数fがあって、T2=f(T1)が成り立つとき、T1はT2を決定するという。また、T1がT2を保存しfがT2と同じ変換器のクラスに属するとき、T1はT2を包摂するという。本研究では、T1が単値線形拡張ボトムアップ木変換器、T2が単値ボトムアップ木変換器で与えられるとき、保存性、包摂性の双方がcoNEXPTIMEで決定可能であることを示した。
(2)拡張線形ボトムアップ木変換器の関数性判定が多項式時間判定可能であることを示した。
(3)関係データベースにおいてアクセス制御を前提とするセキュリティ尺度として、（問合せに基づく）l（エル）-多様性という概念を導入した。データベースインスタンスDがl-多様性を満たすとは、アクセス権限のある問合せとその結果に基づいてどのように推論を行っても、Dに含まれるセンシティブな情報（アクセス権限のない情報）の候補をl個未満に絞れないことをいう。l-多様性の判定法として、SQLを用いて定義に基づいて判定する手法と、Dを命題論理式に変換してモデル計数ソルバーを用いて判定する方法とを実装し、実データに基づいて比較を行った。
|
| Research Progress Status |
27年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
27年度が最終年度であるため、記入しない。
|
Research Products
(4 results)
-
-
-
[Presentation] Query-based l-diversity2015
Author(s)
Chittaphone Phonharath, Ryonosuke Takayama, Kenji Hashimoto and Hiroyuki Seki
Organizer
7th International Conference on Advances in Databases, Knowledge, and Data Applications
Place of Presentation
Roma, Italy
Year and Date
2015-05-25 – 2015-05-25
Int'l Joint Research
-
