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

Abstract

現代密碼學函式庫中包含大量組合語言程式碼，無論是直接撰寫成，抑或是透過編譯器產生。其中，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.