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

2018 年度 実績報告書

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

研究課題

研究課題/領域番号 17H01720
研究機関早稲田大学

研究代表者

寺内 多智弘  早稲田大学, 理工学術院, 教授 (70447150)

研究分担者 海野 広志  筑波大学, システム情報系, 准教授 (80569575)
研究期間 (年度) 2017-04-01 – 2022-03-31
キーワードプログラム検証 / ソフトウェアモデル検査 / 型システム / 自動定理証明 / 分離論理 / 循環証明
研究実績の概要

依存型・依存エフェクトシステムと一階述語不動点論理(first-order fixpoint logic)による高階プログラムの時相論理仕様検証に関する研究を行った。研究の成果をまとめた論文は理論計算機科学分野におけるトップ国際会議LICS 2018に採録された。また、関連して、一階述語不動点論理式の真偽性を解く自動定理証明アルゴリズムの研究および一階述語不動点論理による双模倣性の検証などのについても研究を推進し、The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)およびThird Workshop on Mathematical Logic and its Applications (MLA 2019)にてこの研究に関する講演を行った。

また、循環証明(cyclic proof)と分離論理(separation logic)に関する研究も行った。具体的には、循環証明による分離論理の定理証明は、再帰データ構造を含む場合カット除去不可能であることを示した。この研究に関してThe 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)、日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)およびMLA2019にて講演を行った。

加えて、サイドチャネル攻撃に対する耐タンパ性の検証など情報セキュリティに関するプログラム検証の研究を行った。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は、特に再帰データ構造に対する破壊的代入を含むプログラムの検証に適したプログラム論理である分離論理のための自動定理証明に関する研究および高階関数を含むプログラムの検証に関する研究を行い成果を得た。来年度以降は、今年度の研究で得た知見をもとに、高階関数および破壊的代入可能な再帰データ構造を含むプログラムの検証に有効な枠組みの構築を目指す。

今後の研究の推進方策

今年度の研究で得られた知見をもとに研究を推進する。これまでの研究から帰納的定義を含む分離論理とリファイント型システムを融合したプログラム検証枠組みが有効と推測され、この枠組みの確立を目指す。分離論理において帰納的定義は再帰データ構造を表すために用いられるが、既存の分離論理を用いた自動プログラム検証は帰納的定義を十分に扱えず再帰データ構造の扱いは不十分である。今後は、分離論理の自動定理証明やポイントサンプリングによる不変条件推論などの技術を応用することにより、効果的な自動検証の枠組みの確立を目指す。また、リファインメント型と融合することにより高階関数の扱いおよび型による柔軟なユーザーインタフェースの提供も期待される。

また、自動・半自動プログラム検証の鍵となる自動定理証明技術についての研究も行う。具体的には、今年度に引き続き循環証明による帰納的定義を含む分離論理のための定理証明および一階述語不動点論理のための自動定理証明の研究を行う。前者は上記の通り再帰データ構造への破壊的代入を含むプログラムの検証に有効な枠組みであり、また、後者の論理は(破壊的データ構造を含むプログラムの検証には直接用いられないが)再帰関数・ループを含むプログラムの検証を直接的に表現することができる。加えて、様々な論理における量化子付き式のためのより効率よい自動証明についての研究も行う。

  • 研究成果

    (9件)

すべて 2019 2018

すべて 雑誌論文 (3件) (うち国際共著 2件、 査読あり 3件、 オープンアクセス 3件) 学会発表 (6件) (うち国際学会 5件、 招待講演 3件)

  • [雑誌論文] A Formal Analysis of Timing Channel Security via Bucketing2019

    • 著者名/発表者名
      Tachio Terauchi, Timos Antonopoulos
    • 雑誌名

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

      巻: 11426 ページ: 29~50

    • DOI

      https://doi.org/10.1007/978-3-030-17138-4_2

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • 著者名/発表者名
      Nanjo Yoji、Unno Hiroshi、Koskinen Eric、Terauchi Tachio
    • 雑誌名

      Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), ACM

      巻: LICS 2018 ページ: 759~768

    • DOI

      10.1145/3209108.3209204

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • 著者名/発表者名
      Satake Yuki、Unno Hiroshi
    • 雑誌名

      Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), Lecture Notes in Computer Science, Springer

      巻: 10981 ページ: 105~123

    • DOI

      10.1007/978-3-319-96145-3_6

    • 査読あり / オープンアクセス
  • [学会発表] Solving First-Order Fixpoint Logic for Program Verification2019

    • 著者名/発表者名
      Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen
    • 学会等名
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • 国際学会 / 招待講演
  • [学会発表] On Cut-Elimination Theorem in Cyclic-Proof Systems2019

    • 著者名/発表者名
      Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
    • 学会等名
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • 国際学会
  • [学会発表] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)
  • [学会発表] On Cut-elimination in Cyclic Proof Systems2018

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)
    • 国際学会
  • [学会発表] Horn Clauses and Beyond for Relational and Temporal Program Verification2018

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)
    • 国際学会 / 招待講演
  • [学会発表] Information Flow Security and its Applications to Side Channel Attack Resilience2018

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      The 4th Franco-Japanese Workshop on Cybersecurity
    • 国際学会 / 招待講演

URL: 

公開日: 2019-12-27  

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

Powered by NII kakenhi