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

SHF:Small：合作研究：用代数几何中的 Craig 插值修正算术电路

• 批准号: 1910368
• 负责人: Florian Enescu
• 金额: $ 18.99万
• 依托单位: Georgia State University Research Foundation, Inc.
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-06-15 至 2023-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1910368&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Rectification

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.

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

项目成果

Algebraic Techniques for Rectification of Finite Field Circuits

• DOI: 10.1109/vlsi-soc53125.2021.9606976
• 发表时间: 2021-10
• 期刊: 2021 IFIP/IEEE 29th International Conference on Very Large Scale Integration (VLSI-SoC)
• 作者: V. Rao;Haden Ondricek;P. Kalla;Florian Enescu

Word-Level Multi-Fix Rectifiability of Finite Field Arithmetic Circuits

有限域算术电路的字级多重修正可整流性

• 发表时间: 2021
• 期刊: The 22nd International Symposium on Quality Electronic Design (ISQED'21
• 作者: Rao, V;Ilioaea, I;Ondricek, H;Kalla, P;Enescu, F.
• 通讯作者: Enescu, F.

Logic Synthesis from Polynomials with Coefficients in the Field of Rationals

• DOI: 10.1109/ismvl57333.2023.00026
• 发表时间: 2023-05
• 期刊: 2023 IEEE 53rd International Symposium on Multiple-Valued Logic (ISMVL)
• 作者: Bhavani Sampathkumar;Bailey Martin;Ritaja Das;P. Kalla;Florian Enescu

Rectification of Integer Arithmetic Circuits using Computer Algebra Techniques

使用计算机代数技术修正整数运算电路

• DOI: 10.1109/iccd53106.2021.00039
• 发表时间: 2021
• 期刊: 2021 IEEE 39th International Conference on Computer Design (ICCD
• 作者: Rao, Vikas;Ondricek, Haden;Kalla, Priyank;Enescu, Florian
• 通讯作者: Enescu, Florian