Software Analysis based on Formaly Language Theory and Its Application to Security Verification

2015 Fiscal Year Final Research Report

• Project/Area Number: 23300008
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Nagoya University (2012-2015); Nara Institute of Science and Technology (2011)
• Principal Investigator: Seki Hiroyuki 名古屋大学, 情報科学研究科, 教授 (80196948)
• Co-Investigator(Kenkyū-buntansha): OGAWA MIZUHITO 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024) ; KAJI YUICHI 奈良先端科学技術大学院大学, 情報科学研究科, 准教授 (70263431) ; HASHIMOTO KENJI 名古屋大学, 大学院情報科学研究科, 助教 (90548447)
• Project Period (FY): 2011-04-01 – 2016-03-31
• Keywords: ソフトウェア検証 / 形式言語理論 / モデル検査 / XML / 情報保存性 / 木変換器 / セキュリティ

Outline of Final Research Achievements

We obtained the following research results on information preservation and security of structured data, especially XML documents, based on tree language theory. A translation v is said to preserve a query q if there is a query q’ that can obtain from v(t) the same result when q is applied to t. We obtained decidability and complexity results on the problem of deciding preservation based on tree transducers and n-ary node queries. An inference attack is a behavior that tries to obtain the result of an unauthorized query by combining the result of authorized queries and other public information. We focused on k-secrecy and l-diversity as security notions against inference attacks. We discussed the decidability of schema k-secrecy problem and also compared the effectiveness of our two proposed methods of deciding l-diversity.

Free Research Field

ソフトウェア基礎理論