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

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

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.