Projected Model Counters for Quantitative Information Flow Analysis

• Project/Area Number: 17K00098
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Nagoya University
• Principal Investigator: Hashimoto Kenji 名古屋大学, 情報学研究科, 助教 (90548447)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Project Status: Completed (Fiscal Year 2020)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2017: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
• Keywords: 投射モデル計数 / 量的情報流解析 / BDD / 阻止節 / 変数順序 / d-DNNF / 成分キャッシュ

Outline of Final Research Achievements

Quantitative Information Flow (QIF) was introduced for a quantitative security criterion to capture how much information is leaked though software systems. One way to analyzing QIF is based on projected model counting. In this work, we implemented on the SAT solver GlueMiniSat ROBDD and d-DNNF construction techniques for projected models. Besides, we used our BDD/d-DNNF compilers to analyze dynamic information flow analysis, a variant of QIF analysis, and confirmed its effectiveness.

Academic Significance and Societal Importance of the Research Achievements

モデル計数・列挙技術を共通のSATソルバ上に実装することでそれらを複合的に利用できる環境を構築した。投射モデル計数・列挙を行うツールは一般のモデル計数・列挙のためのツールに比べて公開されているものはまだ少ない。今回、投射モデル計数を行うGPMCや投射モデル集合を表現するROBDDの構築を直接的に行うツールPC2BDDを開発し一般公開した。投射モデル計数・列挙は、量的情報流解析に限らず、規模の多い解析対象の部分的な性質を解析するのに有用であり今回のツールはそのような解析にも役立つ。

Research Products

• [Journal Article] Quantifying Dynamic Leakage - Complexity Analysis and Model Counting-based Calculation - (2019)
  • Author(s): Bao Trung Chu, Kenji Hashimoto, Hiroyuki Seki
  • Journal Title: IEICE Transactions on Information and Systems Volume: E102.D Issue: 10 Pages: 1952-1965
  • DOI: 10.1587/transinf.2019EDP7132
  • NAID: 130007722186
  • ISSN: 0916-8532, 1745-1361
  • Year and Date: 2019-10-01
  • Peer Reviewed
• [Presentation] 命題論理式の全ての投射モデルを表現するBDDの構成法 (2021)
  • Author(s): 磯貝 孝明, 橋本 健二, 酒井 正彦
  • Organizer: 人工知能学会 第116回人工知能基本問題研究会
• [Presentation] On the Compositionality of Dynamic Leakage and Its Application to the Quantification Problem (2019)
  • Author(s): Bao Trung Chu, Kenji Hashimoto, Hiroyuki Seki
  • Organizer: The 30th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE 2019)
  • Int'l Joint Research
• [Remarks] Projected Model Counting and Enumeration
  • URL: https://www.trs.cm.is.nagoya-u.ac.jp/projects/PMC/
• [Remarks] GPMC
  • URL: https://www.trs.cm.is.nagoya-u.ac.jp/~k-hasimt/tools/gpmc.html