Verification of high-level programs containing mutable higher-order recursive data structures
Project/Area Number |
17H01720
|
Research Category |
Grant-in-Aid for Scientific Research (B)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Research Field |
Software
|
Research Institution | Waseda University |
Principal Investigator |
|
Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
Project Period (FY) |
2017-04-01 – 2022-03-31
|
Project Status |
Completed (Fiscal Year 2022)
|
Budget Amount *help |
¥17,940,000 (Direct Cost: ¥13,800,000、Indirect Cost: ¥4,140,000)
Fiscal Year 2021: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2020: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2019: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2018: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2017: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
|
Keywords | プログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 分離論理 / 循環証明 / 代数的エフェクト / ソフトウェアモデル検査 / プログラミング言語 / プログラム論理 |
Outline of Final Research Achievements |
We have achieved the following research results. (1) New methods for temporal property verification of higher-order programs. (2) New results on cyclic proof systems,formal deduction systems for mathematical induction, and new methods for deciding validity of formulas in first-order fixpoint logic with background theories. (3) A new type and effect system for verifying temporal properties of programs with algebraic effects and handlers, an emerging programming language feature for uniformly expressing a variety of computational effects including destructive updates. (4) Research achievements on the application of program verification and synthesis techniques to security, such as a method for repairing real-world regular expressions vulnerable to ReDoS attacks. (5) New results on the formal language theory of regular expressions extended with real-world features such as backreferences and lookaheads.
|
Academic Significance and Societal Importance of the Research Achievements |
非決定的動作を含む高階プログラムについて初の相対的完全な検証を実現するリファインメント型システムの提案、様々な問題の解決に応用できる一階不動点論理の妥当性判定のための新しいアルゴリズムを提案、深刻なセキュリティ脅威であるReDoS脆弱性を修復するため初のプログラム合成手法の提案など、本研究はこれまでのプログラミング言語・形式検証・定理証明・セキュリティの研究を大きく飛躍させた。よって、本研究の成果は極めて高い学術的および社会的意義を持つと考える。
|
Report
(6 results)
Research Products
(24 results)
-
-
-
-
-
[Journal Article] A Formal Analysis of Timing Channel Security via Bucketing2019
Author(s)
Terauchi Tachio, Antonopoulos Timos
-
Journal Title
In Proceedings of the 8th International Conference on Principles of Security and Trust (POST 2019), Lecture Notes in Computer Science
Volume: 11426
Pages: 29-50
DOI
ISBN
9783030171377, 9783030171384
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-