• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証

研究課題

研究課題/領域番号 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: おおむね順調に進展している

理由

研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、自動定理証明・依存型型システムなど高階プログラム検証のための基盤技術の研究および関連技術のセキュリティへの応用において実績をあげた。しかしながら、今回は特に破壊的代入を許す再帰的データ構造に特価する技術についての成果は上げられなかった。

今後の研究の推進方策

引き続き、高階プログラム検証および自動定理証明など関連技術に関する研究を行う。特に、破壊的データと再帰的データ構造の扱いについての研究を進める。

報告書

(1件)
  • 2017 実績報告書

研究成果

(4件)

すべて 2018 2017

すべて 雑誌論文 学会発表

  • [雑誌論文] Relatively complete refinement type system for verification of higher-order non-deterministic programs2018

    • 著者名/発表者名
      Hiroshi Unno, Yuki Satake, and Tachio Terauchi
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: 2 ページ: 1-29

    • DOI
      10.1145/3158100
    • 関連する報告書
      2017 実績報告書
    • 査読あり / オープンアクセスとしている
  • [雑誌論文] Compositional Synthesis of Leakage Resilient Programs2017

    • 著者名/発表者名
      Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
    • 雑誌名

      Proceedings of the 6th International Conference on Principles of Security and Trust (POST 2017), Lecture Notes in Computer Science

      巻: 10204 ページ: 277-297

    • DOI
      10.1007/978-3-662-54455-6_13
    • 関連する報告書
      2017 実績報告書
    • 査読あり / 国際共著/国際学会である / 謝辞記載あり
  • [雑誌論文] Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels2017

    • 著者名/発表者名
      Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei
    • 雑誌名

      Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), ACM SIGPLAN Notices

      巻: 52(6) ページ: 362-375

    • DOI
      10.1145/3062341.3062378
    • 関連する報告書
      2017 実績報告書
    • 査読あり / 国際共著/国際学会である
  • [学会発表] Compositional Synthesis of Leakage Resilient Programs2018

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      NII Shonan Meeting Seminar 115: Intensional and Extensional Aspects of Computation: From Computability and Complexity to Program Analysis and Security
    • 関連する報告書
      2017 実績報告書
    • 国際共著/国際学会である

URL: 

公開日: 2017-04-28   更新日: 2019-07-17  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi