An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics

Summary

• Garois Field の算術回路の形式検証を提案
  • 検証: 回路が等価か
• ネットリストを連立代数方程式で表現し、特性pが2より大きい拡張体$mathbb{F}_{p^m}$上の演算に効率的に適用できる新しい多項式縮約手法に基づいてこれを解く
• 本手法は、逆トポロジカル項順序を用いてGröbner基底を導出することにより、対象回路にバグが含まれていても、検証を完了することができる
• また、Galois-Field二項モーメント図の拡張を導入し、多項式削減を高速に実行する。実験により、提案手法は現代暗号を含む実用的な$mathbb{F}_{p^m}$算術回路を効率的に検証できることを示す
• 拡張された多項式削減技術により、元の手法に比べて最大で約5倍の速度で検証が可能であることを実証した。