2015 Fiscal Year Research-status Report
| Project/Area Number |
15K00087
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
南出 靖彦 東京工業大学, 情報理工学研究科, 教授 (50252531)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現 / プッシュダウンオートマトン |
|---|
| Outline of Annual Research Achievements |
正規表現マッチングに起因するサーバサイドプログラムにおける新たな形態の脆弱性（ReDoS 脆弱性）を検出する研究を行った．具体的にはバックトラックに基づく正規表現マッチングの実行時間のオーダを決定する解析アルゴリズムを開発した．正規表現からマッチングの計算過程を表現する先読み付きトップダウン木トランスデューサを構築し，その増加率のオーダを決定している．増加率の解析は，AhoとUllmanによる先読みの無いトップダウン木トランスデューサに対する解析手法を，先読み付きに拡張することで実現している．この解析アルゴリズムを実装し，既存のPHP プログラムで使用されている正規表現を対象に実験を行い，オーダが2乗や３乗となる正規表現の検出に成功した．また，そのオーダの振る舞いを示す入力パターンを生成でき，脆弱性の原因の理解を支援している．
時間の概念を取り入れた時間プッシュダウン・オートマトンの研究を行った．時間プッシュダウン・オートマトンにおける到達可能性問題が決定可能であることは，2012年にAbdullaらによって示されていたが，その証明は非常に複雑であり，表現力も不自然に弱い体系となっていた．それに対して，本研究は小数部検査制約を導入し，さらに体系を一般化することで，SynchronizedRecursive Timed Automataという体系を提案し，小数部検査制約により言語の表現力が広がることを証明した．また、到達可能性問題の決定可能性について，backward-forward simulation を用いて見通しの良い証明を与え，既存の結果よりも強い計算状況に対する到達可能性が決定可能であることを示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
正規表現を用いた文字列操作はウェブプログラム等において重要な役割を果たしており，その計算量を決定するアルゴリズムは実用上非常に有用である．また，理論的にも多項式オーダの次数を木トランスデューサの理論を用いて決定している点が新規性が高い．
|
| Strategy for Future Research Activity |
正規表現に関する研究に関しては，成果を実用的なシステムとして実装し公開する．実用的なシステムとするためには，入力パターンの提示方法をさらに工夫する必要がある．また，実際のプログラムに現れる複雑な正規表現を扱うために，モデル検査の技術を取り入れることを考えている．理論面の研究に関しては，国際会議などへの参加により，国内外の関連分野の研究者との交流を進め，研究を加速する．
|
| Causes of Carryover |
平成27年度中に購入を計画していたノートPC１台について，機種等を検討した結果，次年度に購入することとした．
|
| Expenditure Plan for Carryover Budget |
平成28年度の早い時期に、前年度に計画していたノートPC１台を購入し，効果的に利用し，研究を進める．
|
