請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/88563完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 陳偉松 | zh_TW |
| dc.contributor.advisor | Tony Tan | en |
| dc.contributor.author | 潘廣霖 | zh_TW |
| dc.contributor.author | Kuang-Lin Pan | en |
| dc.date.accessioned | 2023-08-15T16:51:08Z | - |
| dc.date.available | 2023-11-09 | - |
| dc.date.copyright | 2023-08-15 | - |
| dc.date.issued | 2023 | - |
| dc.date.submitted | 2023-07-22 | - |
| dc.identifier.citation | [1] Daniel J. Bernstein, Tung Chou, and Peter Schwabe. 2013. McBits: Fast constant-time code-based cryptography. In Cryptographic hardware and embedded systems - CHES 2013, Springer Berlin Heidelberg, Berlin, Heidelberg, 250–272.
[2] Eric Cheng. 2016. Binary analysis and symbolic execution with angr. PhD thesis. PhD thesis, The MITRE Corporation. [3] Dong Pyo Chi, Jeong Woon Choi, Jeong San Kim, and Taewan Kim. 2015. Lattice based cryptography for beginners. Cryptology ePrint Archive. [4] Tung Chou. McBits revisited. In Cryptographic Hardware and Embedded Systems–CHES: 19th International Conference, Taipei, Taiwan, September 25-28, 2017, Proceedings, Springer, 213–231. [5] Chi-Ming Marvin Chung, Vincent Hwang, Matthias J Kannwischer, Gregor Seiler, Cheng-Jhih Shih, and Bo-Yin Yang. 2021. NTT multiplication for NTT-unfriendly rings: New speed records for saber and NTRU on cortex-M4 and AVX2. IACR Transactions on Cryptographic Hardware and Embedded Systems (2021), 159–188. [6] Stephen A Cook and Stȧl O Aanderaa. 1969. On the minimum computation time of functions. Transactions of the American Mathematical Society 142, (1969), 291–314. [7] Jan-Pieter D’Anvers, Angshuman Karmakar, Sujoy Sinha Roy, and Frederik Vercauteren. 2018. Saber: Module-LWR based key exchange, CPA-secure encryption and CCA-secure KEM. In Progress in cryptology – AFRICACRYPT 2018, Springer International Publishing, Cham, 282–305. [8] Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, and Grigore Roşu. 2019. A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture. In Proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation (PLDI’19), ACM, 1133–1148. DOI: http://dx.doi.org/10.1145/3314221.3314601. [9] Shuhong Gao and Todd Mateer. 2010. Additive fast fourier transforms over finite fields. IEEE Transactions on Information Theory 56, 12 (2010), 6265–6272. [10] Michael T. Heideman, Don H. Johnson, and C. Sidney Burrus. 1985. Gauss and the history of the fast fourier transform. Archive for History of Exact Sciences 34, 3 (September 1985), 265–277. DOI: http://dx.doi.org/10.1007/BF00348431 [11] Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2022. Verified NTT multiplications for NISTPQC KEM lattice finalists: Kyber, SABER, and NTRU. IACR Transactions on Cryptographic Hardware and Embedded Systems (2022), 718–750. [12] Ming-Hsien Tsai Jiaxiang Liu Xiaomu Shi and Bo-Yin Yang. 2022. CryptoLine: A tutorial. (2022). Retrieved May 29, 2023 from https://github.com/fmlab-iis/cryptoline/blob/ master/doc/tutorial.pdf. [13] M Donald MacLaren. 1970. The art of computer programming. Volume 2: Seminumerical algorithms (donald e. knuth). SIAM. [14] Robert J McEliece. 1978. A public-key cryptosystem based on algebraic coding theory. Coding Thv 4244, (1978), 114–116. [15] John M Pollard. 1971. The fast fourier transform in a finite field. Mathematics of computation 25, 114, 365–374. [16] Léo Ducas Roberto Avanzi Joppe Bos and Damien Stehlé. 2019. CRYSTALS-kyber (version 2.0) – submission to round 2 of the NIST post-quantum project. [17] Dipanwita Sarkar, Oscar Waddell, and R. Kent Dybvig. 2004. A nanopass infrastructure for compiler education. In Proceedings of the ninth ACM SIGPLAN international conference on functional programming (ICFP ’04), Association for Computing Machinery, New York, NY, USA, 201–212. DOI: http://dx.doi.org/10.1145/1016850.1016878. [18] Harshdeep Singh. 2020. Code based cryptography: Classic McEliece. Retrieved May 22, 2023 from https://arxiv.org/abs/1907.12754. [19] Andrei L Toom. 1963. The complexity of a scheme of functional elements realizing the multiplication of integers. In Soviet mathematics doklady, 714–716. [20] VAMPIRE -Virtual Applications and Implementations Research Lab. 2022. SUPERCOP. Retrieved May 22, 2023 from https://bench.cr.yp.to/supercop.html. [21] Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. In Proceedings of the 2017 ACM SIGSAC conference on computer and communications security, 1789–1806. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/88563 | - |
| dc.description.abstract | 現代密碼學函式庫中包含大量組合語言程式碼，無論是直接撰寫成，抑或是透過編譯器產生。其中，SIMD 指令常常做為提升效率的優化手段。如何有效率且簡約地使用手邊現有的工具來驗證這樣的程式碼，是正規驗證的一大課題。本論文拓展了模型檢查工具 CryptoLine，加入一系列的向量指令，並從實作後量子密碼學協議的函式庫中選取一些子程式來驗證其正確性和整數運算的安全性。驗證結果說明 Vector CryptoLine 採用的方法能順利建模來描述此類向量指令集在計算快速乘法時的行為，並且有潛力能被用來驗證未來其他後量子密碼學的函式庫。 | zh_TW |
| dc.description.abstract | Modern cryptographic libraries contain a large amount of assembly code derived either manually or through the use of compilers, where SIMD instructions are commonly used to reduce latency and increase speed. There is a challenge in verifying them efficiently and succinctly with the tools we have at our disposal. This thesis extends the model checking software, CryptoLine, with a set of vectorized instructions. Selected subroutines from various post-quantum cryptographic libraries are examined for correctness and integer safety. The results demonstrate that the approach adopted by Vector CryptoLine is successful in modelling these vectorized instructions in various forms of fast multi-limb multiplications, and has the potential to be used to validate other post-quantum cryptographic libraries in the future. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2023-08-15T16:51:08Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2023-08-15T16:51:08Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 口試委員會審定書 (Thesis Acceptance Certificate) .. i
Acknowledgements .. iii 摘要 (Abstract in Chinese) .. v Abstract .. vii Contents .. ix List of Figures .. xi List of Tables .. xiii List of listings .. xv Chapter 1 Introduction .. 1 Chapter 2 Background .. 3 2.1 Multi-precision arithmetic .. 3 2.2 Fast Fourier transform .. 4 2.3 Lattice-based cryptography .. 5 2.4 Code-based cryptography .. 6 2.5 Design on domain-specific languages .. 6 Chapter 3 Overview of CryptoLine .. 9 3.1 Syntax .. 10 3.2 Semantics .. 11 3.3 Safety constraints .. 13 Chapter 4 Vector CryptoLine .. 15 4.1 Syntax extension .. 15 4.2 Design of Vector CryptoLine .. 16 4.3 Automatic variable aliasing .. 19 4.4 Case studies .. 20 4.4.1 Kyber NTT .. 20 4.4.2 SABER NTT .. 22 Chapter 5 Implementations .. 25 5.1 The additive FFT .. 25 5.2 The source code .. 27 5.3 Techniques used in McBits .. 29 5.4 Extraction of assembly code .. 31 5.5 Modeling the bit-shiftings .. 39 5.6 Generating the specifications .. 41 5.6.1 The post-condition .. 46 5.6.2 Implemention details .. 50 5.7 Verification result .. 51 Chapter 6 Conclusion .. 53 References .. 55 | - |
| dc.language.iso | en | - |
| dc.subject | 形式驗證 | zh_TW |
| dc.subject | 密碼學 | zh_TW |
| dc.subject | 向量化運算 | zh_TW |
| dc.subject | vectorized computation | en |
| dc.subject | formal verification | en |
| dc.subject | cryptography | en |
| dc.title | 密碼學函式庫實作中向量化基本操作的形式驗證 | zh_TW |
| dc.title | Formal Verification of Vectorized Implementations of Cryptographic Primitives | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 111-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.coadvisor | 王柏堯 | zh_TW |
| dc.contributor.coadvisor | Bow-Yaw Wang | en |
| dc.contributor.oralexamcommittee | 楊柏因;黃鐘揚 | zh_TW |
| dc.contributor.oralexamcommittee | Bo-Yin Yang;Chung-Yang Huang | en |
| dc.subject.keyword | 形式驗證,密碼學,向量化運算, | zh_TW |
| dc.subject.keyword | formal verification,cryptography,vectorized computation, | en |
| dc.relation.page | 57 | - |
| dc.identifier.doi | 10.6342/NTU202300977 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2023-07-24 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 資訊工程學系 | - |
| 顯示於系所單位： | 資訊工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-111-2.pdf | 1.14 MB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。