密碼學函式庫實作中向量化基本操作的形式驗證

Formal Verification of Vectorized Implementations of Cryptographic Primitives

潘廣霖(Kuang-Lin Pan)

指導教授 ： 陳偉松 ； 王柏堯

國立臺灣大學/電機資訊學院/資訊工程學系/碩士(2023年)

https://doi.org/10.6342/NTU202300977

摘要

現代密碼學函式庫中包含大量組合語言程式碼，無論是直接撰寫成，抑或是透過編譯器產生。其中，SIMD 指令常常做為提升效率的優化手段。如何有效率且簡約地使用手邊現有的工具來驗證這樣的程式碼，是正規驗證的一大課題。本論文拓展了模型檢查工具 CryptoLine，加入一系列的向量指令，並從實作後量子密碼學協議的函式庫中選取一些子程式來驗證其正確性和整數運算的安全性。驗證結果說明 Vector CryptoLine 採用的方法能順利建模來描述此類向量指令集在計算快速乘法時的行為，並且有潛力能被用來驗證未來其他後量子密碼學的函式庫。

關鍵字

形式驗證 ； 密碼學 ； 向量化運算

並列摘要

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.

並列關鍵字

formal verification ； cryptography ； vectorized computation

參考文獻

[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.