2017 Fiscal Year Annual Research Report
冗長ガロア体算術に基づくセキュリティハードウェアの高水準設計技術の研究開発
| Project/Area Number |
17H00729
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
本間 尚文 東北大学, 電気通信研究所, 教授 (00343062)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 計算機システム |
|---|
| Outline of Annual Research Achievements |
平成29年度は，多項式環表現および冗長表現基底と呼ばれる冗長なガロア体表現を対象として，その拡大体および合成体上の算術演算回路の形式的表現手法を開発した．
具体的には，これまでに開発したガロア体算術演算回路を形式的に表すグラフ表現「ガロア体算術回路グラフ(GF-ACG」の理論を拡張した．ガロア体は，整数環との代数的な類似性に着目すると，整数における各桁の“重み”がガロア体では“基底”に，各桁の“取り得る値”がガロア体では“多項式係数の取り得る値”に対応する．これに加えて，整数では暗黙的に演算（加算や乗算）の規則が定義されていたが，ガロア体では既約多項式として演算規則を明示的に定義する．結果として，基底集合，多項式係数の取り得る値の集合，既約多項式によってガロア体は形式的に定義される．本研究では，これを冗長表現にも拡張するため，基底集合部分に任意の冗長性を許す剰余多項式環の基底表現を導入するとともに，既約多項式部分を多項式の積の形で表現した．また，その変数を用いて拡張算術回路グラフ(Extended GF-ACG: XGF-ACG)を定式化した．その基本構造としては，これまでに開発したGF-ACGと同様に，機能の“算術化(Arithmetization)”と“階層化 (Hierarchization)”を用いた．
開発したXGF-ACGを用いて多項式環表現されたガロア体上の並列乗算器を網羅的に設計し，当該XGF-ACGから変換したハードウェア記述言語 (HDL) 記述の論理シミュレーションを通して，表現された機能の完全性を評価した．なお，XGF-ACGから従来のHDL記述への変換では，誤り等が発生しないよう一対一に変換する方式を考案した．
以上の形式的設計手法に加えて，本研究では，その関連・応用技術についても合わせて検討した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初予定していた成果が得られており，今後の計画に対する道筋も見えている．具体的には，冗長表現を含めたガロア体算術演算回路の形式的表現を実現するため，基底集合部分に任意の冗長性を許す剰余多項式環の基底表現を導入するとともに，既約多項式部分を多項式の積の形で表現することができた．また，その変数を用いて拡張算術回路グラフ(Extended GF-ACG: XGF-ACG)を定式化することができた．研究を進めるにつれて新たな課題・関連する課題も出現しているが，新たな課題に対しては定式化・実験方法等の変更で対応可能であり，関連する課題に対しては並行して研究開発を行う体制が整っているため，当初研究計画を変更するほどではない．
|
| Strategy for Future Research Activity |
上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，H30年度は，H29年度に定式化したXGF-ACGが表す回路機能の形式的検証手法の理論を構築するとともに，その検証システムを開発する．開発の鍵となるのは，検証対象となるXGF-ACGの回路機能の正当性を判定する問題をいかに多項式イデアル所属問題に帰着させるかである．開発手法では，まず，検証対象となる機能との等価性判定に用いる内部回路記述を多項式集合と見なしてグレブナー基底に変換する．ここで，冗長表現を非冗長表現と同様に扱うため，線形再帰関係LRRと呼ばれる関係式を多項式集合に追加して効率的に変換を行う予定である．この着想は，冗長表現と擬巡回符号との等価性から得ている．変換には任意の多項式集合をグレブナー基底へと変換するブッフバーガーアルゴリズムを用いる．次に，得られたグレブナー基底を用いて多項式簡約を実行することにより，検証対象の機能が多項式集合により導出できるかどうかを判定する．ここでもLRRを導出時に用いる．本研究では，以上の形式的検証手法を定式化するとともに，同検証システムのプロトタイプソフトウェアを開発する．開発では必要に応じて各種数値計算ライブラリを利用する．また，関連する研究課題に対しても引き続き並行して実施する予定である．
|
