SHF:Small:Collaborative Research: Rectification of Arithmetic Circuits with Craig Interpolants in Algebraic Geometry

University Of Utah, Salt Lake City UT

Investigators

Abstract

Arithmetic circuits are a critical component of computer, communication and cyber-security systems. Such circuits have to be designed for efficiency in terms of power consumption, high performance and low cost. For this reason, arithmetic circuits undergo careful and custom design. Manual custom design raises the potential for errors or bugs in the circuits. Bugs in arithmetic circuits can have catastrophic consequences with regards to safety and security of systems. Attackers can maliciously exploit the vulnerabilities introduced due to arithmetic bugs and compromise the security of cyber-infrastructure. To address these issues, the investigators of this project conduct research to not just detect the presence of bugs, but also to automatically rectify buggy arithmetic circuits to make them free of errors. As the team of researchers has expertise in computer engineering as well as in mathematics, the novelty of the project lies in exploring cross-disciplinary concepts from these areas to auto-correct arithmetic circuits, while maintaining low cost and efficient design implementation. The project will impact the design of robust circuit backbone for communication and cyber-security systems, as well as in ensuring cyber-infrastructure to be resilient to arithmetic bug-attacks. As the circuits perform arithmetic computations, the investigators explore the concept of Craig Interpolation (CI) in the domain of algebraic geometry. While the concept of CI is well known in many first-order theories in logic and automated reasoning, it has not been studied from an algebraic perspective. The investigators invent new theories and algorithms for producing CI in algebraic geometry, and investigate how these algorithms can be used to automatically rectify arithmetic circuits. A buggy arithmetic circuit can be rectified in many different ways, i.e. many rectification functions can be computed, each corresponding to different implementation costs. A key aspect of the project's investigations lies in modeling the cost of logic synthesis of rectification functions vis-a-vis the exploration of the lattice of all algebraic interpolants. 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. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.