PQC Masking 驗證論文閱讀分析：很多硬體安全真正缺的，不是多跑幾次 solver，而是證明能不能跨整個參數族活下去

論文基本資訊

• 論文標題：From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification
• 作者：Ray Iskander、Khaled Kirah
• 年份：2026
• 來源：arXiv:2604.18717
• 論文連結：https://arxiv.org/abs/2604.18717
• 主題：PQC Hardware Security、Masking Verification、Formal Verification、Lean 4、Side-Channel Resistance、ML-KEM / ML-DSA

如果前面幾篇 sectools.tw 的主線，已經一路從 PQC 硬體 side-channel 驗證、pre-silicon masking 證據、AI / agent runtime 的形式保證 寫到「到底哪些安全性是真的被證明，而不是只是被大量測過」，那這篇論文剛好補上一個非常關鍵、但很容易被低估的縫：你說某個 masking 性質在一個小 modulus 上被 SMT solver 枚舉驗過，這到底算不算真的證明它對正式 PQC 參數也成立？

作者的答案很直接：不算，至少不夠。 因為 ML-KEM 與 ML-DSA 真正工作的 modulus，和你拿來做有限枚舉驗證的小 toy setting，根本不是同一件事。這篇論文真正厲害的地方，不是再跑更大一輪 solver，而是把整件事從 bit-vector／有限域枚舉問題，改寫回 ring theory 問題，然後用 Lean 4 做出一個對所有 q > 0 都成立的 machine-checked universal proof。

這篇論文想解決什麼？

背景先講白一點：PQC hardware 尤其是 ML-KEM、ML-DSA 這類 NTT-heavy 設計，常用 first-order arithmetic masking 來擋 power side-channel。形式上，secret x 會被拆成兩個 share s0、s1，滿足：

s0 + s1 ≡ x (mod q)

對攻擊者來說，如果他只能 probe 單一 wire，那理想狀況是：不管 secret 是什麼，單獨看到某條 wire 的分布都不應該改變。

作者前作的 QANARY 框架已經把這件事往工程上推很遠：它能在大規模 PQC accelerator netlist 上做 structural dependency analysis，甚至驗到 117 萬 cell、30 個 module。但前作裡一個關鍵 soundness theorem，實際上只在 q = 5 的有限情況上，用 Z3 / CVC5 與 Python 枚舉方式 machine-check 過。

這就留下了一個很尷尬的空缺：

• ML-KEM 用的 modulus 是 3329
• ML-DSA 用的 modulus 是 8,380,417
• 但你真正 machine-check 的卻是 q = 5

論文要補的，就是這個從「有限例子被驗過」到「所有 production parameter 都被結構性涵蓋」之間的斷層。

作者的核心主張：SMT 枚舉給的是證據，不是可攜帶的保證

這篇最值得記住的一句話，可以濃縮成：

SMT solvers 很會把有限世界檢查乾淨，但它們不會替你做 modulus 上的結構性歸納。

作者把有限枚舉方法的限制拆得很清楚：

• 沒有 induction：在 q = 5 上成立，不代表在 q = 3329 上也自動成立
• 規模爆炸：wire function 空間會隨參數爆開，根本不可能靠枚舉硬推到 production modulus
• trusted base 太大：你還得一起信 Z3、CVC5、外圍 Python 編碼與 SMT-LIB 轉譯沒有搞錯

所以這篇不是在嫌 SMT 沒用，而是在說：如果你想把 masking verification 提升到 certification-ready 等級，光有 finite-domain evidence 還不夠，你需要 universal proof。

論文真正證明了什麼？

它要證的核心性質其實很簡潔。作者定義一個 wire function：

w : Zq × Zq → β

也就是某條 wire 的值，來自兩個 shares。接著定義所謂的 value-independence：

w(x - s1, s1) = w(x' - s1, s1)
for all s1, x, x'

直白講，就是：在 share reparametrization 後，這條 wire 的值不會因 secret 換成別的值而改變。

作者的主要定理就是：

只要 wire function 對 secret value-independent，那它對任何 secret 的 marginal histogram 都相同；換句話說，單條 wire 的分布不隨 secret 改變。

這正是「這條 wire 不洩漏 secret」所需要的核心代數前提。更重要的是，這個結果不再只是在特定 q、特定輸出型別、特定列舉空間裡成立，而是對 所有 q > 0、所有 wire function、任意可判等輸出型別 都成立。

最漂亮的地方：主定理在 Lean 4 裡只要五行

這篇很有戲劇性的地方，是作者把先前需要 2²⁵ 次 finite evaluation 才敢說「我們 machine-check 過」的東西，換成 Lean 4 後，主證明本體只剩五行 tactic script。

這不是在耍帥，而是剛好證明一件更大的事：原本看起來很重的驗證，其實不是因為性質本身複雜，而是因為你之前站在錯的 formalism 上。

作者的論點很狠也很準：

• 在 bit-vector / SMT 世界，你必須把 universality 拆成一大堆有限例子去跑
• 在 Z/qZ 的 commutative ring 世界，關鍵 reparametrization 不過就是 sub_add_cancel 這種自然代數恆等式

換句話說，這篇不是只把 proof 寫進 Lean，而是指出 arithmetic masking verification 的自然抽象層，本來就應該是 ring axioms，不是 bit-vector SAT。

除了主定理，作者還補了哪些 supporting results？

這篇不是只交一條 theorem 就收工。它另外整理出一整組 supporting proof suite，涵蓋：

• Boolean / arithmetic reparametrization round-trip
• reparametrization bijectivity
• overflow bounds，把抽象代數結果接回 bit-vector implementation
• RNG bias characterization
• universal non-tightness counterexample：證明某些 converse 不會自動成立

這裡我特別喜歡作者沒有把結果包裝成「既然主 theorem 成立，其他都不是事」。相反地，他們很老實地補上實作世界需要的橋：

• 抽象代數證明很漂亮，但硬體最後還是 bit-width、overflow、RNG bias 這些髒東西在作祟
• 所以你不能只證 abstract theorem，還得證明 abstract layer 跟 implementation layer 之間怎麼接

這讓整篇不只是數學上更乾淨，也更接近真實 certification pipeline。

這篇對 PQC hardware security 的真正意義是什麼？

我覺得這篇的價值不在「Lean 4 很厲害」而已，而在於它把一種很常見、卻很容易被默默接受的安全錯覺拆掉了：

很多硬體安全驗證真正缺的，不是再多跑一點 testcase，而是先分清楚你手上的到底是 sample-level evidence，還是 parameter-portable proof。

在 PQC migration 時代，這個差異很大。因為 NIST 已經把正式標準推上線，後面要面對的是：

• 不同 modulus、不同 parameter set 的可攜性
• 長生命週期硬體 IP 的再使用
• 供應鏈審查與 third-party assurance
• 設計者如何向 evaluator 說明「這不是只在 toy setting 成立」

這篇論文等於替 PQC hardware masking verification 補上一塊更適合進入 assurance story 的底座：把本來依賴 solver 列舉的 soundness claim，往 kernel-checked universal proof 推進。

它也順手說明了一件事：trusted base 本身就是安全面的一部分

很多工程論文談 formal verification，只會講「有沒有 proof」，但這篇很清楚地談到 trusted base。先前方法要一起信：

• Z3
• CVC5
• 外部 Python 腳本
• SMT encoding 本身沒失真

Lean 4 這版 proof 的意義，是把信任基底壓回到 Lean kernel。這不是說 kernel 就 magically perfect，而是說：你把原本分散在多個求解器與 glue code 的信任風險，收斂到更小、更可審計的一層。

這個思路其實跟 agent runtime security 很像：真正有價值的 assurance，不是多一個 wrapper，而是縮小那個你最後不得不信的核心。

這篇論文的限制在哪？

當然，它不是「PQC masking verification 已經全部解完」。至少有幾個邊界要記得：

• 它證的是 r-free sub-theorem，不是整個 probabilistic security pipeline 的全部細節一次收完
• information-theoretic conclusion 本身沒有全部在 artifact 裡 formalize，作者也明講這部分是由標準論證接上
• 這篇更偏 foundation paper，不是直接給你完整 production sign-off recipe
• glitches、higher-order probing、物理實作細節 仍然需要其他層的模型與證據

也就是說，它補的是很底層、很關鍵的一塊地基；不是把整棟房子一次蓋完。

我怎麼看這篇？

我會把這篇看成一種很典型、也很值得資安研究多做的工作：不是再發明一個新攻擊，而是回頭檢查我們原本拿來說服自己的證據，到底哪裡其實還只是近似。

它最有價值的，不是「五行證完」這個漂亮故事，而是背後那個更不舒服的訊息：

很多看起來已經很正式的硬體安全驗證，真正差的未必是更多算力，而是把問題翻回正確數學語言的那一步。

對 PQC hardware 這條線來說，這篇論文提醒我們：當你真的要把 masking assurance 帶進標準、認證與長期維護，關鍵往往不是測得夠不夠多，而是證明能不能跨參數活下去。

一句話總結

這篇論文真正補上的，不是又一個 PQC masking 結果，而是把「在小世界裡驗過」提升成「在整個 modulus 家族裡都站得住」的那座橋。