SHF: Small: New Directions in Groebner Basis based Verification using Logic Synthesis Techniques

University Of Utah, Salt Lake City UT

Investigators

Abstract

With the spread of Internet and mobile devices, transferring information robustly, safely and securely has become more important than ever. Computer hardware associated with such operations performs sophisticated arithmetic computations, which requires careful, custom design of such circuits. Custom design raises the potential for bugs in the circuits, compromising their security. Verification of the correctness of such circuits is an imperative. However, their arithmetic nature makes them notoriously hard to verify, and contemporary algorithms lack the wherewithal to address this problem. This project investigates the application of computational algebra, Groebner basis techniques, to formally verify circuits for such applications. In particular, the project analyzes the use of the circuit itself as the underlying data-structure to perform Groebner basis computations and verification. By using logic synthesis as a bridge to connect computational algebra algorithms with circuit design, the project addresses the challenge and scalability of hardware verification. The project impacts computer-aided verification technology, secure system design, and it advances knowledge and application in mathematics as well as computer engineering. Validation of hardware for cyber-security also protects the privacy and security of data, which has a direct impact on our society.