2016 Fiscal Year Research-status Report
ソフトウェアセキュリティのための量を扱う計算モデルの提案
| Project/Area Number |
26540025
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
|
|---|
| Project Period (FY) |
2014-04-01 – 2018-03-31
|
| Keywords | セキュリティ / 量的情報流 / プライバシー |
|---|
| Outline of Annual Research Achievements |
プログラムに入力された機密情報が出力に流出するかどうかを解析することは，情報漏えい対策やプライバシ保護において重要である．このような解析における定量的な尺度として，量的情報流が注目されている．プログラムの量的情報流とは，プログラムfの出力変数Yの値を観測したときに入力変数X の値についてどの程度の情報が得られるかを表す値であり，XとYの相互情報量で定義される．量的情報流を解析する手法の一つとして，量的情報流の計算を背景理論付き論理式のモデル計数問題（#SMT）に帰着する手法が提案されており，背景理論付き論理式の充足可能性判定ツール（SMTソルバ）を用いた#SMTの解を求めるツール（#SMTツール）が実装されている．本年度は，量的情報流解析に用いられる#SMTツールの計算効率の向上を以下の手順で行った．
はじめに，#SMTツールにおいて充足不能コアとモデルのキャッシュを利用する改良を試みた．その改良を前提とし，出力変数値の探索順が計算効率に与える影響をベンチマークプログラムを用いて調査した．次に，SMTツールを利用して得られるモデルから出力変数のサンプル値を取得し，そこから計算効率の向上が確率的に期待できる探索順を求める手法を提案した．また，論理式のレベルで簡単な充足可能性判定を前処理として行うことで探索空間を小さくする手法を提案した．最後に，解析対象プログラムの抽象解釈による静的解析を利用して出力変数値に関するビットレベルの解析を行い，その結果を利用して効率のよい探索順を得る手法を提案した．提案手法を実装したツールを用いて評価実験を行ったところ，モデル数が多いベンチマークについて実行時間を小さくすることができた．また，論理式のレベルでの前処理や静的解析による前処理によって効率の良い探索順を得られることが確認でき，提案手法の有効性を示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
量的情報流を解析する手法として，量的情報流の計算を背景理論付き論理式のモデル計数問題（#SMT）に帰着する手法の高速化については当初の目的を達成することができた．最終段階で文字列データを扱うプログラムの量的情報流解析に取り組んだ．計数法の効果の検討を行った結果，動的計画法を用いることにより改良が可能であることが分かり，理論的考察までを行った．提案手法の評価のため，補助事業期間の延長を申請し承認されたところである．
|
| Strategy for Future Research Activity |
動的計画法に基づく文字列計数アルゴリズムを実装し，評価実験ならびに成果発表を行う予定である．
|
| Causes of Carryover |
平成28年9月，計数法の効果の検討を行った結果，動的計画法を取りいれた改良アルゴリズムを用いれば，当初の目的をより精緻に達成するための計算速度が得られること，そのためには当初の予定よりさらに4ヵ月を要することが判明した．そこで補助事業期間の延長を申請するために，予算の一部を次年度用に残した．
|
| Expenditure Plan for Carryover Budget |
改良アルゴリズムを用いた評価実験と論文発表のための経費として使用する．
|
