HOME > 研究者 > 本間尚文先生 > 高安全・高信頼な情報通信のためのトロイフリーLSIシステム設計・検証技術の開発(第1回)

数学的アプローチでHT検出技術の開発を行っている研究者は、先生の他にいるのでしょうか。

研究している人はいるかもしれませんが、手法の確立に成功したのは、おそらく私のグループが初めてだと思います。

とくに、回路機能や回路仕様を表す代数方程式をZDD形式に変換した際、その記述には一意性があることが重要であり、これをグレブナー基底というのですが、変換後の記述がグレブナー基底ではない場合、ブッフベルガーのアルゴリズムを用いて再度変換する必要があります。つまり、①回路機能の方程式をZDD形式記述で表現→②グレブナー基底であることを確認→違う場合はブッフベルガーのアルゴリズムを用いて再度変換→③得られたZDD表現の等価性を検証、というのが従来の手順です。

しかし、ブッフベルガーのアルゴリズムを用いた変換は、大きな回路ほど計算量が膨れ上がり、かなりの時間を要します。それが最大の課題でした。
 ですが、ここで大きなブレークスルーがありました。それはZDD形式記述に変換する際、ある変数順序に従って変換すれば、得られた方程式は必ずグレブナー基底になり、しかも高速変換が可能というものです。この成果は、そうしたブレークスルーが評価され、この分野のトップジャーナルに掲載されました。

ZDDに基づく形式記述に変換することで関数がコンパクトになることと、ある特殊な順序での変換がグレブナー基底に結びつくことは、それぞれ別の分野からヒントを得て構築した

確実かつ高速にグレブナー基底に変換できる画期的な方法を見つけたことで、この手法が確立したということですね。ところで、LSI設計を専門とされていたのに、なぜハードウェアセキュリティの研究を始めることになったのですか。

私が主に研究対象としていたのが、数学的な計算をする回路だったからです。博士課程修了後、この研究をどのように生かすべきかを考える中で、暗号処理のハードウェアが複雑な計算回路から構成されていることを知り、その設計や検証技術に興味を持ちました。

ただ、それまで暗号に関わる専門的な数学に触れる機会がなかったため、いちから勉強することになりました。教材を探すところから始めたのですが、当時は暗号のために数学を「使いこなす」ための教科書がほとんどなく、苦労しました。それから今日まで15年ほど、新しい暗号やセキュリティ技術が生まれるたびに必要な数学の勉強を重ねています。大変ではありますが、これまでの積み重ねが現在の研究に繋がっているという実感があるため、今後も継続していくつもりです。

量子コンピュータにも耐性を持つ暗号など次々と新たな暗号技術が登場しており、数学的な多様性も増しているが、ハードウェアセキュリティの研究には必要な知識であり、研究室の学生とともに勉強を続けている

LSIの回路仕様とHDLコードを数式化し、その等価性を数学的に検証する。専門性の高い話をわかりやすくお教えいただき、ありがとうございました。新しい手法で検証時間が飛躍的に短縮し、これまで不可能とされていた検証が可能になる等、すばらしい成果に心が踊ります。次回はバックエンド設計時と、LSI製造後のHT検出技術開発について、お伺いいたします。

Copyright(C) SECOM Science and Technology Foundation