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

算术电路是计算机、通信和网络安全系统的重要组成部分。这样的电路必须被设计为在功耗、高性能和低成本方面的效率。出于这个原因，算术电路经过仔细和定制的设计。手动定制设计增加了电路中出现错误或缺陷的可能性。算术电路中的错误可能会对系统的安全性造成灾难性的后果。攻击者可以恶意利用由于算法错误而引入的漏洞，并危及网络基础设施的安全。为了解决这些问题，该项目的研究人员不仅要检测错误的存在，还要自动纠正错误的算术电路，使其没有错误。由于研究团队在计算机工程和数学方面都有专业知识，该项目的新奇在于探索从这些领域到自动校正算术电路的跨学科概念，同时保持低成本和高效的设计实现。该项目将影响通信和网络安全系统的鲁棒电路主干的设计，以及确保网络基础设施能够抵御算术漏洞攻击。当电路执行算术计算时，研究人员探索了代数几何领域中的克雷格插值（CI）概念。虽然CI的概念在逻辑和自动推理的许多一阶理论中是众所周知的，但它还没有从代数的角度进行研究。研究人员发明了新的理论和算法，用于在代数几何中产生CI，并研究如何使用这些算法来自动纠正算术电路。有缺陷的算术电路可以以许多不同的方式被校正，即，可以计算许多校正函数，每个校正函数对应于不同的实现成本。该项目的调查的一个关键方面在于模拟成本的逻辑综合整流功能，相对于所有代数插值格的探索。该项目影响了计算机辅助验证技术，安全系统设计，并促进了数学和计算机工程的知识和应用。网络安全硬件的验证也保护了数据的隐私和安全，这对我们的社会有直接的影响。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.