Dependent refinement types and predicate constraints for program verification

• Project/Area Number: 23K24826
• Project/Area Number (Other): 22H03570 (2022-2023)
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Multi-year Fund (2024); Single-year Grants (2022-2023)
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Waseda University
• Principal Investigator: 寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
• Co-Investigator(Kenkyū-buntansha): 海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
• Project Period (FY): 2022-04-01 – 2027-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥16,770,000 (Direct Cost: ¥12,900,000、Indirect Cost: ¥3,870,000); Fiscal Year 2026: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2025: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000); Fiscal Year 2024: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2023: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000); Fiscal Year 2022: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
• Keywords: プログラム検証 / 依存篩型 / 述語制約 / 自動定理証明 / 不動点論理 / 型システム / 述語制約解消 / 代数的エフェクト

Outline of Research at the Start

本研究の目標は、型理論と制約解消技術によるソフトウェアプログラムの正しさの検証である。特に、「依存篩型(dependent refinement types)」と「述語制約(predicate constraint)」を用いた手法の深化を目指す。

Outline of Annual Research Achievements

代数的エフェクトハンドラを含むプログラムのための依存篩型によるプログラム検証手法について研究を行った。具体的には、これまでの型推論と述語制約解消による手法を、Answer Type Modificationという限定継続等コントロールエフェクトのための型システムの概念とうまく組み合わせることにより、世界初の代数的エフェクトハンドラの動作を正確に解析することのできる依存篩型システムを開発した。この研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Principles of Programming Languages(POPL)に採録された。

加えて、制約解消による文字列抽出のための正規表現の生成・修正に関する研究と、後方参照により拡張された正規表現の表現力に関する研究を行った。前者の研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Programming Language Design and Implementation(PLDI)に採録された。後者の研究は理論計算機科学分野の難関国際会議であるInternational Symposium on Mathematical Foundations of Computer Science(MFCS)に採録された。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は主に代数的エフェクトハンドラを含むプログラムのための依存篩型システムに関する研究を行い成果を得た。

また、述語制約解消と自動定理証明に関する研究としては、前年度に提案した双対性をうまく用いた解消解消・不動点論理のための自動定理手法について引き続き研究を行っており、こちらの研究もおおむね順調に進展している。

Strategy for Future Research Activity

引き続き述語制約および不動点論理に関する研究を行う。特に、前年度開発した、述語制約への帰着と不動点論理の双対性を用いた新たな不動点論理妥当性判定手法の応用および手法のさらなる深化を目指す。加えて、引き続き代数的エフェクトハンドラや多相再帰(polymorphic recursion)など型システムに関する研究を行う。

Research Products

• [Journal Article] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers (2024)
  • Author(s): Kawamata Fuga, Unno Hiroshi, Sekiyama Taro, Terauchi Tachio
  • Journal Title: Proceedings of the ACM on Programming Languages (POPL) Volume: 8 Issue: POPL Pages: 115-147
  • DOI: 10.1145/3633280
  • Peer Reviewed / Open Access
• [Journal Article] Trace Effects for a Language with Algebraic Effect Handlers (2023)
  • Author(s): 川俣 楓河, 寺内 多智弘
  • Journal Title: Computer Software Volume: 40 Issue: 2 Pages: 2_19-2_48
  • DOI: 10.11309/jssst.40.2_19
  • ISSN: 0289-6540
  • Year and Date: 2023-04-21
  • Peer Reviewed / Open Access
• [Journal Article] On the Expressive Power of Regular Expressions with Backreferences (2023)
  • Author(s): Taisei Nogami, Tachio Terauchi
  • Journal Title: In Proceedings of the 48th Mathematical Foundations of Computer Science (MFCS 2023), Leibniz International Proceedings in Informatics (LIPIcs) 272 Volume: LIPICS
  • Peer Reviewed / Open Access
• [Journal Article] Repairing Regular Expressions for Extraction (2023)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Journal Title: In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), PACMPL 7(PLDI) Volume: 7 Issue: PLDI Pages: 1633-1656
  • DOI: 10.1145/3591287
  • Peer Reviewed / Open Access
• [Journal Article] On Lookaheads in Regular Expressions with Backreferences (2023)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Journal Title: IEICE Transactions on Information and Systems E106-D (5) Volume: 5 Pages: 959-975
  • Peer Reviewed / Open Access
• [Journal Article] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification (2023)
  • Author(s): Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
  • Journal Title: In Proceedings of the 50th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2023), PACMPL 7(POPL) Volume: 7 Issue: POPL Pages: 2111-2140
  • DOI: 10.1145/3571265
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] On Lookaheads in Regular Expressions with Backreferences (2023)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Journal Title: In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) Volume: 228
  • Peer Reviewed / Open Access
• [Journal Article] Repairing DoS Vulnerability of Real-World Regexes (2022)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Journal Title: In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), IEEE Computer Society Volume: S&P 2022 Pages: 2060-2077
  • DOI: 10.1109/sp46214.2022.9833597
  • Peer Reviewed
• [Presentation] Repairing DoS Vulnerability of Real-World Regexes (2024)
  • Author(s): Tachio Terauchi
  • Organizer: NII Shonan Meeting Seminar 159: Web Application Security
  • Int'l Joint Research / Invited
• [Presentation] Repairing Regular Expressions for Extraction (2024)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Organizer: ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
• [Presentation] Nested Data Type における多相再帰のための主要型付けを持つ型システム (2024)
  • Author(s): 川原 知真, 寺内 多智弘
  • Organizer: ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
• [Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers (2024)
  • Author(s): Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi
  • Organizer: ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
• [Presentation] Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness (2024)
  • Author(s): 野上 大成, 寺内 多智弘
  • Organizer: ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
• [Presentation] Repairing DoS Vulnerability of Real-World Regexes (2023)
  • Author(s): Tachio Terauchi
  • Organizer: Technology Challenges in Non-Traditional Security
  • Int'l Joint Research / Invited
• [Presentation] Applications of Program Verification and Synthesis Techniques to Security, from Non-Interference to ReDoS (2023)
  • Author(s): Tachio Terauchi
  • Organizer: Vietnam-Japan Autumn School on Cyber Security
  • Int'l Joint Research / Invited
• [Presentation] Repairing DoS Vulnerability of Real-World Regexes (2023)
  • Author(s): Tachio Terauchi
  • Organizer: NII Shonan Meeting Seminar 180:The Art of SAT
  • Int'l Joint Research
• [Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers (2023)
  • Author(s): Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
  • Organizer: NII Shonan Meeting Seminar 203:Effect Handlers and General-Purpose Languages
  • Int'l Joint Research / Invited
• [Presentation] Repairing DoS Vulnerability of Real-World Regexes (2023)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Organizer: 第22回情報科学技術フォーラム（FIT2023
  • Invited
• [Presentation] On Lookaheads in Regular Expressions with Backreferences (2023)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Organizer: ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
• [Presentation] On Lookaheads in Regular Expressions with Backreferences (Poster Presentation) (2023)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Organizer: ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
• [Presentation] Nested Data Type における多相再帰の型推論手法 (ポスター発表) (2023)
  • Author(s): 川原 知真, 寺内 多智弘
  • Organizer: ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
• [Presentation] 代数的エフェクトハンドラのための篩型システム (ポスター発表) (2023)
  • Author(s): 川俣 楓河, 海野 広志, 関山 太郎, 寺内 多智弘
  • Organizer: ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
• [Presentation] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification (2023)
  • Author(s): Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
  • Organizer: ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
• [Presentation] 後方参照付正規表現の表現力について (2023)
  • Author(s): 野上 大成, 寺内 多智弘
  • Organizer: ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
• [Presentation] Repairing DoS Vulnerability of Real-World Regexes (from IEEE S&P 2022) (2022)
  • Author(s): Nariyoshi Chida, Tachio Terauchi
  • Organizer: 2022年 暗号と情報セキュリティワークショップ
  • Invited