Galois Tech Talk: Application of Computer Algebra Techniques in Verification of Galois Field Multipliers: Potential + Challenges
Presented by Priyank Kalla.
Applications in Cryptography require multiplication and exponentiation operations to be performed over Galois fields GF(2^k). Therefore, there has been quite an interest in the hardware design and optimization of such multipliers. This has led to impressive advancements in this area — such as the use of composite field decomposition techniques, use of Montgomery multiplication, among others.
My research group has recently begun investigations in the verification of such Galois Field multipliers. Unfortunately, the word-length (k) in such multipliers can be very large: typically, k = 256. Due to such large word-lengths, verification techniques based on decision diagrams, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques, mainly Groebner bases theory, to tackle this problem. In this talk, we will see why Groebner bases techniques look promising, while at the same time also studying the challanges that have to be overcome.