| 研究課題/領域番号 |
17H01720
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| 研究分担者 |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2022-03-31
|
| 研究課題ステータス |
交付 (2019年度)
|
| 配分額 *注記 |
17,940千円 (直接経費: 13,800千円、間接経費: 4,140千円)
2019年度: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2018年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2017年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
|
|---|
| キーワード | プログラム検証 / ソフトウェアモデル検査 / 型システム / 自動定理証明 / プログラム論理 / プログラミング言語 |
|---|
| 研究実績の概要 |
1.Leakage Resilienceというサイドチャネル攻撃耐タンパ性に関する研究を行った。本研究課題でも重要な技術であるSMTソルバなど近代自動定理証明アルゴリズムによるプログラム解析が鍵となる。今回は、特に、限量子が入れ子になったSMT問題を効率よく解く手法が求めれられた。成果をまとめた論文を情報セキュリティに関する国際会議POST2017で発表した。最優秀賞論文賞にノミネートされるなど高い評価を得た。2.情報流解析の枠組みにおいて、プログラム検証技術によるタイミング攻撃の検出のための手法を研究した。提案した検証体系は任意のk-safety性質の検証へ適用可能であり、タイミング攻撃以外の応用も期待される。成果をまとめた論文をプログラミング言語に関する国際会議PLDI2017で発表した。採択率は322本中42本・15%であった。3.安全性・活性など様々な時相的仕様を効率よく検証するための統一的検証枠組みについての研究を行った。特に非決定性を含む高階関数型言語プログラムを対象としており、依存型型システムによる合成的手法の提案をした。成果をまとめた論文をプログラミング言語に関する国際会議POPL2017で発表した。採択率は272本中66本・24%であった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、自動定理証明・依存型型システムなど高階プログラム検証のための基盤技術の研究および関連技術のセキュリティへの応用において実績をあげた。しかしながら、今回は特に破壊的代入を許す再帰的データ構造に特価する技術についての成果は上げられなかった。
|
| 今後の研究の推進方策 |
引き続き、高階プログラム検証および自動定理証明など関連技術に関する研究を行う。特に、破壊的データと再帰的データ構造の扱いについての研究を進める。
|
