Generating Programs for Polynomial Multiplication with Correctness Assurance

Generating Programs for Polynomial Multiplication with Correctness Assurance
复制标题

DOI:
10.1145/3571786.3573017
复制
发表时间:
2023-01
期刊:
Proceedings of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation
影响因子:
--
通讯作者:
Ryohei Tokuda;Yukiyoshi Kameyama
Ryohei Tokuda;Yukiyoshi Kameyama
中科院分区:
其他
文献类型:
--
作者:
Ryohei Tokuda;Yukiyoshi Kameyama

文献摘要

相似文献

程序生成技术在需要高性能的领域中很流行,例如线性代数、图像处理和数据库。然而,很难生成具有正确性保证的高性能程序,而密码学需要两者兼而有之。Masuda和Kameyama提出了一个基于DSL的框架来实现程序生成器、分析器和公式生成器,并得到了许多密码算法所必需的数论变换(NTT)的有效和正确的实现。本文从两个方面推进了他们的研究。首先,我们开发了一个生成和分析框架,以便程序生成由程序分析驱动。作为一个具体的结果,我们发现在以前的研究中遗漏了一个优化。其次,我们研究了该框架是否可以应用于其他算法,包括逆NTT。通过组合生成的程序,我们得到了多项式乘法的有效和正确的实现,多项式乘法是几种后量子密码算法的密钥。
Program-generation techniques prevail in domains that need high performance, such as linear algebra, image processing, and database. Yet, it is hard to generate high-performance programs with correctness assurance, and cryptography needs both. Masuda and Kameyama proposed a DSL-based framework for implementing a program generator, an analyzer, and a formula generator, and obtained an efficient and correct implementation of Number-Theoretic Transform (NTT) that is necessary for many cryptographic algorithms. This paper advances their study in two ways. First, we develop a generation-and-analysis framework so that program generation is driven by program analysis. As a concrete result, we have found an optimization missed in previous studies. Second, we investigate whether the framework can be applied to other algorithms, including inverse NTT. By combining generated programs, we have obtained an efficient and correct implementation of polynomial multiplication, the key for several post-quantum cryptographic algorithms.