暗号技術に基づく関数を用いたプログラムに対する情報フロー解析法の開発

本年度は,暗号技術に基づく関数を用いたプログラムに対する情報フロー解析に関して以下の研究を行った・解析モデルと解析アルゴリズムの評価・拡張新たに標準化され,実装が進んでいる暗号技術を調査し,その性質を現在の解析モデルで表現できるか否かを調査した.具体的には,長期署名の標準規格であるXAdESを調査した.XAdESで用いられている暗号技術はハッシュ関数,ディジタル署名,タイムスタンプである.解析モデルはハッシュ関数とディジタル署名の性質を記述できるようになっている.XAdESで用いられるタイムスタンプはディジタル著名の一種であることが確認できた.よって,昨年度のモデルで表現できることが分かった.また実際に解析モデルに従って記述した.・解析アルゴリズムの健全性の証明昨年度提案した解析アルゴリズムが定義した健全性を満たすことの証明を行った.昨年度提案した解析モデルには多くの暗号技術の性質を反映したため,健全性の定義が従来の定義と異なっている.また,解析アルゴリズムの構成も従来と異なっている.そのため従来の証明テクニックがそのまま使えない.よって今年度は新たに,公理系に基づく証明テクニックを用いて健全性の照明を行った.・情報フロー解析システムの開発昨年度提案した解析アルゴリズムを計算機上に実装し,その性能を実験的に評価した.解析対象のプログラムはXAdESを実装したものである.効率を向上させるため,解析対象のプログラムにおける情報フローを表すオートマトンを簡約化する処理を含めた.その結果,大幅に効率が向上することが確認できた.

本年度は,暗号技術に基づく関数を用いたプログラムに対する情報フロー解析に関して以下の研究を行った・解析モデルと解析アルゴリズムの評価・拡張新たに標準化され,実装が進んでいる暗号技術を調査し,その性質を現在の解析モデルで表現できるか否かを調査した.具体的には,長期署名の標準規格であるXAdESを調査した.XAdESで用いられている暗号技術はハッシュ関数,ディジタル署名,タイムスタンプである.解析モデルはハッシュ関数とディジタル署名の性質を記述できるようになっている.XAdESで用いられるタイムスタンプはディジタル著名の一種であることが確認できた.よって,昨年度のモデルで表現できることが分かった.また実際に解析モデルに従って記述した.・解析アルゴリズムの健全性の証明昨年度提案した解析アルゴリズムが定義した健全性を満たすことの証明を行った.昨年度提案した解析モデルには多くの暗号技術の性質を反映したため,健全性の定義が従来の定義と異なっている.また,解析アルゴリズムの構成も従来と異なっている.そのため従来の証明テクニックがそのまま使えない.よって今年度は新たに,公理系に基づく証明テクニックを用いて健全性の照明を行った.・情報フロー解析システムの開発昨年度提案した解析アルゴリズムを計算機上に実装し,その性能を実験的に評価した.解析対象のプログラムはXAdESを実装したものである.効率を向上させるため,解析対象のプログラムにおける情報フローを表すオートマトンを簡約化する処理を含めた.その結果,大幅に効率が向上することが確認できた.