Masked NTT Hardware 論文閱讀分析：很多 PQC 硬體真正卡住的，不是有沒有 masking，而是 tape-out 前根本證不出它沒漏

本文由 AI 產生、整理與撰寫。

論文基本資訊

• 論文標題：Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators
• 作者：Ray Iskander、Khaled Kirah
• 年份：2026
• 來源：arXiv:2604.15249
• 論文連結：https://arxiv.org/abs/2604.15249
• DOI：10.48550/arXiv.2604.15249
• 主題：PQC Hardware Security、Side-Channel Resistance、Masking Verification、NTT Accelerators、Formal Verification、Pre-Silicon Security

這篇論文我覺得很值得補，因為它碰到一個 post-quantum 硬體安全裡很現實、但常被「有做 masking 就好像差不多安全了」掩蓋掉的問題：很多 PQC accelerator 真正難的，不是想出 masking 方案，而是你根本沒辦法在 tape-out 前，對一個大到 production 等級的 NTT 設計，證明那些 share 沒有在某個你沒注意到的地方偷偷重新匯流。

這件事之所以重要，是因為 ML-KEM（FIPS 203）和 ML-DSA（FIPS 204）這種 lattice-based PQC 硬體，不只規模大，還有大量 arithmetic masking、pipeline register、forwarding path 與 modular reduction。很多現有 masking verification 工具，在 Boolean gadget 或小型組件上很好用，但一到這種 production 級的 arithmetic NTT 設計，就不是 timeout，就是根本看不到 multi-cycle 的 share recombination。

所以這篇 paper 最有價值的地方，不只是又做一個 verification tool，而是它抓到核心落差：真正卡住 FIPS 140-3 side-channel evidence 的，常常不是工程師不知道要驗，而是現有 exact verification 根本撐不到 production size。

這篇在解什麼問題？

作者想解的是一個非常實務的 pre-silicon security 問題：對大規模、first-order masked 的 PQC accelerator，如何在正式流片前，快速又有數學保證地找出可能發生 share convergence 的危險路徑，並把人工 triage 範圍壓到還能處理的程度。

masking 的基本安全直覺是：同一個 secret 的不同 share，不該在可觀測的組合邏輯路徑裡重新相遇。問題是，當設計裡有：

• 大量 arithmetic operations，
• deep pipelines，
• register boundary，
• NTT / Barrett reduction 這種 field arithmetic data path，

你很難靠人工 review 或傳統單週期工具真的看清楚哪裡出了事。

也就是說，這篇在解的不是「如何證明一個小 masking gadget 安全」，而是：如何把 masking verification 從幾千 cell 的學術尺度，拉到百萬 cell 的 production 硬體尺度。

核心想法：先接受 exact verification 不會先解決規模問題，再用分層驗證把問題壓回可處理範圍

這篇的路線我蠻認同，因為它沒有假裝自己一上來就能對 100 多萬 cells 做完整 exact proof，而是走一條比較成熟的分層路線。作者提出一個四階段 hierarchy：

1. D0 / D1 structural dependency analysis
2. fresh-mask refinement
3. Boolean SADC
4. Arithmetic SADC

這套設計的精神很清楚：先用 sound-but-incomplete 的 structural test 快速抓出可能有問題的地方，再用更重的 distributional / arithmetic refinement 把 false positives 壓掉。

換句話說，它不是先追求「每一條線都精準定案」，而是先把 production 規模下最關鍵的事情做好：零漏報地抓出可能危險區，然後把人工和 SMT 的火力集中在真正值得看的 subset 上。

真正值得記的不是 D1，而是它把 multi-cycle leakage 明確拉進來

很多 masking verification 的盲點，是只看單一 clock cycle。作者特別補了一個 MC-D1（multi-cycle D1），把 label propagation 延伸跨 register boundary 做 fixed-point 分析。

這個補強很關鍵，因為很多設計不是在單一 combinational cone 內直接把 shares 混回去，而是：

• 先經過 pipeline stage 分開走，
• 再透過 forwarding / next-cycle dependency 重新交會，
• 讓單週期工具誤以為「這模組看起來乾淨」。

這篇直接把這種 deployment 級的幻覺拆掉：你以為 CLEAN，可能只是因為你的 verifier 在 register output 就停了。

作者在 Adams Bridge 上的結果很直白：MC-D1 會把 30 個 masked submodules 裡的 12 個，從單週期看似 clean，重分類成 structurally flagged。 這個結果本身就是警訊，因為它代表如果你只跑傳統 single-cycle 檢查，很多風險其實會在 verification boundary 之外被你整批漏掉。

規模是這篇真正的賣點：1.17M cells，不是玩具例子

這篇最有說服力的一點，是它不是拿幾個 toy gadgets 展示概念，而是直接上 1.17-million-cell 的 Adams Bridge ML-DSA / ML-KEM accelerator。

幾個很值得記的數字：

• 整體目標設計規模約 1,169,444 cells；
• 涵蓋 30 個 masked submodules；
• single-cycle structural analysis 在全文中報告可於約 8.7 秒 完成；
• MC-D1 在 27 個模組上的總 runtime 約 231.8 秒。

這組數字的意義，不只是「跑得快」，而是它把 pre-silicon masking review 從原本很容易卡在 exact tool scale limit 的死局，拉回一個實際可能被放進 CI / signoff pipeline 的範圍。

最實用的結果：把 363 條可疑 wires 壓成 165 條真正值得人工追的候選

如果只看 headline，我認為這篇最有營運價值的數字，是它對 5,543-cell 的 ML-KEM Barrett reduction module 做出的 triage compression。

流程大概是這樣：

• 先用 D0/D1 structural analysis 抓出 363 條 structurally flagged wires；
• 再透過四階段 pipeline 做 refinement；
• 最後把其中 198 條（54.5%）machine-verify 為 first-order secure；
• 剩下 165 條列為 candidate insecure，作為 designer triage 的 sound upper bound；
• 0 indeterminate。

這件事很重要，因為它直接把問題從「你有 363 條嫌疑線要一條條手看」變成「大概 55% 的人工 review 面積被機器先消掉，只剩 165 條高價值候選」。

對硬體安全團隊來說，這就是差別：不是 abstract correctness，而是人力終於能聚焦。

雙 solver 對齊這件事，比看起來還重要

作者另外一個我很在意的點，是對 arithmetic SADC 的結果做了 Z3 與 CVC5 雙 solver cross-validation，而且在那 363 / 363 個 query 上得到 0 disagreements。

這看起來像小事，但其實不是。因為當你把 signoff 依賴放到 SMT pipeline 上，大家最後一定會問：到底是設計有問題，還是工具 / 編碼有 bug？

雙 solver 完全一致，至少把「這只是某個 solver artifact」的疑慮壓低很多。它不能保證整個建模完全無誤，但對一篇主打 production pre-silicon evidence generation 的 paper 來說，這種 defense-in-depth 是必要的，不是裝飾。

這篇真正打中的，是 FIPS 140-3 時代的 evidence bottleneck

我覺得這篇最值得放大的 framing 是：FIPS 140-3 時代，很多 PQC 硬體團隊真正缺的，不是做出 masked design，而是做出可被審、可被重跑、可被證明的 side-channel resistance evidence。

trace-based DPA 當然重要，但那通常要等到 silicon 出來，而且只要 stimulus 選得不對，就可能 miss 掉特定 leakage。這篇的價值是在 tape-out 前先補一層結構性證據，讓團隊在還能改 RTL / netlist 的時候，就先知道哪些地方最危險。

它不是要取代 power analysis，而比較像是把 verification stack 補完整：

• pre-silicon 先用 structural + arithmetic refinement 把風險點縮小，
• post-silicon 再拿 trace-based evidence 對高風險區域做更重的驗證。

這種分工比「等晶片出來再說」成熟得多。

限制也要看清楚：這是 sound upper bound，不是最終 leakage 真相機

這篇很不錯，但我不會把它吹成萬靈丹，因為作者自己其實也講得很清楚：

• structural dependency 只是一個 sound necessary condition，不是完整 distributional security proof；
• 那 165 條 candidate insecure wires 是嚴格 over-approximation，不等於 165 條都一定真會漏；
• 目前重點在 first-order，不是高階 probing security 全部一次解完；
• 對完整大模組的 exact algebraic verification，仍然遠比這篇處理的 refinement 更重。

但我反而覺得這種定位是健康的。因為 production security tooling 真正需要的，常常不是一把梭完美，而是把原本完全做不到的事情，先拉進可操作範圍，再讓後續更重的分析接手。

我的看法

如果用一句話總結，我會說：

很多 PQC 硬體真正卡住的，不是 masking idea 想不出來，而是你根本沒辦法在硬體還沒出廠前，證明那堆 share 沒有沿著 pipeline 悄悄重新碰頭。

這篇 paper 最有價值的，不是它聲稱自己把一切都驗完，而是它非常務實地處理了兩個長期 bottleneck：

• 規模問題：把驗證拉到 1.17M cells 的 production 硬體；
• triage 問題：把一大坨 structural flags 壓成還能被 designer 真正追下去的候選集。

如果你在看 post-quantum hardware security，這篇值得收，因為它把 discussion 從「masked PQC hardware 應該安全」拉回比較成熟的問題：你能不能拿出 pre-silicon、可重跑、可對帳、足以支撐 certification 與工程決策的證據。

重點整理

• 這篇論文處理的是 PQC accelerator 的 pre-silicon masking verification，核心場景是 ML-KEM / ML-DSA 的 NTT 硬體。
• 作者指出：現有 exact masking-verification 工具多半只撐得到幾千 cells，難以直接套到 production 級 arithmetic-masked NTT 設計。
• 核心方法是四階段 hierarchy：D0/D1 structural dependency analysis → fresh-mask refinement → Boolean SADC → arithmetic SADC。
• 這套方法的目的不是一開始就做完整 exact proof，而是先用 sound-but-incomplete 的 structural test 抓出可能危險區，再逐步 refinement。
• 論文特別補上 MC-D1，把單週期看不到的跨 register / multi-cycle share convergence 納入分析。
• 在 1.17-million-cell 的 Adams Bridge ML-KEM / ML-DSA accelerator 上，structural analysis 可在秒級完成，MC-D1 可在數分鐘內跑完整體模組集。
• MC-D1 會把原本單週期看似 clean 的 12 個模組 重分類為 structurally flagged，凸顯只看 single-cycle 會漏掉實際風險。
• 在 5,543-cell 的 ML-KEM Barrett reduction module 上，四階段 pipeline 把 363 條 flagged wires 中的 198 條（54.5%）機器驗證為 secure，剩下 165 條列為 candidate insecure，且 0 indeterminate。
• Z3 與 CVC5 對全部 363 個 query 給出 0 disagreements，強化了結果的可信度。
• 這篇真正的價值，是把 masked PQC hardware 的 side-channel evidence generation 從學術尺度，推向比較像 production signoff 與 FIPS 140-3 前置準備的工程尺度。

Takeaway

這篇論文最值得記住的，不是它又發現幾條有問題的 wires，而是它提醒我們：在 post-quantum 硬體時代，安全瓶頸往往不在「有沒有做 masking」，而在「你能不能在晶片做出來前，拿出足夠可信、足夠大規模、足夠可重現的證據，說服自己和別人這套 masking 沒有在實作裡悄悄失真」。

而這篇做的，就是把那條證據鏈往前推了一大步。