Efficient Gröbner basis reductions for formal verification of galois field multipliers
Efficient Gröbner basis reductions for formal verification of galois field multipliers
复制标题
用于伽罗瓦域乘数形式化验证的高效 Gröbner 基约简
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Florian Enescu
中科院分区：
文献类型：
--
作者：
Jinpeng Lv;P. Kalla;Florian Enescu
伽罗华域运算在密码学、纠错码、信号处理等领域有着广泛的应用。乘法是伽罗华域运算的核心。利用基于计算机代数/代数几何的方法，研究了F(2k)型伽罗华域上(模)乘法器硬件实现的形式化验证问题。乘法器电路被建模为F(2k)[x1，x2，…，xd]中的多项式系统，并且验证问题被表示为对应(根)理想中的成员测试。这需要计算gröbner基，这可能是计算密集型的。为了克服这一局限性，我们分析了电路的拓扑结构，并推导出表示多项式的项阶。随后，利用伽罗华域上的Gröbner基理论，我们证明了这个项序使得多项式集合本身成为这一理想的Gröbner基--从而显著地改进了验证。使用我们的方法，我们可以验证F(2163)中高达163位电路的正确性，并检测其中的错误；而目前的方法是不可行的。
Galois field arithmetic finds application in many areas, such as cryptography, error correction codes, signal processing, etc. Multiplication lies at the core of most Galois field computations. This paper addresses the problem of formal verification of hardware implementations of (modulo) multipliers over Galois fields of the type F(2k), using a computer-algebra/algebraic-geometry based approach. The multiplier circuit is modeled as a polynomial system in F(2k)[x1, x2, ... , xd] and the verification problem is formulated as a membership test in a corresponding (radical) ideal. This requires the computation of a Gröbner basis, which can be computationally intensive. To overcome this limitation, we analyze the circuit topology and derive a term order to represent the polynomials. Subsequently, using the theory of Gröbner bases over Galois fields, we prove that this term order renders the set of polynomials itself a Gröbner basis of this ideal - thus significantly improving verification. Using our approach, we can verify the correctness of, and detect bugs in, upto 163-bit circuits in F(2163); whereas contemporary approaches are infeasible.