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: Minamide Yasuhiko 東京工業大学, 情報理工学院, 教授 (50252531)
• Project Period (FY): 2015-04-01 – 2019-03-31
• Project Status: Completed (Fiscal Year 2018)
• Budget Amount: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000); Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2016: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000); Fiscal Year 2015: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• 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.

Academic Significance and Societal Importance of the Research Achievements

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

Research Products

• [Journal Article] Derivatives of Regular Expressions with Lookahead (2019)
  • Author(s): Takayuki Miyazaki, Yasuhiko Minamide
  • Journal Title: Journal of Information Processing Volume: 未定 Pages: 9-9
  • NAID: 130007663795
  • Peer Reviewed / Open Access
• [Journal Article] Configuration Reachability Analysis of Synchronized Recursive Timed Automata (2018)
  • Author(s): Yuya Uezato and Yasuhiko Minamide
  • Journal Title: Computer Software Volume: 35 Issue: 1 Pages: 1_140-1_168
  • DOI: 10.11309/jssst.35.1_140
  • NAID: 130006356068
  • ISSN: 0289-6540
  • Peer Reviewed / Open Access
• [Journal Article] Weighted Pushdown Systems with Indexed Weight Domains (2016)
  • Author(s): Yasuhiko Minamide
  • Journal Title: Logical Methods in Computer Science Volume: 12 Pages: 1-27
  • DOI: 10.2168/lmcs-12(2:9)2016
  • NAID: 120006582518
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Monoid-based Approach to the Inclusion Problem on Superdeterministic Pushdown Automata (2016)
  • Author(s): Yuya Uezato and Yasuhiko Minamide
  • Journal Title: International Conference on Developments in Language Theory Volume: LNCS 9840 Pages: 393-405
  • DOI: 10.1007/978-3-662-53132-7_32
  • ISBN: 9783662531310, 9783662531327
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Synchronized Recursive Timed Automata (2015)
  • Author(s): Yuya Uezato, Yasuhiko Minamide
  • Journal Title: International Conference on Logic for Programming, Artificial Intelligence, and Reasoning Volume: LNCS 9452 Pages: 249-265
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Presentation] 先読み付き正規表現の微分 (2018)
  • Author(s): 宮嵜 貴之, 南出 靖彦
  • Organizer: 情報処理学会プログラミング研究会 第121回プログラミング研究発表会
• [Presentation] バックトラックによる正規表現マッチングの計算量判定の実装 (2018)
  • Author(s): 高橋 和也, 南出 靖彦
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] 先読み付き正規表現と解析表現の微分 (2018)
  • Author(s): Takayuki Miyazaki, Yasuhiko Minamide
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] Streaming String Transducerの合成の形式的証明 (2018)
  • Author(s): 赤間 仁志, 南出 靖彦
  • Organizer: プログラミングおよびプログラミング言語ワークショップ
• [Presentation] 言語の包含判定に基づくサニタイズ文脈の自動決定 (2018)
  • Author(s): 高橋 和也, 南出 靖彦
  • Organizer: プログラミングおよびプログラミング言語ワークショップ
• [Presentation] バックトラックによる正規表現マッチングの時間計算量解析 (2016)
  • Author(s): 中川みなみ, 南出 靖彦
  • Organizer: 第107回プログラミング研究会
  • Place of Presentation: 福岡市A.R.Kビル
  • Year and Date: 2016-01-13
• [Presentation] 更新可能時間オートマトンの新たな拡張について (2015)
  • Author(s): 上里 友弥, 南出 靖彦
  • Organizer: 日本ソフトウェア科学会第３２回大会
  • Place of Presentation: 早稲田大学
  • Year and Date: 2015-09-08