トロイフリー暗号ハードウェアの高水準設計・検証手法の開拓
| Project/Area Number |
20J12887
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60040:Computer system-related
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
伊東 燦 東北大学, 工学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2020-04-24 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2021: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2020: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | ハードウェアセキュリティ / 暗号 / ハードウェアトロイ / 形式検証 / 暗号ハードウェア / 計算機代数 |
|---|
| Outline of Research at the Start |
近年，LSIチップに秘密裏に挿入されるバックドアの一種であるハードウェアトロイ(HT)挿入の危険性が指摘されてきている．本研究では，HTが挿入された場合に特にセキュリティ上問題となり得る暗号ハードウェアに焦点を当て，その形式的検証手法の確立を目指す．提案手法では，HTが挿入されていないことを数学的に証明することで検証を行うことから，従来困難と考えられてきたHTの根絶を図ることができる．
|
| Outline of Annual Research Achievements |
本年度では，(i)ハードウェアトロイ（HT）のトリガー条件の特定手法，(ii)挿入箇所特定手法の２つの確立を目指して研究を行った．
まず(i)については，HTが挿入された組み合わせ回路と，設計仕様であるガロア体方程式との間で，出力差分を取ることでHTの作動条件を特定する手法を開発した．具体的には，まず，検証対象となる回路の各プライマリ出力について，その論理機能をプライマリ入力変数で書き下した方程式を導出する．この導出過程における多項式表現に，ゼロサプレス型二分決定グラフ（ZDD)を用いることで，高速な多項式導出を可能とする．次に，回路機能を表す多項式と，設計仕様となるガロア体方程式の間で差分を取ることで，HTの機能を表現した方程式を導出する．最後に，この差分の方程式について，充足可能条件を導くことで，HTの動作条件を特定する．
次に，(ii)については，挿入されるHTが，特定の入力候補でのみ動作することに注目し，それをうまく活用することでHTにあたる論理ゲートを絞り込む手法を提案した．提案手法では，まず回路上のすべての論理ゲートについて，その機能をガロア体方程式として導出する．次に，ガロア体方程式の次数が，活性化確率の負の対数に比例するという特徴を利用して，HTに対応する論理ゲートを絞り込む．提案手法では，論理ゲートの充足条件の数を直接求めるのではなく，ガロア体方程式の次数に着目することで，高速にHTを絞り込むことが可能である．
上記の(i)と(ii)の有効性を確認するために，楕円曲線暗号向けのガロア体乗算器と，AESについてHT検知実験を行った．前者については，従来手法や形式検証ツールであるSynopsys Formalityよりも短い時間で，HTが検知可能なことを示した．また，AESについても，約３秒でHTの動作条件および挿入箇所特定が可能なことを示した．
|
| Research Progress Status |
令和3年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和3年度が最終年度であるため、記入しない。
|
Report
(2 results)
Research Products
(8 results)
