| 研究課題/領域番号 |
15K00087
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | ソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現 / プッシュダウンオートマトン |
|---|
| 研究実績の概要 |
ウェブ基盤技術の検証のための基礎理論として以下の研究を行った．
１）Web ブラウザに搭載されているクロスサイトスクリプティング保護機構であるXSS Auditor の有効性を検証する研究を行った．XSS Auditor で実行される検査を二つのトランスデューサの包含判定としてモデル化した．トランスデューサの包含判定は一般には決定不能問題であるため，保守的な検査アルゴリズムを実装した．非常に限定された状況においては，XSS Auditorの保護機能が有効であることが検証できた．
２）ウェブプログラムの実装において用いられるテンプレート言語におけるサニタイズ関数の自動挿入に関する研究を行った．Google Closuresテンプレート言語において，文脈に依存するサニタイズ関数の自動挿入が実現されていたが，文脈の概念が明確に定義されておらず，また，正当性の証明についてもいくつかの問題があることが分かった．本研究においては，ラベル付き正規表現を用いて文脈の定義を明確にし，また，文脈自由言語と正規言語の包含判定の考え方により，サニタイズの自動挿入アルゴリズムを再設計し，型健全性として自動挿入アルゴリズムの正しさを証明した．
３）先読み付き正規表現に対して，文字列の組の集合として表示的な意味論を与えた．文字列の各組は，マッチングによって消費される部分と先読みにマッチする部分を表している．このように意味論を与えた時，先読み付き正規表現の意味が，二つの正規言語の直積の有限和で表せることを示した．
４）昨年度行ったStreaming Transducer の合成の構成法に関する研究について，証明支援系Isabelle/HOLによる基礎的な部分の形式化を行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
XSS対策技術などウェブ基盤技術において，形式言語理論を用いたモデル化と検証技術の開発が着実に進んできているが，研究成果の発表の面で一部遅れが生じている．本研究も前半で展開した正規表現マッチングの時間計算量の検査について，他の研究者により関連の大きい論文が出版されたため，研究成果を精査し，差分を十分に明らかし，論文として発表する必要が生じている．
XSS Auditorに関してはこれまで理論的な分析が全く行われておらず，本研究による形式言語理論によるモデル化と検証は新たな方向性を示した研究と言える．
|
| 今後の研究の推進方策 |
検証の基礎となる形式言語理論が複雑なものとなってきており，基盤となる理論については証明支援系Isabelle/HOLによる形式化を行う予定である．
本研究も前半で展開した正規表現マッチングの時間計算量の検査について，いくつかの研究グループにより関連の大きい論文が出版されたため，関連する研究グループの訪問などを通じて議論を進め，研究結果を整理しより適用範囲の広い理論の構築を目指す．
|
| 次年度使用額が生じた理由 |
（理由）関連連研究との差分を整理する必要が生じたため，今年度は国際会議での発表を断念した．そのため，旅費の支出が予定よりも少額となった．
（使用計画）次年度には，研究結果を整理し国際会議等での研究発表を行うことを目指している．最終年度にあたるため，国内外の研究集会での発表を行う予定であり，次年度に繰り越しとなった助成金は主にそのための旅費等に使用する予定である．
|
