2011 Fiscal Year Research-status Report
| Project/Area Number |
23700026
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
寺内 多智弘 名古屋大学, 情報科学研究科, 准教授 (70447150)
|
|---|
| Project Period (FY) |
2011-04-28 – 2014-03-31
|
| Keywords | 量的情報流 / プログラム検証 / セキュリティ / プログラミング言語 |
|---|
| Research Abstract |
量的情報流(Quantiative Information Flow)とは、機密情報を扱うプログラムが機密情報を漏洩する量をShannon Entropyなど情報理論の概念に基づき正式に定義したものである。本研究の目的は、量的情報流にて定義される、プログラムが機密情報の漏洩量を、静的プログラム解析・モデル検査などのプログラム検証の手法を用い、自動的に推論ないしその上限の検証をしようというものである。本年度は、量的情報流の困難性についての研究を推進した。具体的には、主に、プログラムの量的情報流が与えられた実数値以下であるかということを判定する「量的情報流の上限問題」についての困難性について研究を進めた。既存研究で扱われていなかった、Belief, Min Entropy Channel Capacity, Guessing Entropy Channel Capacityなどの情報理論の概念に基づく量的情報流も対象とした。これにより、これらのいくつかの場合は(例えば全分布でBeliefの上限を検証する場合)は比較的容易に検証が可能であり、モデル検査による到達性検証など既存の手法が有効であることが明らかになった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
「実績の概要」で述べたように、当初の計画に沿って、本年度は量的情報流の上限問題の困難性の研究を推進した。
|
| Strategy for Future Research Activity |
研究実施計画に沿い、現実のプログラムへの応用を目指す。ただし、本年度の研究で量的情報流の検証は(既存の手法では)非常に困難である場合が多いということが明らかになったため、応用例を通信プロトコルなど比較的小さなプログラムを対象にするという方針も考慮する。
|
| Expenditure Plans for the Next FY Research Funding |
情報収集・研究成果発表などの目的で国内外の学会に出席するための参加費および旅費として使用する。また、国内外の学術雑誌への掲載料および論文別刷の費用として使用する。また、検証実験等に使用するハードウェアおよびソフトウェアを購入する。ソフトウェアは、負担をできるだけ軽減するため、有償サポートつきのものを購入する。
|
Research Products
(3 results)
