pith. sign in

arxiv: 2604.15249 · v2 · submitted 2026-04-16 · 💻 cs.CR

Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

Ray Iskander , Khaled Kirah This is my paper

Pith reviewed 2026-05-10 10:34 UTC · model grok-4.3

classification 💻 cs.CR
keywords post-quantum cryptographyside-channel verificationmaskingML-KEMhardware acceleratorsstructural analysisSADCNTT
0
0 comments X

The pith

A four-stage pipeline scales first-order masking verification to million-cell ML-KEM and ML-DSA accelerators.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a verification hierarchy that starts with structural dependency analysis to flag potential leakage paths in masked hardware, then refines masks and applies Boolean and arithmetic single-authentication distance checks to confirm security. This extends exact verification beyond the few-thousand-cell limit of prior tools to full production modules such as the 1.17-million-cell Adams Bridge accelerator and its 5,543-cell Barrett reduction submodule. On that submodule the pipeline classifies 198 of 363 flagged wires as secure, leaves 165 for designer review as a sound upper bound, and produces zero indeterminate cases, with every verdict agreed by two independent SMT solvers. The approach matters for FIPS 140-3 certification because post-quantum accelerators must demonstrate side-channel resistance at scale, where exhaustive manual inspection is infeasible.

Core claim

The paper claims that D0/D1 structural dependency analysis combined with fresh-mask refinement, Boolean SADC, and arithmetic SADC forms a sound and complete first-order masking verification pipeline for masked NTT and arithmetic modules; when run on the 5,543-cell ML-KEM Barrett reduction module it machine-verifies 198 of 363 structurally flagged wires as secure, reports the remaining 165 as candidate insecure wires, leaves zero wires indeterminate, and obtains identical verdicts from Z3 and CVC5 across all 363 wires.

What carries the argument

The D0/D1 structural dependency analysis that identifies all candidate first-order leakage paths before SADC confirmation.

If this is right

  • Structural analysis finishes in seconds across all 30 masked submodules of the 1.17-million-cell accelerator.
  • The multi-cycle D1 extension reclassifies 12 modules from structurally clean to flagged, capturing sequential dependencies.
  • Manual review effort shrinks from hundreds of structural flags to 165 actionable candidates with mathematical certificates.
  • The pipeline applies uniformly to both NTT and arithmetic modules in masked ML-KEM and ML-DSA implementations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same staged approach could be adapted to verify masking in other post-quantum algorithms or higher-order masking schemes.
  • Routine use in hardware design flows would allow earlier detection of leakage issues before tape-out.
  • Zero indeterminate cases on the tested module suggests the hierarchy is decisive for typical arithmetic datapaths, though larger or more irregular designs would still need empirical checks.

Load-bearing premise

The D0/D1 structural dependency analysis must correctly and completely identify every potential first-order leakage path without missing any dependencies or producing false negatives.

What would settle it

Discovery of a first-order leakage in any wire the pipeline classifies as secure inside the ML-KEM Barrett reduction module, or any disagreement between Z3 and CVC5 on the 363 verdicts.

Figures

Figures reproduced from arXiv: 2604.15249 by Khaled Kirah, Ray Iskander.

Figure 1
Figure 1. Figure 1: Label lattice L = {⊥, S₀, S₁, BOTH} for first-order (d = 1) structural dependency analysis. 3.1. Problem Statement Consider a first-order masking scheme where a secret value s is split into two shares s_0 and s_1 such that s = s_0 ⊕ s_1 (Boolean masking) or s = (s_0 + s_1) mod q (arithmetic masking). Under the standard probing model [7], a circuit is first-order probing secure if an adversary observing any… view at source ↗
Figure 2
Figure 2. Figure 2: Module classification under single-cycle (SC-D1) and multi-cycle (MC-D1) structural dependency analysis. MC-D1 reclassifies 12 CLEAN modules as INSECURE. SC-D1 identifies 59,061 structurally insecure wires across the 27 completed modules in 8.7 seconds total.1 [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: Decomposition of 614,126 MC-D1 insecure wires by root-cause category [PITH_FULL_IMAGE:figures/full_fig_p019_4.png] view at source ↗
read the original abstract

Post-quantum cryptographic (PQC) accelerators implementing ML-KEM (FIPS 203) and ML-DSA (FIPS 204) require side-channel resistance evidence for FIPS 140-3 certification. However, exact masking-verification tools scale only to gadgets of a few thousand cells. We present a four-stage verification hierarchy, D0/D1 structural dependency analysis, fresh-mask refinement, Boolean Single-Authentication Distance Checking (SADC), and arithmetic SADC, that extends sound first-order masking verification to production arithmetic modules. Applied to the 1.17-million-cell Adams Bridge ML-DSA/ML-KEM accelerator, structural analysis completes in seconds across all 30 masked submodules. A multi-cycle extension (MC-D1) reclassifies 12 modules from structurally clean to structurally flagged. On the 5,543-cell ML-KEM Barrett reduction module, the pipeline machine-verifies 198 of 363 structurally flagged wires (54.5%) as first-order secure, reports 165 as candidate insecure for designer triage (a sound upper bound), and leaves 0 indeterminate. Every verdict is cross validated by Z3 and CVC5 with 0 disagreements across 363 wires. The result narrows manual review from hundreds of structural flags to 165 actionable candidates with mathematical certificates, enabling pre-silicon side-channel evidence generation on production ML-KEM hardware.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper proposes a four-stage verification hierarchy (D0/D1 structural dependency analysis, fresh-mask refinement, Boolean SADC, and arithmetic SADC) for scalable first-order masking verification of post-quantum cryptographic accelerators. Applied to the 1.17-million-cell Adams Bridge ML-DSA/ML-KEM design, structural analysis runs in seconds on all 30 submodules; on the 5,543-cell Barrett reduction module the pipeline verifies 198 of 363 flagged wires as secure, reports 165 as insecure candidates, and leaves zero indeterminate, with every verdict agreed by Z3 and CVC5.

Significance. If the D0/D1 analysis is complete, the work provides a practical route to pre-silicon side-channel evidence for production-scale masked PQC hardware required for FIPS 140-3. Notable strengths are the machine-checked cross-validation on 363 wires with zero solver disagreements, the multi-cycle MC-D1 extension, and the reduction of manual review to a sound upper bound of 165 candidates.

major comments (1)
  1. [Abstract] Abstract: the claim that the pipeline machine-verifies 198 wires as first-order secure and supplies a sound upper bound on the remaining 165 rests on the unproven completeness of D0/D1 structural dependency analysis. No formal definition, inductive argument, or exhaustive check on a toy masked arithmetic gadget is supplied to show that every first-order leakage path (including carry propagation and modular-reduction interactions) is captured; a missed dependency would leave an insecure wire unflagged and implicitly treated as secure.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback on the completeness of our D0/D1 analysis. We address the concern directly below and will strengthen the manuscript accordingly.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the pipeline machine-verifies 198 wires as first-order secure and supplies a sound upper bound on the remaining 165 rests on the unproven completeness of D0/D1 structural dependency analysis. No formal definition, inductive argument, or exhaustive check on a toy masked arithmetic gadget is supplied to show that every first-order leakage path (including carry propagation and modular-reduction interactions) is captured; a missed dependency would leave an insecure wire unflagged and implicitly treated as secure.

    Authors: We agree that an explicit formal argument would strengthen the presentation. D0/D1 computes the transitive closure over the gate-level netlist's structural dependencies, which by definition includes all combinational paths, carry propagations, and modular-reduction interactions; any first-order leakage path must therefore appear as a dependency flag. This makes the set of 165 candidates a sound upper bound: missed flags can only enlarge the triage set, never cause an insecure wire to be declared secure. To address the referee's point directly, the revised manuscript will add (1) a formal definition of the D0/D1 relations, (2) a short inductive argument establishing completeness for both combinational and sequential logic, and (3) an exhaustive verification on a toy masked arithmetic gadget (e.g., 4-bit masked adder) confirming all leakage paths are captured. These additions will be placed in a new subsection of Section 3. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation chain is self-contained and externally validated

full rationale

The paper defines a four-stage hierarchy (D0/D1 structural analysis, fresh-mask refinement, Boolean SADC, arithmetic SADC) and applies it directly to an external 1.17-million-cell Adams Bridge accelerator. On the 5543-cell Barrett module it reports machine-verified secure/insecure classifications for all 363 flagged wires, with every verdict cross-checked by independent external solvers Z3 and CVC5 showing zero disagreements. No equations reduce to fitted parameters, no predictions are constructed from the same data used to define the method, and no load-bearing claims rest on self-citations or prior results by the same authors. The derivation therefore remains independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claim rests on the domain assumption that structural dependency analysis plus SADC soundly captures first-order masking security for arithmetic NTT modules; no free parameters are introduced and the invented stages are the method itself.

axioms (1)
  • domain assumption First-order masking security of arithmetic modules can be reduced to structural dependency checks followed by Boolean and arithmetic single-authentication distance verification
    Invoked to justify the four-stage pipeline as a sound extension of prior small-gadget verification.
invented entities (2)
  • D0/D1 structural dependency analysis no independent evidence
    purpose: Rapid pre-filter to identify candidate leakage paths in masked hardware
    New stage that enables scaling beyond prior tool limits
  • Boolean SADC and arithmetic SADC no independent evidence
    purpose: Solver-based machine verification of security for flagged wires
    Core verification techniques introduced in the hierarchy

pith-pipeline@v0.9.0 · 5553 in / 1463 out tokens · 60755 ms · 2026-05-10T10:34:00.051004+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 7 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

    cs.CR 2026-04 accept novelty 8.0 partial

    Machine-checked Lean proofs show that fresh inter-stage masking in prime-field PINI gadgets erases prior multiplicity, satisfying only the second gadget's security parameter.

  2. Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

    cs.CR 2026-04 unverdicted novelty 8.0

    Machine-checked Lean 4 proofs establish PF-PINI composition theorems for prime-field arithmetic masking, showing fresh inter-stage masks erase prior security parameters and diagnosing non-uniformity in Microsoft's Ada...

  3. Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

    cs.CR 2026-04 accept novelty 8.0 full

    Machine-checked proofs establish that fresh per-stage masking in Cooley-Tukey NTT pipelines over Z/qZ yields per-context uniformity at every stage under the ISW first-order probing model.

  4. From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

    cs.CR 2026-04 accept novelty 8.0 full

    A Lean 4 formalization proves that value-independence implies identical marginal distributions for masking verification across all positive integers q.

  5. Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis

    cs.CR 2026-04 conditional novelty 8.0

    Strategic masking of three consecutive mid-layers in NTT hardware defeats soft-analytical side-channel attacks with only 43% overhead while single-layer masking plus shuffling falls short of claimed 2^46–2^96 margins.

  6. The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

    cs.CR 2026-05 conditional novelty 7.0 full

    Arbitrary-depth k-stage masked NTT pipelines with fresh inter-stage masking and PF-PINI(≤2) gadgets satisfy a universal 2/q per-observation leakage bound, machine-checked in Lean 4.

  7. Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

    cs.CR 2026-04 unverdicted novelty 6.0 partial

    Barrett reduction's masked internal map has preimage sizes in {0,1,2}, establishing a universal 1-bit leakage barrier, with the trichotomy and PF-PINI properties machine-checked in Lean 4.

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages · cited by 6 Pith papers · 1 internal anchor

  1. [1]

    title Post-quantum cryptography standards: FIPS 203, 204, 205

    The National Institute of Standards and Technology, U.S. Department of Commerce, "Module-Lattice- Based Key-Encapsulation Mechanism Standard," NIST Federal Information Processing Standards (FIPS) 203," doi: 10.6028/NIST.FIPS.203, 2024

    work page doi:10.6028/nist.fips.203 2024

  2. [2]

    Module-Lattice-Based Digital Signature Standard (ML-DSA),

    S. U. D. o. C. The National Institute of Standards and Technology, "Module-Lattice-Based Digital Signature Mechanism," NIST Federal Information Processing Standards (FIPS) 204," doi: org/10.6028/NIST.FIPS.204, 2024

    work page doi:10.6028/nist.fips.204 2024

  3. [3]

    SILVER – Statistical Independence and Leakage Structural Dependency Analysis for Masked NTT Hardware 35 Verification,

    David Knichel, Pascal Sasdrich, Amir Moradi, "SILVER – Statistical Independence and Leakage Structural Dependency Analysis for Masked NTT Hardware 35 Verification," in ASIACRYPT 2020 , Daejeon, South Korea (Virtual), 2020

    work page 2020

  4. [4]

    maskVerif: Automated verification of higher-order masking in presence of physical defaults,

    Gilles Barthe, Sonia Belaid, Gaetan Cassiers, Pierre-Alain Fouque, Benjamin Gregoire, Francois-Xavier Standaert, "maskVerif: Automated verification of higher-order masking in presence of physical defaults," in European Symposium on Research in Computer Security, Luxembourg, 2019

    work page 2019

  5. [5]

    Prover - Toward More Efficient Formal Verification of Masking in Probing Model,

    Feng Zhou, Hua Chen, Limin Fan, "Prover - Toward More Efficient Formal Verification of Masking in Probing Model," IACR Transactions on Cryptographic Hardware and Embedded Systems , vol. 1, pp. 552- 585, 2025, DOI:10.46586/tches.v2025.i1.552-585

    work page doi:10.46586/tches.v2025.i1.552-585 2025

  6. [6]

    Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs,

    B. Gigerl, V. Hadzic, R. Primas, S. Mangard, and R. Bloem, "Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs," in Proc. USENIX Security, 2021

    work page 2021

  7. [7]

    Private circuits: Securing hardware against probing attacks,

    Y. Ishai, A. Sahai, D. Wagner, "Private circuits: Securing hardware against probing attacks," in CRYPTO 2003

    work page 2003

  8. [8]

    https://dictionary.cambridge.org/dictionary/english/canary-in-a-coalmine,

    "https://dictionary.cambridge.org/dictionary/english/canary-in-a-coalmine," Cambridge Dictionary, April

    work page

  9. [9]

    Side-Channel Attack on Adams Bridge,

    E. Karabulut and R. Azarderakhsh, "Side-Channel Attack on Adams Bridge," in Cryptology ePrint Archive, Report 2025/009. In Proc. IEEE International Symposium on Hardware Oriented Security and Trust (HOST), 2025

    work page 2025

  10. [10]

    Analysis of Adams Bridge masking,

    M.-J. O. Saarinen, "Analysis of Adams Bridge masking," in Hardwear.io USA 2025

    work page 2025

  11. [11]

    Adams Bridge Accelerator: Bridging the Post-Quantum Transition,

    M. Bisheh-Niasar, E. Karabulut, B. Upadhyayula, A. Norris, and L. Pillilli, "Adams Bridge Accelerator: Bridging the Post-Quantum Transition," Cryptology ePrint Archive, Report 2026/256, 2026

    work page 2026

  12. [12]

    Strong non-interference and type-directed higher-order masking,

    Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, and Rébecca Zucchini, "Strong non-interference and type-directed higher-order masking," in 23rd ACM Conference on Computer and Communications Security, Hofburg Palace, Vienna, Austria, 2016

    work page 2016

  13. [13]

    Formal verification of masked hardware implementations in the presence of glitches,

    R. Bloem, H. Groß, R. Iusupov, B. Könighofer, S. Mangard, J. Winter, "Formal verification of masked hardware implementations in the presence of glitches," in EUROCRYPT, 2018

    work page 2018

  14. [14]

    ProverNG: Efficient verification of compositional masking for cryptosystem’s side-channel security,

    Y. Yang, F. Zhou, Y. Wang, H. Chen, L. Fan, A. Wang, "ProverNG: Efficient verification of compositional masking for cryptosystem’s side-channel security," in ICICS 2025, LNCS 16219, pp. 57–76. Springer, Singapore, 2026

    work page 2025

  15. [15]

    IronMask: Versatile Verification of Masking Security,

    S. Belaïd, D. Mercadier, M. Rivain, and A. R. Taleb, "IronMask: Versatile Verification of Masking Security," Cryptology ePrint Archive, paper 2021/1671, 2021

    work page 2021

  16. [16]

    VerMI: Verification tool for masked implementations,

    V. Arribas, S. Nikova, and V. Rijmen, "VerMI: Verification tool for masked implementations," in ICECS 2018, Bordeaux, France

    work page 2018

  17. [17]

    INDIANA — Verifying (random) probing security through indistinguishability analysis,

    C. Beierle, J. Feldtkeller, A. Guinet, T. Güneysu, G. Leander, J. Richter-Brockmann, P. Sasdrich, "INDIANA — Verifying (random) probing security through indistinguishability analysis," EUROCRYPT 2025, LNCS 15608, pp. 33–63. ePrint 2024/833

    work page 2025

  18. [18]

    CocoAlma: A Versatile Masking Verifier,

    Vedad Hadžić and Roderick Bloem, "CocoAlma: A Versatile Masking Verifier," in 21st Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), 2021

    work page 2021

  19. [19]

    COCO: Co-Design and Co-Verification of Masked Software Implementations on CPUs,

    B. Gigerl, V. Hadzic, R. Primas, S. Mangard, Roderick Bloem , "COCO: Co-Design and Co-Verification of Masked Software Implementations on CPUs," in 30th USENIX Security Symposium , Vancouver, B.C., Canada, 2021

    work page 2021

  20. [20]

    PROLEAD: A Probing-Based Hardware Leakage Detection Tool,

    N. Müller, A. Moradi, "PROLEAD: A Probing-Based Hardware Leakage Detection Tool," IACR Transactions on Cryptographic Hardware and Embedded Systems, vol. 4, pp. 311-348, 2022. https://doi.org/10.46586/tches.v2022.i4.311-348

    work page doi:10.46586/tches.v2022.i4.311-348 2022

  21. [21]

    aLEAKator: HDL mixed-domain simulation for masked hardware and software formal verification,

    N. Amiot, Q. L. Meunier, K. Heydemann, E. Encrenaz, "aLEAKator: HDL mixed-domain simulation for masked hardware and software formal verification," ePrint 2025/2193, 2025

    work page 2025

  22. [22]

    MATCHI: Compositional verification of Hardware Private Circuit designs,

    G. Cassiers, "MATCHI: Compositional verification of Hardware Private Circuit designs," ePrint 2025

    work page 2025

  23. [23]

    Compositional Security of Masked Hardware Implementations,

    G. Cassiers, C. Momin, and F.-X. Standaert, "Compositional Security of Masked Hardware Implementations," in IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES), Structural Dependency Analysis for Masked NTT Hardware 36 Volume 2021, Issue 4

    work page 2021

  24. [24]

    Tight private circuits: Achieving probing security with the least refreshing,

    S. Belaïd, D. Goudarzi, M. Rivain, "Tight private circuits: Achieving probing security with the least refreshing," in ASIACRYPT 2018, Brisbane, Australia

    work page 2018

  25. [25]

    On the power of expansion: More efficient constructions in the random probing model,

    S. Belaïd, M. Rivain, A.R. Taleb, "On the power of expansion: More efficient constructions in the random probing model," in EUROCRYPT 2021

    work page 2021

  26. [26]

    Formal verification of side-channel countermeasures via elementary circuit transformations (CheckMasks),

    J.-S. Coron , "Formal verification of side-channel countermeasures via elementary circuit transformations (CheckMasks)," in ACNS 2018

    work page 2018

  27. [27]

    Tornado: Automatic generation of probing-secure masked bitsliced implementations,

    S. Belaïd, P.-E. Dagand, D. Mercadier, M. Rivain, R. Wintersdorff, "Tornado: Automatic generation of probing-secure masked bitsliced implementations," in EUROCRYPT 2020

    work page 2020

  28. [28]

    A sound method for switching between Boolean and arithmetic masking,

    L. Goubin, "A sound method for switching between Boolean and arithmetic masking," in CHES 2001

    work page 2001

  29. [29]

    Conversion from arithmetic to Boolean masking with logarithmic complexity,

    J.-S. Coron, J. Großschädl, P.K. Vadnala, M. Tibouchi, "Conversion from arithmetic to Boolean masking with logarithmic complexity," in FSE 2015

    work page 2015

  30. [30]

    Formal verification of arithmetic masking,

    B. Gigerl, R. Primas, S. Mangard, "Formal verification of arithmetic masking," in ACNS 2023 (ePrint 2022/849)

    work page 2023

  31. [31]

    eVer: Universal and automated verification of side-channel security for additive, inner product, polynomial and general code-based masking,

    M. Gourjon, M. Orlt, P. Pauls, A. Treff, "eVer: Universal and automated verification of side-channel security for additive, inner product, polynomial and general code-based masking," ePrint 2026/208

    work page 2026

  32. [32]

    VERICA — Verification of combined attacks: Automated formal verification of security against simultaneous faults and probes,

    J. Richter-Brockmann, J. Feldtkeller, P. Sasdrich, T. Güneysu, "VERICA — Verification of combined attacks: Automated formal verification of security against simultaneous faults and probes," in TCHES 2022

    work page 2022

  33. [33]

    Prime-field masking in hardware and its soundness against low-noise SCA attacks,

    G. Cassiers, L. Masure, C. Momin, T. Moos, F.-X. Standaert , "Prime-field masking in hardware and its soundness against low-noise SCA attacks," in TCHES 2023

    work page 2023

  34. [34]

    Mangard, E

    S. Mangard, E. Oswald, T. Popp, Power Analysis Attacks: Revealing the Secrets of Smart Cards, Springer, 2007

    work page 2007

  35. [35]

    On the Cost of Lazy Engineering for Masked Software Implementations,

    J. Balasch, B. Gierlichs, V. Grosso, O. Reparaz, F.-X. Standaert, "On the Cost of Lazy Engineering for Masked Software Implementations," in proceedings of CARDIS 2014

    work page 2014

  36. [36]

    Domain-Oriented Masking: Compromising Security for Each and Every Clock Cycle?,

    H. Groß, S. Mangard, and T. Korak, "Domain-Oriented Masking: Compromising Security for Each and Every Clock Cycle?," in 18th International Conference on Cryptographic Hardware and Embedded Systems (CHES 2016)

    work page 2016

  37. [37]

    sv2v: SystemVerilog to Verilog conversion,

    Z. Miri, "sv2v: SystemVerilog to Verilog conversion," in GitHub, 2019. Available: https://github.com/zachjs/sv2v

    work page 2019

  38. [38]

    Yosys Open SYnthesis Suite,

    C. Wolf, "Yosys Open SYnthesis Suite," in 2016. Available: https://yosyshq.net/yosys/

    work page 2016

  39. [39]

    Z3: An efficient SMT solver,

    L. de Moura, N. Bjørner, "Z3: An efficient SMT solver," in TACAS 2008

    work page 2008

  40. [40]

    A unified approach to global program optimization,

    G. Kildall, "A unified approach to global program optimization," in POPL , 1973

    work page 1973

  41. [41]

    Monotone data flow analysis frameworks,

    J.B Kam, J.D. Ullman, "Monotone data flow analysis frameworks," Acta Informatica,, vol. 7, no. 3, p. 305– 317, 1977

    work page 1977

  42. [42]

    Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis

    R. Iskander, K. Kirah, "Partial Number Theoretic Transform Masking in Post Quantum Cryptography Hardware: A Security Margin Analysis," arXiv:2604.03813, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  43. [43]

    Efficient CPA Attack on Hardware Implementation of ML-DSA in Post- Quantum Root of Trust,

    M. Karabulut, R. Azarderakhsh, "Efficient CPA Attack on Hardware Implementation of ML-DSA in Post- Quantum Root of Trust," Cryptology ePrint Archive, 2025/009, 2025

    work page 2025

  44. [44]

    Single-trace side-channel attacks on masked lattice-based encryption,

    R. Primas, P. Pessl, S. Mangard, "Single-trace side-channel attacks on masked lattice-based encryption," in CHES 2017

    work page 2017

  45. [45]

    On exploiting message leakage in (few) NIST PQC candidates for practical message recovery and key recovery attacks,

    P. Ravi, S. Bhasin, S. Sinha Roy, A. Chattopadhyay, "On exploiting message leakage in (few) NIST PQC candidates for practical message recovery and key recovery attacks," IEEE T-IFS, 2022. (ePrint 2020/1559.)

    work page 2022