2018 Fiscal Year Final Research Report
Verification of Web technologies based on the theory of formal languages
| Project/Area Number |
15K00087
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | ソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現 / プッシュダウンオートマトン / 構文解析 |
|---|
| Outline of Final Research Achievements |
Starting from verification problems related to the foundation of Web technologies, we have investigated the theory and practice of verification based on various computation models. Our main contribution is that we developed an analysis that determines the order of execution time for regular expression matching based on backtracking. The analysis first constructs a tree transducer with lookahead simulating search of regular expression matching and then determines the growth rate of the tree transducer. The growth rate was determined by extending the analysis for tree transducers without lookahead by Aho and Ullman. We conducted experiments on regular expressions obtained from publicly available PHP programs and successfully found regular expressions with quadratic and cubic orders.
|
| Free Research Field |
ソフトウェア検証
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究で開発した正規表現マッチングの時間計算量解析はウェブソフトウェアのReDoS脆弱性の検出に直接応用可能なものであり，ウェブソフトウェアの信頼性の向上に貢献する．また，本研究で展開した形式言語理論の研究は，ウェブの基盤技術にとどまらずより一般のソフトウェア検証に応用できる．特に，正規表現マッチングの時間計算量解析の理論とストリーミングトランスデューサの合成に関する研究は，今後のソフトウェア検証研究の進展の基盤となるものである．
|
