Abstract

Galois field (GF) arithmetic finds numerous applications in communication and security-related hardware, and formal verification of GF arithmetic circuits is of prime importance. Current techniques for formally verifying such circuits are based on computer algebra methods that proved successful in verifying integer and GF arithmetic circuits. However, the methods are limited to designs with known bit position of the primary inputs and outputs. In addition, the methods for Galois field arithmetic circuits require the knowledge of the irreducible polynomial P(x), that affects the function and performance of the arithmetic implementation in GF(2m). This paper presents a computer algebra based technique that reverse engineers GF(2m) multipliers directly from the gate-level netlist of the design. The approach is based on first extracting a unique polynomial in Galois field of each output element independently. Then, it processes 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 the GF(2m) multipliers in m threads. Experiments were performed on bit-blasted Mastrovito and Montgomery multipliers with different P (x), including NIST-recommended polynomials and optimal polynomials for different microprocessor architectures.

References:

[1] Efficient Parallel Verification of Galois Feild Multipliers. (Best paper nomination)
Cunxi Yu and Maciej Ciesielski
IEEE/ACM 22nd Asia and South Pacific Design Automation Conference (ASP-DAC'17), Jan. 16-19, Chiba/Tokyo, Japan.

[2] Formal Analysis of Galois Field Arithmetic - Parallel Verification and Reverse Engineering.
Cunxi Yu and Maciej Ciesielski
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. (TCAD'18)

 

Tool

The tool is implemented in C++(g++4.9) and tested on Ubuntu System.

Download the tool and examples (tar.gz) (check online)

Please check README on github.

https://github.com/ycunxi/Parallel_Formal_Analysis_GaloisField

*** Report ends here ******(contact: ycunxi@umass.edu)