| 研究課題/領域番号 |
20J12887
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60040:計算機システム関連
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
伊東 燦 東北大学, 工学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2020-04-24 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
1,700千円 (直接経費: 1,700千円)
2021年度: 800千円 (直接経費: 800千円)
2020年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | ハードウェアセキュリティ / 暗号 / ハードウェアトロイ / 形式検証 / 暗号ハードウェア / 計算機代数 |
|---|
| 研究開始時の研究の概要 |
近年，LSIチップに秘密裏に挿入されるバックドアの一種であるハードウェアトロイ(HT)挿入の危険性が指摘されてきている．本研究では，HTが挿入された場合に特にセキュリティ上問題となり得る暗号ハードウェアに焦点を当て，その形式的検証手法の確立を目指す．提案手法では，HTが挿入されていないことを数学的に証明することで検証を行うことから，従来困難と考えられてきたHTの根絶を図ることができる．
|
| 研究実績の概要 |
本年度では，(i)ハードウェアトロイ（HT）のトリガー条件の特定手法，(ii)挿入箇所特定手法の２つの確立を目指して研究を行った．
まず(i)については，HTが挿入された組み合わせ回路と，設計仕様であるガロア体方程式との間で，出力差分を取ることでHTの作動条件を特定する手法を開発した．具体的には，まず，検証対象となる回路の各プライマリ出力について，その論理機能をプライマリ入力変数で書き下した方程式を導出する．この導出過程における多項式表現に，ゼロサプレス型二分決定グラフ（ZDD)を用いることで，高速な多項式導出を可能とする．次に，回路機能を表す多項式と，設計仕様となるガロア体方程式の間で差分を取ることで，HTの機能を表現した方程式を導出する．最後に，この差分の方程式について，充足可能条件を導くことで，HTの動作条件を特定する．
次に，(ii)については，挿入されるHTが，特定の入力候補でのみ動作することに注目し，それをうまく活用することでHTにあたる論理ゲートを絞り込む手法を提案した．提案手法では，まず回路上のすべての論理ゲートについて，その機能をガロア体方程式として導出する．次に，ガロア体方程式の次数が，活性化確率の負の対数に比例するという特徴を利用して，HTに対応する論理ゲートを絞り込む．提案手法では，論理ゲートの充足条件の数を直接求めるのではなく，ガロア体方程式の次数に着目することで，高速にHTを絞り込むことが可能である．
上記の(i)と(ii)の有効性を確認するために，楕円曲線暗号向けのガロア体乗算器と，AESについてHT検知実験を行った．前者については，従来手法や形式検証ツールであるSynopsys Formalityよりも短い時間で，HTが検知可能なことを示した．また，AESについても，約３秒でHTの動作条件および挿入箇所特定が可能なことを示した．
|
| 現在までの達成度 (段落) |
令和3年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
令和3年度が最終年度であるため、記入しない。
|
