Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform
Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform
复制标题
统一程序生成与验证：数论变换案例研究
DOI：
10.1007/978-3-030-99461-7_8
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Masahiro Masuda and Yukiyoshi Kameyama
中科院分区：
文献类型：
--
作者：
S. Nakano;S. Fujita;A. Kadokura;Y. Tanaka;R. Kataoka;A. Nakamizo;K. Hosokawa;S. Saita;Masahiro Masuda and Yukiyoshi Kameyama
在生成式编程的上下文中为生成的代码提供正确性保证是一个很难探索的问题。该工作提出了一种统一的程序生成和验证方法，并将其应用于格密码学中的关键构件--数论变换的实现。我们的验证策略是基于问题分解的：虽然我们发现试图一次性证明整个程序的功能正确性是困难的，但优化程序中的低级组件及其高级算法结构可以使用适当抽象级别的过程来单独验证，我们证明了这样的分解和随后的验证在基于无标记-最终风格的程序生成方法中自然地实现，从而导致对高度优化的程序进行端到端的功能正确性验证。
Giving correctness assurance to the generated code in the context of generative programming is a poorly explored problem. Such assurance is particularly desired for applications where correctness of the optimized code is far from obvious, such as cryptography.This work presents a unified approach to program generation and verification, and applies it to an implementation of Number-Theoretic Transform, a key building block in lattice-based cryptography. Our strategy for verification is based on problem decomposition: While we found that an attempt to prove functional correctness of the whole program all at once is intractable, low-level components in the optimized program and its high-level algorithm structure can be separately verified using procedures of appropriate levels of abstraction.We demonstrate that such a decomposition and subsequent verification of each component are naturally realized in a program-generation approach based on the tagless-final style, leading to an end-to-end functional correctness verification of a highly optimized program.
DOI：
10.1145/3009837.3009880
发表时间：
2016
期刊：
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
影响因子：
--
作者：
O. Kiselyov;Aggelos Biboudis;Nick Palladinos;Y. Smaragdakis
通讯作者：
Y. Smaragdakis
分阶段抽象解释器：通过元编程进行快速、模块化的整个程序分析
影响因子：
--
作者：
Guannan Wei;Yuxuan Chen;Tiark Rompf
通讯作者：
Tiark Rompf
优化NTT算法的验证
DOI：
--
发表时间：
2020
期刊：
Verified Software: Theories, Tools, Experiments
影响因子：
--
作者：
J. Navas;B. Dutertre;Ian A. Mason
通讯作者：
Ian A. Mason