量的情報流の正確な検証

• 研究課題/領域番号: 23700026
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: ソフトウエア
• 研究機関: 名古屋大学
• 研究代表者: 寺内 多智弘 名古屋大学, 情報科学研究科, 准教授 (70447150)
• 研究期間 (年度): 2011 – 2013
• 研究課題ステータス: 完了 (2013年度)
• 配分額: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円); 2013年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2012年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2011年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
• キーワード: セキュリティ / プログラミング言語 / プログラム検証 / 量的情報流 / 情報セキュリティ / プログラム解析 / ソフトウェアモデル検査

研究概要

量的情報流の困難性に関する研究を行い、beliefやmin entropy channel capacityなど様々な情報理論的尺度に基づく量的情報流に関する検証・推論問題の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も考察した。また、ソフトウェアモデル検査技術と#SATソルバ等カウンティングアルゴリズムを応用した高精度な量的情報流上限検証・推論アルゴリズムを提案した。また、検証アルゴリズムの基礎となるソフトウェアモデル検査技術の改良に関する研究を行った。

研究成果

• [雑誌論文] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • 著者名/発表者名: Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
  • 雑誌名: Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science 巻: 8410 ページ: 392-411
  • DOI: 10.1007/978-3-642-54833-8_21
  • 査読あり / 謝辞記載あり
• [雑誌論文] Quantitative Information Flow as Safety and Liveness Hyperproperties (2014)
  • 著者名/発表者名: Hirotoshi Yasuoka and Tachio Terauchi
  • 雑誌名: Theoretical Computer Science 巻: - ページ: 167-182
  • DOI: 10.1016/j.tcs.2013.07.031
  • 査読あり / 謝辞記載あり
• [雑誌論文] Automating Relatively Complete Verification of Higher-Order Functional Programs. In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013) (2013)
  • 著者名/発表者名: Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
  • 雑誌名: ACM SIGPLAN Notices 巻: 48(1) ページ: 75-86
• [雑誌論文] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて (2013)
  • 著者名/発表者名: 岩塚卓也,寺内多智弘,結縁祥治
  • 雑誌名: 情報処理学会論文誌 : プログラミング(PRO) 巻: 6(3)
  • NAID: 110009656444
• [雑誌論文] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて (2013)
  • 著者名/発表者名: 岩塚卓弥, 寺内多智弘, 結縁祥治
  • 雑誌名: 情報処理学会論文誌プログラミング(PRO) 巻: 6(3) ページ: 20-32
  • NAID: 110009656444
  • 査読あり
• [雑誌論文] Automating Relatively Complete Verification of Higher-order Functional Programs (2013)
  • 著者名/発表者名: Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
  • 雑誌名: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), ACM 巻: - ページ: 75-86
  • DOI: 10.1145/2429069.2429081
  • NAID: 120006669372
  • 査読あり
• [雑誌論文] Automated Verification of Higher-order Functional Programs (2013)
  • 著者名/発表者名: Tachio Terauchi
  • 雑誌名: Proceeings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science, Springer 巻: 7294 ページ: 2-2
  • DOI: 10.1007/978-3-642-29822-6_2
• [雑誌論文] Quantitative Information Flow as Safety and Liveness Hyperproperties. In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012) (2012)
  • 著者名/発表者名: Hirotoshi Yasuoka and Tachio Terauchi
  • 雑誌名: Electronic Proceedings in Theoretical Computer Science 巻: 85 ページ: 77-91
• [雑誌論文] Quantitative Information Flow as Safety and Liveness Hyperproperties (2012)
  • 著者名/発表者名: Hirotoshi Yasuoka, Tachio Terauchi
  • 雑誌名: Proceedings of the 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science 巻: 85 ページ: 77-91
  • DOI: 10.4204/eptcs.85.6
  • 査読あり
• [雑誌論文] On Bounding Problems of Quantitative Information Flow (2011)
  • 著者名/発表者名: Hirotoshi Yasuoka and Tachio Terauchi
  • 雑誌名: Journal of Computer Security 巻: 19.6 ページ: 1029-1082
• [雑誌論文] On bounding problems of quantitative information flow (2011)
  • 著者名/発表者名: Hirotoshi Yasuoka, Tachio Terauchi
  • 雑誌名: Journal of Computer Security 巻: 19 ページ: 1029-1082
  • DOI: 10.3233/jcs-2011-0437
  • 査読あり
• [学会発表] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • 著者名/発表者名: Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
  • 学会等名: ソフトウェア科学会 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
• [学会発表] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • 著者名/発表者名: Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
  • 学会等名: The 23rd European Symposium on Programming (ESOP 2014)
  • 発表場所: Grenoble, France
• [学会発表] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • 著者名/発表者名: Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
  • 学会等名: ソフトウェア科学会 第16回プログラミングおよびプログラミング言語ワークショ ップ (PPL 2014)
  • 発表場所: 熊本県阿蘇市
• [学会発表] Automating Relatively Complete Verification of Higher-Order Functional Programs (2013)
  • 著者名/発表者名: Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
  • 学会等名: ソフトウェア科学会 第15回プログラミ ングおよびプログラミング言語ワークショップ (PPL 2013)
• [学会発表] 無限小定数と限量子除去法によるハイブリッドシステムの検証 (2013)
  • 著者名/発表者名: 岩塚卓也,寺内多智弘,結縁祥治
  • 学会等名: 情報処理学会 第93回プログラミング研究会
• [学会発表] Automating Relatively Complete Verification of Higher-order Functional Programs (2013)
  • 著者名/発表者名: Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
  • 学会等名: 日本ソフトウェア科学界第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
  • 発表場所: 福島県会津若松 東山温泉 御宿東鳳
• [学会発表] 無限小定数と限量子除去法によるハイブリッドシステムの検証 (2013)
  • 著者名/発表者名: 岩塚卓弥, 寺内多智弘, 結縁祥治
  • 学会等名: 情報処理学会プログラミング研究会
  • 発表場所: 国立情報学研究所
• [学会発表] Automating Relatively Complete Verification of Higher-order Functional Programs (2013)
  • 著者名/発表者名: Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
  • 学会等名: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)
  • 発表場所: Rome, Italy
• [学会発表] On Complexity of Verifying Quantitative Information Flow (2012)
  • 著者名/発表者名: Tachio Terauchi
  • 学会等名: Dagstuhl Seminar 12481 : Quantitative Security Analysis
• [学会発表] Automated Verification of Higher-Order Functional Programs (2012)
  • 著者名/発表者名: Tachio Terauchi
  • 学会等名: Proceedings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science 7294
  • 発表場所: (pp.2. Springer)
  • 招待講演
• [学会発表] On Complexity of Verifying Quantitative Information Flow (2012)
  • 著者名/発表者名: Tachio Terauchi
  • 学会等名: Dagstuhl Seminar 12481: Quantitative Security Analsysis
  • 発表場所: Dagstuhl, Germany
  • 招待講演
• [学会発表] Automated Verification of Higher-order Functional Programs (2012)
  • 著者名/発表者名: Tachio Terauchi
  • 学会等名: The 11th International Symposium on Functional and Logic Programming (FLOPS 2012)
  • 発表場所: 神戸大学
  • 招待講演
• [学会発表] Quantitative Information Flow as Safety and Liveness Hyperproperties (2012)
  • 著者名/発表者名: Hirotoshi Yasuoka, Tachio Terauchi
  • 学会等名: The 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012)
  • 発表場所: Tallinn, Estonia
• [学会発表] Relatively Complete Refinement Types from Counterexamples (2011)
  • 著者名/発表者名: Tachio Terauchi
  • 学会等名: NII Shonan Meeting Seminar 005 : Automated Techniques for Higher-Order Program Verification
• [学会発表] Thread-based code cloning for light-weight context sensitive static race detection (2011)
  • 著者名/発表者名: Toshiyuki Manabe, Tachio Terauchi
  • 学会等名: 4th NSFC-JSPS workshop on Formal Methods
  • 発表場所: 奈良
• [学会発表] Relatively Complete Type System for Higher-order Programs (2011)
  • 著者名/発表者名: Tachio Terauchi
  • 学会等名: NII Shonan Meeting on Automated Techniques for Higher-order Program Verification
  • 発表場所: 神奈川