Verification of composite Galois field multipliers over GF ((2m)n) using computer algebra techniques

Galois field computations abound in many applications, such as in cryptography, error correction codes, signal processing, among many others. Multiplication usually lies at the core of such Galois field computations, and is one of the most complex operations. Hardware implementations of such multipliers become very expensive. Therefore, there have been efforts to reduce the design complexity by decomposing the Galois field GF(2^k) as GF ((2^m)ⁿ) where k = m × n. Such a decomposition introduces a hierarchical abstraction - lifting the ground field from GF (2) (bit-level) to GF (2^m) (word-level) - thus simplifying the design. This paper addresses the formal verification problem of such multipliers designed over GF ((2^m)ⁿ), using a computer algebra and algebraic geometry based approach. To prove that the composite field multiplier implementation matches the original specification, we hierarchically formulate the verification problem using the Hilbert´s Nullstellensatz over Galois Fields. A Gröbner basis engine is employed as the underlying computational framework. Experiments are performed with various variable/term orders to demonstrate the efficacy of our approach. We can verify the correctness of upto 1024bit multipliers, whereas SAT/SMT-based approaches are in-feasible.