| 研究課題/領域番号 |
17H00729
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
本間 尚文 東北大学, 電気通信研究所, 教授 (00343062)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 計算機システム |
|---|
| 研究実績の概要 |
まず，これまでに開発した非冗長・冗長表現が混載したガロア体算術演算回路の形式的表現が表す回路機能の形式的検証システムを開発した．開発したシステムでは，まず，検証対象となる機能との等価性判定に用いる内部回路記述を多項式集合と見なしてグレブナー基底に変換する．ここで，冗長表現を非冗長表現と同様に扱うため，線形再帰関係LRRと呼ばれる関係式を多項式集合に追加して変換を行う．変換には任意の多項式集合をグレブナー基底へと変換するブッフバーガーアルゴリズムの高速演算ライブラリを用いた．次に，得られたグレブナー基底を用いて多項式簡約を実行することにより，検証対象の機能が多項式集合により導出できるかどうかを判定する．ここでもLRRを導出時に用いた．
また，これまでに規定した冗長表現を含めて定式化したガロア体表現による高次なガロア体算術演算回路の形式的検証手法を開発した．これまでの手法でも128ビット程度までの次数であれば検証可能であったが，実用的な暗号や誤り訂正プロセッサの機能表現では高次の算術演算（べき乗算や逆元演算など）がしばしば出現し，グレブナー基底の算出を困難としていた．そこで，これまでの計算機代数に基づく形式的検証に自然演繹に基づく形式的検証を組み合わせる新たな検証手法を開発し，高次算術演算の検証を可能とした．同手法の開発にあたっては，高次の算術演算の機能表明が一般に高階層の記述に出現し，入力を単純に内部構造に代入した形で与えられることを利用した．開発手法の評価は，語長が256ビットを越える実用的な乗算回路および誤り訂正符号の復号回路を網羅的に検証することで実施した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初予定していた成果が得られている．具体的には，当初想定した通りに冗長表現を非冗長表現と同様に扱うため線形再帰関係LRRと呼ばれる関係式を多項式集合に追加して変換を行う処理がわずかな計算量の増加で実現できたため，非冗長・冗長表現が混載したガロア体算術演算回路の形式的検証システムの開発を予定通りに進めることができた．また，適宜オープンソースの数値計算ライブラリを組み込むことにより，大きな障害がなくプロトタイプソフトウェアを開発することができた．これにより，最終年度となる次年度に，これまでに開発した形式的設計・検証手法の応用として，ガロア体算術演算ジェネレータを開発する準備が整っている．年度末に新型コロナウイルス感染症拡大により同開発準備に若干の遅れが生じているが，現状では当初研究計画を変更することなく推進できると見込んでいる．
|
| 今後の研究の推進方策 |
上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，R1年度までに開発した非冗長・冗長表現が混載したガロア体算術演算回路の形式的設計・検証手法の応用として，ガロア体算術演算回路ジェネレータを開発する．同ジェネレータは，設計仕様（アーキテクチャ，基数，および算術アルゴリズム）に応じてガロア体算術演算回路のHDL記述を自動生成するシステムである．まず，入力された仕様に応じてXGF-ACGを生成する．次に，これまでに開発したグレブナー基底に基づく検証および自然演繹に基づく検証を併用する検証システムを用いてXGF-ACGコードから回路機能を検証する．その後，検証されたXGF-ACGをHDLの形式に変換して出力する．生成対象は，代表的なガロア体算術演算であるMastrovito乗算とMassey-Omura乗算とする．設計仕様にはアーキテクチャ，基数（2～256の範囲）および使用するガロア体表現を与える．開発方法としては，まず既存のジェネレータを拡張してXGF-ACGの生成システムとXGF-ACGからHDLへの変換システムを開発し，それらをこれまでに開発した検証システムに接続する．最終的には前年までに開発した暗号プロセッサデータパスの自動生成も試みる予定である．また，開発したジェネレータは，Web上で公開する計画である．
|
