| Project/Area Number |
21H04867
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Medium-sized Section 60:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
本間 尚文 東北大学, 電気通信研究所, 教授 (00343062)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
上野 嶺 京都大学, 情報学研究科, 准教授 (80826165)
|
|---|
| Project Period (FY) |
2021-04-05 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥41,080,000 (Direct Cost: ¥31,600,000、Indirect Cost: ¥9,480,000)
Fiscal Year 2024: ¥8,580,000 (Direct Cost: ¥6,600,000、Indirect Cost: ¥1,980,000)
Fiscal Year 2023: ¥8,190,000 (Direct Cost: ¥6,300,000、Indirect Cost: ¥1,890,000)
Fiscal Year 2022: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
Fiscal Year 2021: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
|
|---|
| Keywords | 計算機システム / 情報セキュリティ / ハードウェアセキュリティ |
|---|
| Outline of Research at the Start |
本研究は，暗号や誤り訂正等の機能を搭載するセキュリティハードウェアの形式的設計・検証技術の確立を目指す．まず，非冗長・冗長ガロア体算術が混在する多様なガロア体算術演算回路の統一的な形式的設計手法を開発し，その回路表現を完全かつ高速に検証する計算機代数に基づく形式的検証手法を開発する．その上で，次世代暗号や物理複製困難関数等を実行する先端的なセキュリティハードウェアを対象として，その有効性を実証する．
|
| Outline of Annual Research Achievements |
前年度までに開発したHDL記述の等価性判定を可能とする形式的検証手法を開発するとともに，暗号ハードウェアに適用し，その有効性評価を実施した．開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式もしくは多項式の集合と見なして，その正規形であるグレブナー基底を導出する．ここで，特殊な変数順序（逆トポロジー項順序）をとることにより得られる多項式が自ずとグレブナー基底になることが開発手法の特長となる．本年度は，その特長を数学的に証明した．これにより，同手法を様々な回路に適用する方向性が定まった．さらに多項式をZDD（Zero-suppressed Decision Diagram）に変換することで高次の多項式であってもコンパクトに表現できる効果を実用的な暗号ハードウェアへの適用を通して確認した． その結果，ガロア体演算機能の場合，指数的に表現サイズを削減できることを示した．また，結果として得られるZDD集合はグレブナー基底と等価なことが数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できることも応用を通して確認できた．特に，本年度は，これまで規模の面で困難だった先端的なセキュリティハードウェアの例として，現在世界で最も利用されている暗号AESへの適用を行った．AESは，その暗号化・復号処理全体がガロア体上の演算として記述されるため，開発した手法を用いて組み合わせ回路部分のデータパス全体の設計・検証を実施した．さらに，本年度は，消費電力面で優れたハードウェアアーキテクチャへの適用も検討し，その可能性を実験的に示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初予定していた成果が得られており，今後の計画に対する道筋も見えている．具体的には，
前年度までに開発したHDL記述の等価性判定を可能とする形式的検証手法を開発するとともに，暗号ハードウェアに適用し，その有効性評価を実施した．開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式もしくは多項式の集合と見なして，その正規形であるグレブナー基底を導出する．ここで，特殊な変数順序（逆トポロジー項順序）をとることにより得られる多項式が自ずとグレブナー基底になることが開発手法の特長となる．本年度は，その特長を数学的にも証明した．さらに多項式をZDD（Zero-suppressed Decision Diagram）に変換することで高次の多項式であってもコンパクトに表現できることを暗号ハードウェアへの適用を通して確認した． また，結果として得られるZDD集合はグレブナー基底と等価なことが数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できることも応用を通して確認できた．特に，本年度は，これまで規模の面で困難だった先端的なセキュリティハードウェアの例として，現在世界で最も利用されている暗号AESへの適用を行った．AESは，その暗号化・復号処理全体がガロア体上の演算として記述されるため，開発した手法を用いて組み合わせ回路部分のデータパス全体の設計・検証を実施した．さらに，本年度は，消費電力面で優れたハードウェアアーキテクチャへの適用も検討し，その可能性を実験的に示した．研究を進めるにつれて新たな課題・関連する課題も出現しているが，新たな課題に対しては定式化・実験方法等の変更で対応可能であり，当初研究計画を変更するほどではない．以上から，「おおむね順調に進展している」と自己評価した．
|
| Strategy for Future Research Activity |
上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，これまでに開発した形式的検証手法をさらに高度な暗号ハードウェアに適用し，その有効性評価を実施する．特に，消費電力面で優れたハードウェアアーキテクチャへの適用に加えて，物理攻撃耐性を有するセキュアアーキテクチャを対象に開発手法の有効性を実証する．物理攻撃耐性を有するハードウェアへの適用では，実際に物理攻撃耐性評価実験も並行して実施し，その実用性を明らかにする．さらに，回路にバグやハードウェアトロイがある場合を想定し，それを同定する手法へと開発手法を発展させる．ここでは，等価性検証の結果として得られるZDDの残差からその作動条件および存在箇所を同定する手法を開発する．
|
