| 研究課題/領域番号 |
23700026
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
寺内 多智弘 名古屋大学, 情報科学研究科, 准教授 (70447150)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2014-03-31
|
| キーワード | 量的情報流 / プログラム検証 / セキュリティ / プログラミング言語 |
|---|
| 研究概要 |
量的情報流(Quantiative Information Flow)とは、機密情報を扱うプログラムが機密情報を漏洩する量をShannon Entropyなど情報理論の概念に基づき正式に定義したものである。本研究の目的は、量的情報流にて定義される、プログラムが機密情報の漏洩量を、静的プログラム解析・モデル検査などのプログラム検証の手法を用い、自動的に推論ないしその上限の検証をしようというものである。本年度は、量的情報流の困難性についての研究を推進した。具体的には、主に、プログラムの量的情報流が与えられた実数値以下であるかということを判定する「量的情報流の上限問題」についての困難性について研究を進めた。既存研究で扱われていなかった、Belief, Min Entropy Channel Capacity, Guessing Entropy Channel Capacityなどの情報理論の概念に基づく量的情報流も対象とした。これにより、これらのいくつかの場合は(例えば全分布でBeliefの上限を検証する場合)は比較的容易に検証が可能であり、モデル検査による到達性検証など既存の手法が有効であることが明らかになった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
「実績の概要」で述べたように、当初の計画に沿って、本年度は量的情報流の上限問題の困難性の研究を推進した。
|
| 今後の研究の推進方策 |
研究実施計画に沿い、現実のプログラムへの応用を目指す。ただし、本年度の研究で量的情報流の検証は(既存の手法では)非常に困難である場合が多いということが明らかになったため、応用例を通信プロトコルなど比較的小さなプログラムを対象にするという方針も考慮する。
|
| 次年度の研究費の使用計画 |
情報収集・研究成果発表などの目的で国内外の学会に出席するための参加費および旅費として使用する。また、国内外の学術雑誌への掲載料および論文別刷の費用として使用する。また、検証実験等に使用するハードウェアおよびソフトウェアを購入する。ソフトウェアは、負担をできるだけ軽減するため、有償サポートつきのものを購入する。
|
