2023 Fiscal Year Annual Research Report
セキュリティハードウェアの形式的設計・検証理論の深化と展開
| Project/Area Number |
21H04867
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
本間 尚文 東北大学, 電気通信研究所, 教授 (00343062)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
上野 嶺 東北大学, 電気通信研究所, 助教 (80826165)
|
|---|
| Project Period (FY) |
2021-04-05 – 2026-03-31
|
| Keywords | 計算機システム / 情報セキュリティ |
|---|
| 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の残差からその作動条件および存在箇所を同定する手法を開発する．
|
