トロイフリー暗号ハードウェアの高水準設計・検証手法の開拓

点击翻译按钮获取中文摘要

本年度では，(i)ハードウェアトロイ（HT）のトリガー条件の特定手法，(ii)挿入箇所特定手法の２つの確立を目指して研究を行った．まず(i)については，HTが挿入された組み合わせ回路と，設計仕様であるガロア体方程式との間で，出力差分を取ることでHTの作動条件を特定する手法を開発した．具体的には，まず，検証対象となる回路の各プライマリ出力について，その論理機能をプライマリ入力変数で書き下した方程式を導出する．この導出過程における多項式表現に，ゼロサプレス型二分決定グラフ（ZDD)を用いることで，高速な多項式導出を可能とする．次に，回路機能を表す多項式と，設計仕様となるガロア体方程式の間で差分を取ることで，HTの機能を表現した方程式を導出する．最後に，この差分の方程式について，充足可能条件を導くことで，HTの動作条件を特定する．次に，(ii)については，挿入されるHTが，特定の入力候補でのみ動作することに注目し，それをうまく活用することでHTにあたる論理ゲートを絞り込む手法を提案した．提案手法では，まず回路上のすべての論理ゲートについて，その機能をガロア体方程式として導出する．次に，ガロア体方程式の次数が，活性化確率の負の対数に比例するという特徴を利用して，HTに対応する論理ゲートを絞り込む．提案手法では，論理ゲートの充足条件の数を直接求めるのではなく，ガロア体方程式の次数に着目することで，高速にHTを絞り込むことが可能である．上記の(i)と(ii)の有効性を確認するために，楕円曲線暗号向けのガロア体乗算器と，AESについてHT検知実験を行った．前者については，従来手法や形式検証ツールであるSynopsys Formalityよりも短い時間で，HTが検知可能なことを示した．また，AESについても，約３秒でHTの動作条件および挿入箇所特定が可能なことを示した．