2022 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 |
本年度は，ガロア体上の算術演算（ガロア体算術演算）のZDD（Zero-suppressed Decision Diagram）表現を用いた形式的検証手法の開発を推進した．特に，前年度から開発を推進してきた冗長表現と非冗長表現が混在するガロア体算術演算回路の形式的表現手法に対応する（機能検証の対象となる）HDL記述の等価性を判定する検証手法に関する理論を構築した．ここでは，提案する形式的表現による回路仕様と任意のHDL記述の等価性判定問題をいかに代数的問題（多項式イデアル所属問題）に帰着させるかが重要となる．そこで，開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式集合と見なして，その正規形であるグレブナー基底を導出した．ここで，特に，特殊な変数順序（逆トポロジー項順序）で多項式をZDDに変換することを見出した．この変数順序で変換されたZDD集合はグレブナー基底と等価なことを数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できるという特長を有する．その上で，その動作検証を目的として，簡易なガロア体演算回路（32ビットガロア体乗算器等）の仕様と回路記述から得られたZDD集合間の等価性判定を実行した．その結果から，考案手法により高速かつ完全な検証が可能となる見通しを得た．さらに，考案した形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発した．以上，当初計画していた形式的検証手法の見通しが得られた．
|
| 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集合はグレブナー基底と等価となるため，別途グレブナー基底を導出する膨大な計算を省略できた．さらに，簡易な演算回路の仕様と回路記述から得られたZDD集合間の等価性判定を実行し，その有効性を例証した．以上の形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発した．研究を進めるにつれて新たな課題・関連する課題も出現しているが，新たな課題に対しては定式化・実験方法等の変更で対応可能であり，関連する課題に対しては並行して研究開発を行う体制が整っているため，当初研究計画を変更するほどではない．以上から，「おおむね順調に進展している」と自己評価した．
|
| Strategy for Future Research Activity |
上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，前年度開発した，HDL記述の等価性判定を可能とする形式的検証手法を暗号ハードウェアに適用し，その有効性評価に着手する．開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式集合と見なして，その正規形であるグレブナー基底を導出する．その際，特殊な変数順序（逆トポロジー項順序）で多項式をZDD（Zero-suppressed Decision Diagram）に変換することで得られるZDD集合はグレブナー基底と等価なことが数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できる．その上で，仕様と回路記述から得られたZDD集合間の等価性判定を実行する．本年度は，これまで困難だった先端的なセキュリティハードウェアの例として，現在世界で最も利用されている暗号AESを対象とする．AESは，その暗号化・復号処理全体がガロア体上の演算として記述されるため，開発した手法によるデータパス全体の設計・検証が可能と予想される．本年度は特に，消費電力面で優れたハードウェアアーキテクチャへの適用を行う．
|
