2021 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 |
令和3年度は，冗長表現と非冗長なガロア体表現が混在する算術演算回路を対象として，その拡大体および合成体上の算術演算回路の形式的表現手法を開発した．ここでは，これまでに本研究者が開発したガロア体算術演算回路を形式的に表すグラフ表現「拡張ガロア体算術回路グラフ」の理論を応用した．ガロア体は，整数環との代数的な類似性に着目すると，整数における各桁の“重み”がガロア体では“基底”に，各桁の“取り得る値”がガロア体では“多項式係数の取り得る値”に対応する．これに加えて，整数では暗黙的に演算（加算および乗算）の規則が定義されていたが，ガロア体では既約多項式として演算規則を明示的に定義する．結果として，基底集合，多項式係数の取り得る値の集合，既約多項式によってガロア体は形式的に定義される．本研究では，これを冗長表現と非冗長表現の混在するガロア体算術演算回路にも適用するため，基底集合の表現手法を拡張した．具体的には，既約多項式部分を多項式の積の形で表現した．その基本構造には，これまでの拡張ガロア体算術回路グラフと同様，機能の“算術化(Arithmetization)”と“階層化(Hierarchization)”を用いた．開発した表現手法の評価は，非冗長表現と冗長表現の混在する多様なガロア体演算回路により行った．当該形式的表現から変換したハードウェア記述言語(HDL: Hardware Description Language)記述の論理シミュレーションを通して，表現された機能の完全性を評価した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初予定していた成果が得られており，今後の計画に対する道筋も見えている．具体的には，冗長表現と非冗長表現が混在するガロア体算術演算回路の形式的表現を実現するため，基底集合部分に任意の冗長性を許す剰余多項式環の基底表現を導入するとともに，既約多項式部分を多項式の積の形で表現した．これにより，数表現が混在するガロア体算術演算回路を統一的に表現・定式化できた．研究を進めるにつれて新たな課題・関連する課題も出現しているが，新たな課題に対しては定式化・実験方法等の変更で対応可能であり，関連する課題に対しては並行して研究開発を行う体制が整っているため，当初研究計画を変更するほどではない．以上から，「おおむね順調に進展している」と自己評価した．
|
| Strategy for Future Research Activity |
上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，前年度開発した形式的表現手法と対応する（機能検証の対象となる）HDL記述の等価性を判定する検証手法の理論を構築する．ここでは，形式的表現による回路仕様と任意のHDL記述の等価性判定問題をいかに代数的問題（多項式イデアル所属問題）に帰着させるかが重要となる．開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式集合と見なして，その正規形であるグレブナー基底を導出する．ここで，特殊な変数順序（逆トポロジー項順序）で多項式をZDD（Zero-suppressed Decision Diagram）に変換することを考える．この変数順序で変換されたZDD集合はグレブナー基底と等価なことが数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できる．次に，仕様と回路記述から得られたZDD集合間の等価性判定を実行する．本研究では，以上の形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発する．
|
