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 |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Project Status |
Granted (Fiscal Year 2020)
|
| 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 Annual Research Achievements |
再帰データ構造と再帰関数を含むプログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階述語不動点論理(first-order predicate fixpoint logic)の真偽性判定問題について研究を行った。この研究の成果について招待制国際セミナーDagstuhl Seminar "Deduction Beyond Satisfiability"にて発表を行い、成果をまとめた論文を国際会議に投稿した。また、関連して、必勝戦略合成による量化子を含む一階述語論理式の真偽性判定に関する研究を行い、予備的研究成果についてのポスター発表をAPLAS 2019で行った。
また、前年度に引き続き、再帰データ構造に対する破壊的代入を含むプログラムの検証に適したプログラム論理である分離論理(separation logic)についての研究を行った。具体的には、循環証明(cyclic proof)による分離論理の定理証明は、再帰的述語定義を含む場合カット除去不可能であることを示した。成果をまとめた論文は国内論文誌コンピュータソフトウェアに採録された。
加えて、タイミング攻撃に対する耐タンパ性の検証に関する研究を行った。また、adaptiveな攻撃に対するゲーム理論による安全性議論の枠組みについても研究を行った。成果をまとめた論文はそれぞれ国際会議POST 2019とCSF 2019に採録された。
|
| 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 |
今年度の研究で得られた知見をもとに、研究目的である、オブジェクト指向プログラム検証のための枠組みを設計することを目指す。これまでの研究から、帰納的定義を含む分離論理とリファイント型システムを融合したプログラム検証枠組みが有効と推測され、この枠組みの確立を目指す。分離論理において帰納的定義は再帰データ構造を表すために用いられるが、既存の分離論理を用いたオブジェクト指向プログラムのための自動プログラム検証は帰納的定義を扱えず再帰データ構造の扱いは不十分である。本年度は、前年度に引き続き、循環証明による帰納的定義を含む分離論理の自動定理証明およびポイントサンプリングによる述語推論による一階述語不動点論理の自動定理証明の研究を行い、効果的な自動検証の枠組みの確立を目指す。特に、これまでの研究から、後者の論理体系は様々なプログラム検証の問題を自然に表現できることが分かっており、検証問題を一階述語不動点論理の定理証明の問題に帰着することにより、統一的な検証の枠組みが得られることが期待される。また、リファインメント型と融合することにより高階関数の扱いおよび型による柔軟なユーザーインタフェースの提供も期待される。
具体的には、以下の研究を行う。１．ポイントサンプリングとテンプレート合成による不変条件推論・整礎関係推論を用いた一階述語不動点論理のための定理証明アルゴリズムの研究。２．循環証明(cyclic proof)による帰納的定義を含む分離論理のための自動定理証明および一階不動点論理のための自動定理証明の研究。３．様々な論理における量化子付き式のためのより効率よい自動証明についての研究も行う。また、再帰的エイリアス型と帰納的定義を含む分離論理には深い関連性があることが予想される。それらを拡張リファインメント型システムとして融合し、検証のためのユーザーインタフェースを確立することを目指す。
|
Report
(3 results)
Research Products
(19 results)
-
-
-
-
-
-
-
-
-
[Journal Article] Compositional Synthesis of Leakage Resilient Programs2017
Author(s)
Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
-
Journal Title
Proceedings of the 6th International Conference on Principles of Security and Trust (POST 2017), Lecture Notes in Computer Science
Volume: 10204
Pages: 277-297
DOI
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
-
