研究課題
本年度は、 量的情報流の検証の理論的困難性を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)
2: おおむね順調に進展している
交付申請書に記載した「研究の目的」は量的情報流の正確な検証の困難性の解明と実用的な検証手法の開発である。研究実績の概要で述べた通り、研究はおおむね順調に進展していると思われる。
研究計画での計画に沿い、引き続き量的情報流の検証の困難性についての検証と実用的な検証手法の開発を行う。
国内外の学会に参加するための旅費および参加費に研究費を使用する。また、雑誌論文の掲載費および別刷り代金として研究費を使用する。
すべて 2013 2012
すべて 雑誌論文 (3件) (うち査読あり 2件) 学会発表 (6件) (うち招待講演 2件)
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), ACM
巻: n/a ページ: 75-86
10.1145/2429069.2429081
Proceeings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science, Springer
巻: 7294 ページ: 2
10.1007/978-3-642-29822-6_2
Proceedings of the 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science
巻: 85 ページ: 77-91
10.4204/EPTCS.85.6
