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

随着互联网和移动的设备的普及，健壮、安全、可靠地传输信息变得比以往任何时候都重要。与这种操作相关联的计算机硬件执行复杂的算术计算，这需要对这种电路进行仔细的定制设计。定制设计增加了电路中存在漏洞的可能性，从而危及其安全性。验证这种电路的正确性是必要的。然而，它们的算术性质使它们难以验证，而当代算法缺乏解决这个问题的必要手段。 本计画探讨计算代数的应用，Groebner基本技术，以正式验证此类应用的电路。特别是，该项目分析了使用电路本身作为底层数据结构来执行Groebner基础计算和验证。通过使用逻辑综合作为连接计算代数算法和电路设计的桥梁，该项目解决了硬件验证的挑战和可扩展性。该项目影响了计算机辅助验证技术，安全系统设计，并促进了数学和计算机工程的知识和应用。网络安全硬件的验证还可以保护数据的隐私和安全，这对我们的社会有直接的影响。

With the spread of Internet and mobile devices, transferring information robustly, safely and securely has become more importantthan 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.