2012 Fiscal Year Research-status Report
| Project/Area Number |
23700026
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
寺内 多智弘 名古屋大学, 情報科学研究科, 准教授 (70447150)
|
|---|
| Keywords | 量的情報流 / プログラム検証 / セキュリティ |
|---|
| Research Abstract |
本年度は、 量的情報流の検証の理論的困難性をhyperpropertiesの概念を用い詳細な分類を行った。Clarksonらにより提案されたhyperproperties[#1]は、プログラム検証において、検証対象の性質の分類に役立つ概念である。具体的には、安全性(safety property)活性(liveness property)などひとつの(もしくは、全部の)プログラム実行トレースに対して定義される古典的な検証対象性質の分類を、トレースの集合に対して定義できるように拡張した枠組みである。例えば、k-safety hyperpropertyは、k個のトレースを用い否定することが可能な性質と定義される。(なので、1-safety hyperpropertyは通常のsafety propertyと一致する。)研究代表者は、この概念を用い、量的情報流の検証の分類を行った。この研究により、例えば、機密情報が一様分布である場合は、Shannon entropyによる量的情報流の検証はあらゆるkに対してk-safety hyperpropertyでないのに対し、min entropyによる量的情報流の検証はあるkに対してk-safety hyperpropertyであることが判明した。
また、プログラム検証全般の研究として、特に高階プログラムに有効なプログラム検証の技術の研究を行った。この研究により、理論的に完全な検証を可能となり、実用的にも、従来の手法では検証不可能であった多数のケースの検証に成功した。
[#1] Michael R. Clarkson, Fred B. Schneider: Hyperproperties. Journal of Computer Security 18(6): 1157-1210 (2010)
|
| 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
(9 results)
