Candidate:
Anil
Kumar
Boga
Title:A
graph
based
approach
for
formal
verification
of
Galois
field
multipliers
Date:
August
10,
2022
Time:
11:00
am
Place:
online
Supervisor(s):
Aagaard,
Mark
Abstract:
Data transfer between devices has increased rapidly with improvements in technology and the internet. To protect data from hackers, data is encrypted using methods of cryptography. To make the process of encryption faster, these circuits are often implemented in hardware. A bug in these circuits compromise the security of these systems. Cryptography circuits are becoming large and complex due to the increase in the importance of security and computation power available to the hacker. Hence verification of these circuits is of utmost importance. Time and resources taken by conventional methods increase exponentially with the size and complexity of circuits. Formal verification has the potential to improve the verification process by providing better than exponential complexity for some systems. Conventional formal verification methods do not perform well on cryptography circuits as they are “xor” rich circuits.
Cryptography circuits often consist of Galois field circuits. Galois field circuits are also widely used in various fields like communication, security, and signal processing. There are two main operations in Galois field namely addition and multiplication.
Addition is simply bitwise “xor” of operands. Multiplication is more complicated. Mastrovito, Montgomery and Karatsuba multipliers are optimized algorithms for multiplication. In this thesis, we developed novel methods for the formal verification of Galois field multipliers.
Equivalence verification of Galois field circuits becomes challenging as the size of inputs increases because the asymptotic worst-case complexity is exponential. The previous best-known method reduces the time and memory to some extent by using parallelism. In this thesis, a novel formal verification method is developed which provides a range of 4x—256x speedup when compared to the previously best-known method. We developed novel data structures and algorithms based on using the algebraic normal form as a canonical graph-based representation of Boolean functions. We have developed various normalization methods for our data structures. Experiments were performed on bit-level synthesized Mastrovito, Montgomery and Karatsuba multipliers.