研究課題
H30年度は，前年度に開発した非冗長・冗長表現が混載したガロア体算術演算回路の形式的表現が表す回路機能の形式的検証システムを開発した．開発したシステムでは，まず，検証対象となる機能との等価性判定に用いる内部回路記述を多項式集合と見なしてグレブナー基底に変換する．ここで，冗長表現を非冗長表現と同様に扱うため，線形再帰関係LRRと呼ばれる関係式を多項式集合に追加して変換を行う．次に，得られたグレブナー基底を用いて多項式簡約を実行することにより，検証対象の機能が多項式集合により導出できるかどうかを判定する．ここでもLRRを導出時に用いる．本年度は，以上の形式的検証システムのプロトタイプソフトウェアを開発した．開発ではオープンに利用可能な各種数値計算ライブラリを用いた．さらに，前年度に規定した冗長表現を含めて定式化したガロア体表現による高次なガロア体算術演算回路の形式的検証手法を開発した．特に，高次の算術演算を検証するため，これまでの計算機代数に基づく形式的検証に自然演繹に基づく形式的検証を組み合わせる新たな検証手法を開発した．同検証手法は，高次の算術演算の機能表明が一般に高階層の記述に出現し，入力を単純に内部構造に代入した形で与えられることに着目している．代入操作により得られる機能検証は，等号付き一階述語論理の自然演繹に基づく検証により容易に検証できる．この拡張により，暗号プロセッサ設計に開発手法を応用する際に，高速および低消費電力暗号プロセッサに加えて，暗号実装の脅威となっている各種物理攻撃への対策を施した（対策により高次となった）プロセッサの検証も可能となった．
2: おおむね順調に進展している
当初予定していた成果が得られており，今後の計画に対する道筋も見えている．具体的には，線形再帰関係LRRと呼ばれる関係式を多項式集合に追加して変換を行うことにより，冗長表現を含めたガロア体算術演算回路の形式的検証手法を開発することができた．また，自然演繹に基づく形式的検証をこれまでの計算機代数に基づく手法と組み合わせることにより，より高次なガロア体算術演算回路の形式的検証が可能となった．以上のとおり，これまでの研究開発により，冗長表現を含めた高次のガロア体算術演算回路の形式的設計・検証の目処を立てることできたため，次年度以降これを応用したシステム開発を当初計画通り推進する予定である．
上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，R元年度は，開発した非冗長・冗長表現が混載したガロア体算術演算回路の形式的検証手法の応用として，暗号プロセッサデータパスの形式的設計・検証を実現する．応用例としては，まず，現在世界で最も利用されているブロック暗号AES (Advanced Encryption Standard)を対象とする．AESはISO/IEC国際標準の暗号方式であり，その暗号化処理全体がガロア体上の演算として記述されるため，XGF-ACGによるデータパス全体の設計・検証が可能と予想される．ここでは，高速性や低消費電力性に優れたデータパス，物理攻撃への耐性を有するデータパスを有するAESハードウェアをXGF-ACGを用いて形式的に設計し，主要な構成要素の検証時間を評価することで，開発手法の有効性を実証する．また，現在，CAESARプロジェクトと呼ばれる国際コンペティションにおいて，AESを基本とする認証暗号方式が国際的にいくつも提案されており，今後の活用が期待されていることから，AESを基本とする認証暗号方式への適用も合わせて検討する．具体的には，AES-OCB，AES-COLM，AES-OTRといった次世代方式を対象とする．その上で，上記で設計した暗号プロセッサのプロトタイプをASICで実装した場合の性能評価を実施するとともに，その物理攻撃に対する耐性を評価する．本実験では，本研究代表者らが開発してきた最新の物理攻撃評価ボードを用いて，物理攻撃の中でも特に強力とされるマイクロ磁界プローブによるサイドチャネル攻撃（局所電磁波解析攻撃）に対する耐性評価実験を実施する．
すべて 2019 2018 その他
すべて 雑誌論文 (5件) (うち査読あり 5件) 学会発表 (8件) (うち国際学会 4件、 招待講演 5件) 備考 (1件)
IEEE Transactions on Circuits and Systems I: Regular Papers
巻: 66 ページ: 616-629
10.1109/TCSI.2018.2869086
Journal of Applied Logics
巻: 5 ページ: 1815-1831
IEEE 48th International Symposium on Multiple-Valued Logic
巻: 1 ページ: 62-67
10.1109/ISMVL.2018.00019
巻: 1 ページ: 7-12
10.1109/ISMVL.2018.00010
International Workshop on Constructive Side-Channel Analysis and Secure Design 2018
巻: 1 ページ: 44-60
10.1007/978-3-319-89641-0_3
http://www.ecsis.riec.tohoku.ac.jp/
