2020 Fiscal Year Annual Research Report
Verification of high-level programs containing mutable higher-order recursive data structures
| Project/Area Number |
17H01720
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | プログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 分離論理 / 循環証明 |
|---|
| Outline of Annual Research Achievements |
再帰データ構造と再帰関数を含むプログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階述語不動点論理(first-order fixpoint logic)に関する研究を行った。特に、constrained Horn clauses(CHCs)を拡張した述語制約クラスの制約解消問題に一階述語不動点論理の定理証明問題を帰着し、制約解消アルゴリズムにより自動定理証明を実現するアルゴリズムを開発した。
また、前年度に引き続き、再帰データ構造に対する破壊的代入を含むプログラムの検証に適したプログラム論理である分離論理(separation logic)についての研究を行った。特に、分離論理のための循環証明(cyclic proof)探索の自動化についての研究を行った。
加えて、タイミング攻撃に対する耐タンパ性の検証に関する研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。また、本手法の枠組みで得られる保証の理論的限界についても研究を行った。これらの研究の成果をまとめた論文は国際論文誌Journal of Computer Securityに採録された。
|
| 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 |
今年度の研究で得られた知見をもとに、研究目的である、オブジェクト指向プログラム検証のための枠組みを設計することを目指す。これまでの研究から、帰納的定義を含む分離論理とリファイント型システムを融合したプログラム検証枠組みが有効と推測され、この枠組みの確立を目指す。分離論理において帰納的定義は再帰データ構造を表すために用いられるが、既存の分離論理を用いたオブジェクト指向プログラムのための自動プログラム検証は帰納的定義を扱えず再帰データ構造の扱いは不十分である。今後は、これまでの研究に引き続き、循環証明による帰納的定義を含む分離論理の自動定理証明および述語制約解消問題への帰着による一階述語不動点論理の自動定理証明の研究を行い、効果的な自動検証の枠組みの確立を目指す。特に、これまでの研究から、後者の論理体系は様々な
プログラム検証の問題を自然に表現できることが分かっており、検証問題を一階述語不動点論理の定理証明の問題に帰着することにより、統一的な検証の枠組みが得られることが期待される。また、リファインメント型と融合することにより高階関数の扱いおよび型による柔軟なユーザーインタフェースの提供も期待される。
加えて、不動点論理と述語制約との関連性の深化および、よりよい述語制約解消のアルゴリズムの開発など述語制約についての研究も行う。
|
