遮罩 ML-KEM 抗旁通道攻擊性之形式驗證

Abstract

由於 Shor 演算法的出現，未來在具備大規模量子位元的通用型量子電腦出現後，現今廣泛使用的公鑰密碼系統（如 RSA 與橢圓曲線密碼系統）將不再安全。因此，後量子密碼學 (PQC) 近年來受到廣泛關注與研究。美國國家標準與技術研究院（NIST）於 2024 年公布首批標準化之後量子密碼演算法，其中 ML-KEM 為入選的演算法之一，使其成為旁通道分析研究的重要目標，ML-KEM 的旁通道防禦也因而隨之受到重視，其中遮罩（Masking）為常見的防禦方法之一。然而，遮罩實作往往容易因細微的實作錯誤仍然產生資訊洩漏，因此可藉由形式驗證工具使得遮罩實作具備安全性保證。本論文成果擴充了形式化驗證框架 LeakageVerif，使其支援先前尚未涵蓋但為 ML-KEM 必要的運算，包括模運算、向下取整除法，以及變數位移運算。使用擴充後的 LeakageVerif，我們對 Coron 等人於2022年所提出之算術與布林遮罩間的轉換進行形式驗證，並進一步驗證基於該遮罩轉換所實作之遮罩 ML-KEM。此研究成果顯示，形式驗證工具能有效應用於複雜之遮罩格密碼學實作，並能為其旁通道安全提供更為強力的保證。

Due to the advent of Shor's algorithm, widely deployed public-key cryptosystems, such as RSA and elliptic curve cryptography (ECC), are expected to become vulnerable in the presence of large-scale universal quantum computers in the near future. As a result, post-quantum cryptography (PQC) has attracted significant attention and has been actively researched in recent years. In 2024, the first standardized PQC schemes were published by the U.S. National Institute of Standards and Technology (NIST). Among these schemes, ML-KEM was selected as one of the standardized algorithms, making it a critical target for side-channel analysis research. At the same time, the resistance of ML-KEM against side-channel attacks has also been carefully considered. Though masking is one of the commonly adopted countermeasures, masked implementations are known to be error-prone and may still leak sensitive information due to subtle implementation flaws. Therefore, formal verification is used as a tool to provide security guarantees for masked implementations. In this work, we extend the formal verification framework LeakageVerif to support operations that were previously unsupported but are essential for ML-KEM, including modulo operations, floor division, and variable shift operations. Based on the extended tool, we formally verify both the arithmetic-to-Boolean (A2B) and Boolean-to-arithmetic (B2A) masking conversions proposed by Coron et al. in 2022, as well as a masked ML-KEM implementation built upon these conversions. This work demonstrates that formal verification tools can be effectively applied to complex masked lattice-based cryptographic implementations, providing stronger assurance of side-channel security.