臺灣博碩士論文加值系統

我們使用形式驗證工具 Cryptoline 驗證兩個利用 Bernstein-Yang 演算法的模反元素程式，其中一個是目前以模數為 2^255-19 最快的 x86 實作。本論文提供了驗證此程式所用到的驗證細節與技巧。我們利用形式化方法驗證了此程式的正確性，也展現了一個形式驗證在證明密碼學系統的可信度上的應用。

In this thesis, we conducted formal verification using the Cryptoline tool on two x86 implementations of the Bernstein-Yang algorithm, both designed to operate in constant time. Notably, one of these implementations represents the current fastest constant time modular inversion implementation for prime modulus 2^255-19 on x86. Our study provides comprehensive details and verification techniques for verifying these assembly implementations. By formal methods, the correctness of these implementations is systematically demonstrated. The results of this study provide substantial evidence for the effectiveness of formal verification in ensuring the accuracy and reliability of cryptographic systems.

Verification Letter from the Oral Examination Committee i
Acknowledgements iii
摘要 v
Abstract vii
Contents ix
List of Figures xiii
List of Tables xv
Denotation xix
Chapter 1 Introduction 1
Chapter 2 Preliminary 3
2.1 Modular Inverse Algorithms . . . . . . . . . . . . . . . . . . . . . . 3
2.2 Original Bernstein-Yang Algorithm . . . . . . . . . . . . . . . . . . 4
2.2.1 Definition of 2-adic division steps . . . . . . . . . . . . . . . . . . 4
2.2.2 Iterations of 2-adic division steps . . . . . . . . . . . . . . . . . . . 5
2.2.3 Fast computation of iterations of 2-adic division steps . . . . . . . . 8
2.2.4 Fast modular inversion computation . . . . . . . . . . . . . . . . . 9
2.3 Improved Bernstein-Yang Algorithm . . . . . . . . . . . . . . . . . 11
Chapter 3 Introduction to Cryptoline 13
3.1 Why Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . 13
3.2 What is CRYPTOLINE . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.2.1 Property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3.2.2 The structure of a CRYPTOLINE program . . . . . . . . . . . . . . . 18
3.2.3 CRYPTOLINE instructions . . . . . . . . . . . . . . . . . . . . . . . 19
3.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3.1 Examples of modeling . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3.2 CRYPTOLINE tricks . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.3.3 Verify an assembly program . . . . . . . . . . . . . . . . . . . . . 31
Chapter 4 Verifying a Simple Implementation 33
4.1 x86 25519 Implementation . . . . . . . . . . . . . . . . . . . . . . . 34
4.1.1 C implementation of fpinv25519.c . . . . . . . . . . . . . . . . . 34
4.2 Verifiy Simple Subroutines . . . . . . . . . . . . . . . . . . . . . . . 39
4.2.1 Verify modular addition . . . . . . . . . . . . . . . . . . . . . . . . 39
4.2.2 Verify conditional modular negation . . . . . . . . . . . . . . . . . 40
4.2.3 Verify signed multiplication with addition . . . . . . . . . . . . . . 40
4.2.4 Verify modular multiplication . . . . . . . . . . . . . . . . . . . . . 41
4.2.5 Verify signed multi-limb multiplication with addition . . . . . . . . 41
4.3 Verify 62 divstep iterations . . . . . . . . . . . . . . . . . . . . . . . 43
4.3.1 Pseudo code of the subroutine . . . . . . . . . . . . . . . . . . . . 43
4.3.2 Verify 1 divstep iteration . . . . . . . . . . . . . . . . . . . . . . . 44
4.3.3 Model the subroutine . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.3.4 Verify signed multi-limb multiplication and shift . . . . . . . . . . . 51
4.3.5 Completeness of verification of the subroutine . . . . . . . . . . . . 52
4.4 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
Chapter 5 Verifying a Fast Vectorized Implementation 55
5.1 Vectorized x86 25519 Implementation . . . . . . . . . . . . . . . . . 56
5.1.1 Outline of the assembly code . . . . . . . . . . . . . . . . . . . . . 57
5.2 Verify 20 divstep iterations . . . . . . . . . . . . . . . . . . . . . . . 62
5.2.1 An alternative definition of divstep . . . . . . . . . . . . . . . . . . 63
5.2.2 Verify each divstep iteration . . . . . . . . . . . . . . . . . . . . . 64
5.3 Verify vectorized update . . . . . . . . . . . . . . . . . . . . . . . . 67
5.3.1 Pseudo code of the subroutine . . . . . . . . . . . . . . . . . . . . 67
5.3.2 Computing in parallel . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.3.3 Computing with Montgomery multiplication . . . . . . . . . . . . . 72
5.3.4 Verify signed shift right computed with unsigned shift right . . . . . 74
5.3.5 Use a proof from Coq . . . . . . . . . . . . . . . . . . . . . . . . . 75
5.3.6 Reduce the output range . . . . . . . . . . . . . . . . . . . . . . . . 76
5.4 Verify radix 2^30 number multiplication with reduction . . . . . . . . 78
5.5 Verify simple subroutines . . . . . . . . . . . . . . . . . . . . . . . 80
5.6 Interleaving instructions . . . . . . . . . . . . . . . . . . . . . . . . 82
5.7 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
Chapter 6 Concluding Remarks 85
6.1 Time Consumption . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
6.2 The Verified Results . . . . . . . . . . . . . . . . . . . . . . . . . . 86
References 87
Appendix A — Proof 89
A.1 Proof about arithmetic precision . . . . . . . . . . . . . . . . . . . . 89
Appendix B — Table 91
B.1 Verification Time of the Simple Implementation . . . . . . . . . . . 91
B.2 Verification time of the Fast Vectorized Implementation . . . . . . . 92

[1] D. J. Bernstein and B.-Y. Yang. Fast constant-time gcd computation and modular inversion. 2019(3):340–398, 2019. https://tches.iacr.org/index.php/TCHES/article/view/8298.
[2] p. c. Daniel J. Bernstein and P. Wuille. safegcd-bounds. https://github.com/sipa/safegcd-bounds, 2021.
[3] W. Decker, G.-M. Greuel, G. Pfister, and H. Schönemann. SINGULAR 4-3-0 — A computer algebra system for polynomial computations. http://www.singular.uni-kl.de, 2022.
[4] Y.-F. Fu, J. Liu, X. Shi, M.-H. Tsai, B.-Y. Wang, and B.-Y. Yang. Signed cryptographic program verification with typed cryptoline. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS ’19, page 1591–1606, New York, NY, USA, 2019. Association for Computing Machinery.
[5] P. L. Montgomery. Modular multiplication without trial division. Mathematics of Computation, 44:519–521, 1985.
[6] A. Niemetz, M. Preiner, and A. Biere. Boolector 2.0. J. Satisf. Boolean Model. Comput., 9(1):53–58, 2014.