2017 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 |
1.Leakage Resilienceというサイドチャネル攻撃耐タンパ性に関する研究を行った。本研究課題でも重要な技術であるSMTソルバなど近代自動定理証明アルゴリズムによるプログラム解析が鍵となる。今回は、特に、限量子が入れ子になったSMT問題を効率よく解く手法が求めれられた。成果をまとめた論文を情報セキュリティに関する国際会議POST2017で発表した。最優秀賞論文賞にノミネートされるなど高い評価を得た。2.情報流解析の枠組みにおいて、プログラム検証技術によるタイミング攻撃の検出のための手法を研究した。提案した検証体系は任意のk-safety性質の検証へ適用可能であり、タイミング攻撃以外の応用も期待される。成果をまとめた論文をプログラミング言語に関する国際会議PLDI2017で発表した。採択率は322本中42本・15%であった。3.安全性・活性など様々な時相的仕様を効率よく検証するための統一的検証枠組みについての研究を行った。特に非決定性を含む高階関数型言語プログラムを対象としており、依存型型システムによる合成的手法の提案をした。成果をまとめた論文をプログラミング言語に関する国際会議POPL2017で発表した。採択率は272本中66本・24%であった。
|
| 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 |
引き続き、高階プログラム検証および自動定理証明など関連技術に関する研究を行う。特に、破壊的データと再帰的データ構造の扱いについての研究を進める。
|
