| 研究概要 |
量的情報流の困難性に関する研究を行った。Shannon entropy, min entropy, guessing entropy, beliefなど様々な情報理論的尺度に基づく量的情報流の定義が提案されてきたが、それぞれにつき、システムの情報漏洩量の上限を検査するという「量的情報流上限問題」の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も明らかにした。
また、量的情報流検証問題に対する検証アルゴリズムを提案した。具体的には、量的情報流上限問題をself compositionと呼ばれるプログラム変換を用いてソフトウェアモデル検査の問題に帰着する手法を考案した。また、#SAT等のcounting algorithmを用いた量的情報流推論アルゴリズムの研究も行った。
また、上記の検証アルゴリズムの基礎となるソフトウェアモデル検査技術の抜本的改良を目指した研究を行った。具体的には以下の成果を得た。1.)高階関数を含むプログラムに対して世界初の相対的完全なソフトウェアモデル検査の枠組みを提案した。2.) 高階関数を含むプログラムに対する世界初の相対的完全である二項到達可能性解析を用いた停止性の検証手法を提案した。
|
