Formal Analysis of Galois Field Arithmetics - Parallel Verification and Reverse Engineering

TL;DR

This paper introduces a computer algebra method for verifying and reverse engineering Galois field multipliers directly from gate-level designs, extracting the irreducible polynomial and input/output bit positions efficiently.

Contribution

It presents a novel parallel approach for analyzing GF(2^m) multipliers, enabling verification and reverse engineering without prior knowledge of input/output bit positions or the irreducible polynomial.

Findings

Successfully reverse engineered GF(2^m) multipliers in parallel

Demonstrated high efficiency on synthesized Mastrovito and Montgomery multipliers

Effectively extracted irreducible polynomials, including NIST standards

Abstract

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.