2016 Fiscal Year Annual Research Report
Large scale verification of higher-order programs
| Project/Area Number |
26330082
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
寺内 多智弘 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (70447150)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | プログラム検証 / ソフトウェアモデル検査 / 型システム / 時相論理仕様 / 抽象解釈 / 述語抽象 / 抽象詳細化 |
|---|
| Outline of Annual Research Achievements |
最終年度には次の研究を実施した。１． 前年度・前々年度に行った研究を継続・発展し、また、将来的研究課題を開拓した(後述)。具体的には、時相論理仕様検証の研究、述語抽象・反例を用いた抽象詳細化などソフトウェアモデル検査の基盤技術の研究、また、オブジェクト指向言語に対する検証技術の研究を引き続き行った。２． プログラム検証技術の応用として、情報セキュリティ研究を行った。具体的には、サイドチャネル攻撃に対する耐タンパー性を持つプログラムの合成の研究と、プログラム検証によるタイミング攻撃の検出の研究を行った。成果をまとめた論文は、それぞれ、国際会議POST 2017とPLDI 2017に採録決定している。
研究期間全体を通じて実施した研究を総括すると、時相論理仕様など型システムによる高階プログラムのためのソフトウェアモデル検査手法が扱える性質の拡張、また、ソフトウェアモデル検査など近代の高精度検証の基盤技術である述語抽象における抽象詳細化の改良、などが主な研究成果として挙げられる。これらの結果は、現実の大規模高階プログラムの高精度な検証の重要なファクターになると期待できる。しかし、現実の大規模ソフトウェアは（特に代数データ構造やオブジェクト等の再帰データ構造に対する）破壊的代入を含むものも多く、検証技術をそのようなプログラミング言語機能へ拡張する必要があるという事実も確認した。今後の研究の展開のための課題とする。例えば、分離論理(separation logic)やエイリアス型など、データ構造に対する破壊的代入を扱うためのプログラム論理・型システム等のアイデアを参考に効果的な検証技術を考える。
|
