研究者総覧「情報知」
情報システム学専攻
- 氏 名
- 橋本 健二 (はしもと けんじ)
- 講座等
- ソフトウェア論講座
- 職 名
- 助教
- 学 位
- 博士（情報科学）
- 研究分野
- 形式言語理論 / オートマトン / 形式的検証
研究内容
構造化データ変換の自動検証
近年、XMLやRDFなど木やグラフ構造をもつデータが活用されるようになっている。これらのデータに対して、しばしば目的に応じて必要な部分の抽出や適切な構造への整形が行われる。そうした変換の設計においては、データ変換を通して、必要な情報が欠損しないことや、公開するつもりのない情報が特定されてしまう危険性がないことなどが求められる。構造化データ変換におけるそのような性質の定式化を行い、性質を満たすかどうかを自動的に検証するための枠組みやツールの提供を目指す。現在は、木構造データ変換を対象とし、木変換器とよばれる変換モデルを用いて、以下の性質の定式化や形式的な検証手法についての研究を行っている。
（１）情報保存
目的に応じた必要な情報が変換によって損失しないことの保証がしばしば求められる。一方で、情報保存の条件の厳しさと変換の設計の自由度はトレードオフの関係にある。たとえば、情報保存に関して変換が満たすべき条件が必要以上に厳しければ、ほとんど何も変換できなくなる。情報が損失しないことの定式化はさまざま考えられているが、何を情報とみなし保存すべきと考えるかに応じた条件を設定できる枠組みが望ましい。情報保存の一定式化として問合せ保存が知られている。問合せ保存とは、変換前データに対する問合せの結果が、同等なクラスの問合せによって変換後データから引き出せることをいう。変換後データから変換前データを完全に復元できることを求める可逆性といった性質と比べて、問合せ保存は、状況に応じて適切に問合せの集合を指定することで、必要な情報だけを保存することを要求する柔軟な制約になりうる。それゆえ、問合せ保存の検証はデータ変換の情報保存性に関する重要な問題の１つである。しかし、一般には問合せ保存の判定問題は決定不能である。そのため、問合せ保存の自動検証が可能であるような、木やグラフデータに特化した変換・問合せのなるべく現実的なクラスを発見し、検証法の提案と実装を目的として研究している。
（２）推論攻撃に対する耐性
データベースにおいていくつかの変換（ビュー）を通して抽出・整形して情報が外部に提供される場合に、たとえ一見それらが公開可能な必要最低限の情報だけだとしても、それらから公開する意図のない情報が特定されてしまう場合がある。公開されたデータ中に明示的には現れなくても、得られた複数の情報とそれがどのような変換を通して得られたものなのかなどの情報から推論することで、隠しておきたい情報の候補が必要以上に絞り込まれてしまう危険性がある。そのため、あらかじめそのような状況が発生しうるかどうかの検証が必要である。本研究では、いくつかの変換を通してデータが提供されている状況を想定し、k-安全性という推論攻撃に対する尺度を用いている。k-安全性は、直観的には、変換処理の内容と変換結果を用いて推測される尤もらしい変換前のデータの候補数がk個以上であることを意味する。現在は、木変換器を用いて木構造データのk-安全性の形式的な検査手法に関する研究を行っている。
経歴
- 2009年3月 大阪大学大学院情報科学研究科博士後期課程修了．
- 2009年4月～2013年9月 奈良先端科学技術大学院大学情報科学研究科助教．
- 2013年10月 名古屋大学大学院情報科学研究科情報システム学専攻助教．現在に至る．
所属学会
- 電子情報通信学会
- 情報処理学会
主要論文・著書
- C. Phonharath, K. Hashimoto, and H. Seki, ``Deciding Schema k-Secrecy for XML Databases,'' IEICE Transactions on Information and Systems, Vol. E96-D, No. 6, pp. 1268-1277, 2013.
- K. Miyahara, K. Hashimoto, and H. Seki, ``Node Query Preservation for Deterministic Linear Top-Down Tree Transducers,'' In Proc. of TTATT 2013, Vol. 134, pp. 27-37, 2013.
- Y. Ishihara, N. Suzuki, K. Hashimoto, S. Shimizu, and T. Fujiwara, ``XPath Satisfiability with Parent Axes or Qualifiers Is Tractable under Many of Real-World DTDs,'' In Proc. of DBPL 2013, http://arxiv.org/abs/1308.0769, 2013.
- H. Kuwada, K. Hashimoto, Y. Ishihara, and T. Fujiwara, ``The Consistency and Absolute Consistency Problems of XML Schema Mappings between Restricted DTDs,'' In Proc. of APWeb 2013, pp. 228-239, 2013.
- K. Hashimoto, R. Sawada, Y. Ishihara, H. Seki, and T. Fujiwara, ``Determinacy and Subsumption for Single-valued Bottom-up Tree Transducers,'' In Proc. of LATA 2013, pp. 335-346, 2013.
