Verification of Quantitative Information Flow

• Project/Area Number: 23700026
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Nagoya University
• Principal Investigator: TERAUCHI Tachio 名古屋大学, 情報科学研究科, 准教授 (70447150)
• Project Period (FY): 2011 – 2013
• Project Status: Completed (Fiscal Year 2013)
• Budget Amount: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2013: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2012: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2011: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
• Keywords: セキュリティ / プログラミング言語 / プログラム検証 / 量的情報流 / 情報セキュリティ / プログラム解析 / ソフトウェアモデル検査

Research Abstract

We solved open problems concerning the complexity of various quantitative information flow verification problems. We considered quantitative information flow definitions based on various information theoretic notions such as belief and min entropy channel capacity, and studied the problems both from the computational complexity theoretic aspect and the program verification property classification aspect formalized by the notion of "hyperproperties." We also proposed algorithms for precisely inferring and verifying the quantitative information flow bounds that utilize software model checking and counting algorithms. We also proposed new approaches to software model checking.

Research Products

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