2017 Fiscal Year Annual Research Report
Formal models for quantitative analysis of software security
| 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 |
最終年度：形式級数Sと自然数dに対し，CC(S,d)によって長さdの語のSにおける係数の総和を表し，SC(S,d)によって長さdの語でSにおける係数が非ゼロである個数を表す．本研究では，認識可能級数Sと自然数に対し，CC(S,d)をO(log d)時間で計算するアルゴリズム，代数的級数Sに対してCC(S,d)をdの2乗オーダの時間で計算するアルゴリズム等を提案した．代数的級数に対する提案アルゴリズムは既存の計数ツールABCよりも多くの場合でより正確な計数を行えることを示した．
研究期間全体：暗号システムを，未知の鍵を入力とし実行時間を出力とする通信路であると解釈すると，攻撃者が得られる情報量は通信路の相互情報量（量的情報流）を超えない．本研究ではRSA 暗号の復号アルゴリズムを想定しその量的情報流を精密に算出した．
データベースにおける許可問合せ，スキーマ，問合せの意味等の公開情報を組み合わせて禁止問合せの結果を推論する攻撃によって秘匿問合せの結果がk 個未満に絞りこめないときデータベースはk-安全であるという．本研究では命題論理式のモデル計数問題に帰着してk-安全性を検査する手法を開発し，k-安全性検査システムを実装して有効性を確認した．
量的情報流解析を，背景理論付き論理式のモデル計数問題（#SMT）に帰着する手法がある．本研究では，#SMTツールにおいて充足不能コアとモデルのキャッシュを利用する改良を前提とし，SMTツールを利用して得られるモデルから出力変数のサンプル値を取得し確率的に効率の良い探索順を求める手法，簡単な充足可能性判定を前処理として行い探索空間を小さくする手法，ビットレベルの静的解析を行い効率の良い探索順を得る手法を提案し試作ツールによりその有効性を確認した．
|
