With the spread of Internet and mobile devices, transferring information safely and securely has become more important than ever. The hardware and software systems utilized in such applications, e.g. cryptography, perform arithmetic computations over Galois fields. The specialized nature and the high complexity of the hardware architectures require manual, custom design, which raises the potential for errors/bugs in the design implementation. Hardware bugs in arithmetic circuits not only cause unintended operation, but they also make cryptosystems vulnerable to security attacks. Validating the correctness of, and bug-catching in, arithmetic hardware is imperative. This project investigates the use of modern Symbolic Computer Algebra techniques for formal verification of Galois field arithmetic circuits.
Verification of cyber-security is a problem of great importance, and it is attracting a lot of research at the software-level. However, hardware verification of primitive Galois field computations in crypto-systems has not seen much breakthrough. The main reason for this is that the arithmetic circuit architectures employed in cryptography are very complex and their size is extremely large. Conventional verification techniques are unable to scale with respect to the large size. To address these problems, the project aims to integrate computer algebra with circuit analysis techniques for verification. By exploiting the circuit design information, the project will attempt to overcome the complexity of symbolic computation. This research enables design of domain-specific computer-aided verification tools for efficient, scalable verification of Galois field circuits. The project impacts computer-aided verification technology, secure system-design and validation, and it advances fundamental knowledge in both computer algebra and design verification of arithmetic circuits. Enabling the validation of security and privacy of data also, in general, impacts the society.
