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 |
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥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を開発し一般公開した。投射モデル計数・列挙は、量的情報流解析に限らず、規模の多い解析対象の部分的な性質を解析するのに有用であり今回のツールはそのような解析にも役立つ。
|
Report
(5 results)
Research Products
(5 results)
