Formal Analysis of Galois Field Arithmetics - Parallel Verification and Reverse Engineering
This work addresses a bottleneck in hardware security and verification for engineers, offering a novel method to analyze GF circuits without needing known input/output bit positions or the irreducible polynomial, though it is incremental in improving existing verification techniques.
The paper tackles the problem of verifying and reverse engineering Galois field arithmetic circuits, which are used in communications and security, by developing a computer algebra technique that extracts the irreducible polynomial from gate-level implementations without prior knowledge, achieving high efficiency in experiments on synthesized multipliers.
Galois field (GF) arithmetic circuits find numerous applications in communications, signal processing, and security engineering. Formal verification techniques of GF circuits are scarce and limited to circuits with known bit positions of the primary inputs and outputs. They also require knowledge of the irreducible polynomial $P(x)$, which affects final hardware implementation. This paper presents a computer algebra technique that performs verification and reverse engineering of GF($2^m$) multipliers directly from the gate-level implementation. The approach is based on extracting a unique irreducible polynomial in a parallel fashion and proceeds in three steps: 1) determine the bit position of the output bits; 2) determine the bit position of the input bits; and 3) extract the irreducible polynomial used in the design. We demonstrate that this method is able to reverse engineer GF($2^m$) multipliers in \textit{m} threads. Experiments performed on synthesized \textit{Mastrovito} and \textit{Montgomery} multipliers with different $P(x)$, including NIST-recommended polynomials, demonstrate high efficiency of the proposed method.