2020 Fiscal Year Annual Research Report
トロイフリー暗号ハードウェアの高水準設計・検証手法の開拓
| Project/Area Number |
20J12887
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
伊東 燦 東北大学, 工学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2020-04-24 – 2022-03-31
|
| Keywords | ハードウェアトロイ / 形式検証 / 暗号ハードウェア / ハードウェアセキュリティ / 計算機代数 |
|---|
| Outline of Annual Research Achievements |
本年度はハードウェアトロイ（HT）の検知に向けて，暗号ハードウェアの形式的検証手法の研究を行った．具体的には，(i)ゼロサプレス型二分決定グラフ（ZDD）を用いた効率的な等価性検証の確立と，(ii)多標数ガロア体算術演算回路の検証手法の開発の２つである．以下ではそれぞれについて説明する．
まず(i)では，仕様となるゴールデンモデル（回路機能を表現する方程式）とHTの挿入された検証対象のネットリストの間の等価性を行う技術の開発を行った．もしHTが挿入されていれば，ゴールデンモデルと検証対象のネットリストが等価ではないと判定されることになることから，HTの検知を行うことができる．一般に従来の暗号ハードウェアに対する等価性検証では，計算機代数に基づく等価性検証手法が用いられる．しかし，同手法では，ネットリストにHTが挿入されている場合に，検証過程で出現する多項式の項数が爆発し検証が困難になることが知られていた．そこで，本研究では因数分解を利用することで多項式のコンパクトな表現を与えるZDDを利用し，HTが挿入された場合でも現実的な時間で検証が終了する手法を開発した．本提案手法を用いることで，国際標準暗号であるAESや楕円曲線暗号（ECC）ハードウェアに対して，完全なHTの検知が可能である．
次に(ii)では，次世代の高機能暗号として知られるペアリング暗号で計算の効率化のためにしばしば用いられる，標数が3以上（多標数）のガロア体の演算の検証を効率的に行うための手法を提案した．具体的には，通常の標数2のガロア体算術演算回路に対する等価性検証で有効であるZDDを，多標数のガロア体も表現できるように拡張したGalois-field binary moment diagram (GFBMD)の提案を行った．GFBMDを用いることで，標数2のガロア体算術演算回路と同様に高速に検証が可能である．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究課題では，（１）計算機代数に基づく暗号回路の形式的ハードウェアトロイ（HT）検知手法の確立，（２）HTのトリガー条件および挿入箇所特定のための代数的検証手法の理論的拡張，（３）提案手法を一般に利用しやすい形（ライブラリ等）による配布の３つを予定していた．このうち，本年度の研究では主に（１）を達成することを目標としていた．
これについては，国際標準暗号AESやECCの完全検証が本年度で可能となったことから，当初の予定通りに研究が進んでおり，概ね順調に進展している．
|
| Strategy for Future Research Activity |
今後は，ハードウェアトロイ（HT）が挿入された暗号ハードウェアに対する，（１）HTのトリガー条件および挿入箇所特定手法の確立と，（２）提案HT検出フレームワークのライブラリ等による一般公開の２つを予定している．
まず（１）に関しては，検証対象として与えられたネットリストと，そのゴールデンモデル（設計仕様）となるネットリストが与えられた際に，HTの動作（トリガー）条件の特定を行う．具体的には，まず検証対象のネットリストと，ゴールデンモデルのそれぞれについて，出力の機能を表現する方程式をゼロサプレス型二分決定グラフ（ZDD）の形で得る．このZDDの高速な導出法は，すでに前年度までの研究で提案している．次に，ネットリストとゴールデンモデルのそれぞれに対して得られたZDDの間の残差を求め，その充足条件を列挙することでトリガー条件の特定を行う．次に，HTの挿入箇所特定手法については，HTが非常にまれな入力でのみ故障を引き起こすという特徴を逆手に取ることで，HTにあたる論理ゲートを列挙する手法を提案する．具体的には，与えられたネットリストの各ゲートに対して，プライマリ入力（レジスタの出力）の変数を用いた機能表明（代数方程式）を得る．この代数方程式の次数は，ゲートの充足条件が少なければ少ないほど大きくなるので，この情報を用いることでHTにあたる論理ゲートを絞り込むことができると考えている．
（２）については，本研究ですでに提案したHT検知のための等価性検証手法と，本年度で研究を行うHTのトリガー条件及び挿入箇所特定手法を一般に使いやすい，ライブラリの形で公開することを予定している．具体的には，代表的なオープンソースの論理合成ツールであるYosysへ搭載可能なプラグインの形で公開することで，既存の設計開発の流れに容易に組み込めるようにすることなどを予定している．
|
Research Products
(5 results)
