SHF: Small: Collaborative Proposal: Efficient Computer Algebra Techniques for Scalable Verification of Galois Field Arithmetic Circuits

随着互联网和移动设备的普及，安全可靠地传输信息变得比以往任何时候都更加重要。在这样的应用中使用的硬件和软件系统，例如密码学，在伽罗华域上执行算术计算。硬件体系结构的专业性和高度复杂性需要手动定制设计，这增加了设计实施中出现错误/错误的可能性。算术电路中的硬件错误不仅会导致意外操作，还会使密码系统容易受到安全攻击。验证算术硬件的正确性并捕获错误势在必行。本项目研究使用现代符号计算机代数技术对伽罗华域算术电路进行形式化验证。网络安全验证是一个非常重要的问题，也是软件层面的研究热点。然而，密码系统中原始伽罗瓦域计算的硬件验证并没有太大的突破。其主要原因是密码学中采用的算术电路结构非常复杂，并且其规模非常大。传统的验证技术不能针对大尺寸进行缩放。为了解决这些问题，该项目旨在将计算机代数与电路分析技术相结合进行验证。通过利用电路设计信息，该项目将试图克服符号计算的复杂性。这项研究使设计特定领域的计算机辅助验证工具成为可能，以实现伽罗瓦现场电路的高效、可扩展验证。该项目对计算机辅助验证技术、安全系统设计和验证产生了影响，并提高了计算机代数和算术电路设计验证的基础知识。一般来说，启用数据安全和隐私验证也会对社会产生影响。

With the spread of Internet and mobile devices, transferring information safely and securely has become more important than ever. The hardware and software systems utilized in such applications, e.g. cryptography, perform arithmetic computations over Galois fields. The specialized nature and the high complexity of the hardware architectures require manual, custom design, which raises the potential for errors/bugs in the design implementation. Hardware bugs in arithmetic circuits not only cause unintended operation, but they also make cryptosystems vulnerable to security attacks. Validating the correctness of, and bug-catching in, arithmetic hardware is imperative. This project investigates the use of modern Symbolic Computer Algebra techniques for formal verification of Galois field arithmetic circuits. Verification of cyber-security is a problem of great importance, and it is attracting a lot of research at the software-level. However, hardware verification of primitive Galois field computations in crypto-systems has not seen much breakthrough. The main reason for this is that the arithmetic circuit architectures employed in cryptography are very complex and their size is extremely large. Conventional verification techniques are unable to scale with respect to the large size. To address these problems, the project aims to integrate computer algebra with circuit analysis techniques for verification. By exploiting the circuit design information, the project will attempt to overcome the complexity of symbolic computation. This research enables design of domain-specific computer-aided verification tools for efficient, scalable verification of Galois field circuits. The project impacts computer-aided verification technology, secure system-design and validation, and it advances fundamental knowledge in both computer algebra and design verification of arithmetic circuits. Enabling the validation of security and privacy of data also, in general, impacts the society.