通常、回路機能をHDLコードへと変換した後は、正しく変換されたか否かの検証を実施します。ただし、それは一定回数の入力を行い、仕様通りの出力がされていることを確認するものです。仮に１0億通りの入力パターンがあった場合、すべて入力して確認することは現実的ではありません。ですが、HTが挿入されている場合、それは極めて稀なパターンを入力した時のみ動き出すように設計される可能性が高いため、従来の検証方法では安全性を十分に担保することができません。

そこで私は回路の構造を数式化し、フロントエンド設計時にHTが挿入されていないことを数学的に保証する手法を開発しました。

学生時代にLSIを自動生成する研究を行うなかで、生成された回路の機能を効率的に確認するため、プログラムの入力をxやyなどの記号に置き換えて表現する記号実行（Symbolic Execution）を取り入れた検証技術を構築する必要があり、これに長年取り組んでいました。その技術をHT検知に応用しました。

たとえば「1を入力したら3」、「2を入力したら5」、「3を入力したら7」が出力される場合、それは「2x＋1」という数式で表記できます。回路機能を表現するHDLは連立代数方程式、回路仕様もある代数方程式として記述可能です。

回路を表す連立方程式を解いて入力と出力変数のみの方程式を導き出し、仕様の方程式と等価であることが確認できれば、「全入力パターン検証済み」と同じ保証を得ることができるのです。

ただし、普通に導いていくと方程式は何百万項からなる膨大な式になってしまうため、ZDD（Zero-suppressed Binary Decision Diagram）という、二分木に基づく特殊な形式記述を使います。この形式であれば方程式を極めて小さく表現でき、変数が増えても式がそれほど大きくなりません。

仕様と回路記述を表す多項式をZDDに変換した上で、等価性を検証する

はい。この形式記述であれば従来の最先端の結果よりも200倍高速に検証できるため、これまで困難だった実用的な暗号回路の検証も可能になります。

しかもHTが挿入されていた場合、従来方法はいつまでも計算結果が出ないことから「HTが挿入されている可能性が高い」という消極的な判断をしていました。一方この手法では、バグやHTが存在すれば、ただちに計算を終了して「誤りや不要な機能がある」と明確な答えを返します。変数の改ざんや余分な機能の追加など、機能改変を伴うものであれば、原理的にすべて検出可能です。

ZDDによる形式的検出法により、世界最高効率の回路検証を達成