形式言語理論を駆使したウェブ基盤技術の検証

2018 年度 研究成果報告書

• 研究課題/領域番号: 15K00087
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: ソフトウェア
• 研究機関: 東京工業大学
• 研究代表者: 南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
• 研究期間 (年度): 2015-04-01 – 2019-03-31
• キーワード: ソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現 / プッシュダウンオートマトン / 構文解析

研究成果の概要

ウェブ基盤技術の検証問題から出発し，様々な計算モデルに基づく検証技術の研究を行なった．主な成果としては， バックトラックに基づく正規表現マッチングの実行時間のオーダを決定する解析アルゴリズムの開発があげられる．正規表現からマッチングの計算過程を表現する先読み付き木トランスデューサを構築し，その増加率のオーダを決定している．増加率の解析は，AhoとUllmanによる先読みの無い木トランスデューサに対する解析手法を，先読み付きに拡張することで実現している．既存のPHP プログラムで使用されている正規表現を対象に実験を行い，オーダが2乗や３乗となる正規表現の検出に成功した．

自由記述の分野

ソフトウェア検証

研究成果の学術的意義や社会的意義

本研究で開発した正規表現マッチングの時間計算量解析はウェブソフトウェアのReDoS脆弱性の検出に直接応用可能なものであり，ウェブソフトウェアの信頼性の向上に貢献する．また，本研究で展開した形式言語理論の研究は，ウェブの基盤技術にとどまらずより一般のソフトウェア検証に応用できる．特に，正規表現マッチングの時間計算量解析の理論とストリーミングトランスデューサの合成に関する研究は，今後のソフトウェア検証研究の進展の基盤となるものである．