pith. sign in

arxiv: 2605.25728 · v1 · pith:7K6DRG74new · submitted 2026-05-25 · 🪐 quant-ph

Q-LEAK: Quantum-Based LEAKage Verification for Side-Channel Countermeasures

Walid El Maouaki , Alberto Marchisio , Muhammad Shafique This is my paper

Pith reviewed 2026-06-29 21:37 UTC · model grok-4.3

classification 🪐 quant-ph
keywords quantum verificationside-channel leakageGrover algorithmSAT solvingcryptographic countermeasuresamplitude amplificationtwo-trace leakageCNF encoding
0
0 comments X

The pith

Q-LEAK encodes two-trace leakage conditions as CNF formulas and uses Grover amplitude amplification to recover satisfying assignments for side-channel verification.

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

The paper builds compact CNF representations that capture one-bit power leakage under two-trace conditions for XOR-heavy cryptographic circuits. Classical SAT solvers reach their limits on these time-unrolled designs, so the work compiles each CNF into a quantum oracle. Grover's algorithm then performs amplitude amplification to locate satisfying bitstrings in square-root time. Noiseless simulations on 5-7 variable benchmarks recover valid assignments in 1-4 iterations with marked probabilities above 20 percent. Execution on real quantum hardware still yields at least one assignment that classical solvers confirm as correct despite noise.

Core claim

Q-LEAK compiles the two-trace leakage predicate and CNF constraints into a quantum oracle, then applies amplitude amplification to search for satisfying assignments. In noiseless tests the procedure recovers a satisfying assignment within 1-4 tries and amplifies the marked bitstrings above 20 percent probability. On real hardware the same procedure returns at least one assignment that a classical SAT solver independently verifies as correct.

What carries the argument

The quantum oracle that directly encodes the two-trace leakage predicate together with the CNF constraints, enabling amplitude amplification to mark and boost satisfying assignments.

If this is right

  • Grover search reduces oracle calls from linear in the search space to square-root scaling.
  • The approach succeeds on instances where classical SAT solvers hit complexity walls.
  • Real hardware execution can still produce assignments that pass classical verification.
  • The method targets verification of side-channel countermeasures in cryptographic algorithms.

Where Pith is reading between the lines

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

  • If oracle size stays manageable, the technique could scale verification to circuit sizes beyond current classical reach.
  • Hardware noise did not eliminate all useful output, suggesting tolerance to moderate decoherence may be feasible.
  • Hybrid workflows that feed quantum-found candidates back into classical checkers could become practical for security analysis.
  • Larger problem sizes would require testing whether the encoding overhead remains sub-exponential in the number of state bits.

Load-bearing premise

The two-trace leakage predicate and CNF constraints can be encoded into a quantum oracle without prohibitive growth in qubit count or circuit depth for realistic cryptographic circuits.

What would settle it

A benchmark with more than ten variables where the required oracle depth exceeds hardware coherence time and no classically verified satisfying assignment appears after repeated runs.

Figures

Figures reproduced from arXiv: 2605.25728 by Alberto Marchisio, Muhammad Shafique, Walid El Maouaki.

Figure 1
Figure 1. Figure 1: Cryptographic algorithm is implemented as a cipher in hardware, [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Asymptotic scaling of search cost versus the number of variables [PITH_FULL_IMAGE:figures/full_fig_p001_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Overview of the main contributions of Q-LEAK. Green boxes highlight [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Q-LEAK framework. Compile the protected cipher and BIT model into a two-trace, [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Circuit sketch for SAT-oracle building blocks. [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Q-LEAK results on power side-channel CNF benchmarks. Four CNF cases are plotted (a) number of variables [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Hardware evaluation of Q-LEAK on ibm_marrakesh (156 qubits). Measured bitstring probabilities for (a) case 1 and (b) case 2. Red stems mark candidate SAT assignments; ✓ indicates classically verified solutions (11100, 101101), × marks spurious peaks (11000, 011100) attributed to noise. Green stems show the UNSAT-like background. Results are averaged over 5 runs. case 2 (Fig. 7b). In both cases, one correct… view at source ↗
Figure 8
Figure 8. Figure 8: Projected hard-instance threshold for Q-LEAK oracle-weighted [PITH_FULL_IMAGE:figures/full_fig_p009_8.png] view at source ↗
read the original abstract

Formal verification of power side-channel leakage and its countermeasures in cryptographic algorithms is challenging, as SAT-based methods fail to scale on XOR-heavy, time-unrolled cryptographic circuits with realistic leakage models. We construct compact Conjunctive Normal Form (CNF) cases modeling one-bit leakage under two-trace conditions, linking key dependence and state evolution. Classical solvers quickly reach complexity limits, so we propose Q-LEAK, a quantum-based verification approach using Grover's algorithm, compiling each CNF into an oracle and applying amplitude amplification to search in O(sqrt(N)) oracle calls, with oracles that encode the two-trace leakage predicate and the CNF constraints. Benchmarking against classical SAT shows both potential gains and practical resource limits. In noiseless tests on 5-7 variable benchmarks, Q-LEAK consistently recovered a satisfying assignment within 1-4 tries, with marked bitstrings amplified clearly above the background distribution, exceeding 20 percent probability. The evaluation of Q-LEAK on real quantum hardware revealed at least one classically verified SAT assignment, despite the presence of noise. These results point to a potential path toward quantum-assisted verification of side-channel protections.

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

3 major / 1 minor

Summary. The paper proposes Q-LEAK, a quantum-assisted method for verifying one-bit power side-channel leakage under two-trace conditions in cryptographic circuits. It encodes the leakage predicate together with CNF constraints into a quantum oracle and applies Grover amplitude amplification to search for satisfying assignments in O(√N) oracle calls. On 5-7 variable noiseless benchmarks the method recovers a satisfying assignment in 1-4 iterations with marked bitstrings exceeding 20% probability; a limited hardware run on real quantum hardware also recovers at least one classically verified assignment. The work positions the approach as a route past the scaling limits of classical SAT solvers on XOR-heavy, time-unrolled circuits.

Significance. A working quantum-oracle encoding that remains compact for realistic cryptographic sizes would supply a quadratic speedup for a practically relevant verification task. The small-scale noiseless and hardware demonstrations are concrete evidence that the basic idea is realizable on current devices, but the absence of any resource scaling data prevents assessment of whether the claimed advantage can ever be realized beyond toy instances.

major comments (3)
  1. [Abstract and benchmarking section] Abstract and benchmarking section: the reported success is confined to 5-7 variable instances; no qubit counts, circuit depths, or growth rates versus number of variables or unrolling depth are supplied, leaving the central practicality claim for realistic cryptographic circuits unsupported.
  2. [Oracle-construction description] Oracle-construction description (implicit in §3 and the method outline): the paper asserts that the two-trace leakage predicate plus CNF constraints compile to a compact oracle, yet supplies neither an explicit construction nor an asymptotic resource analysis; without this the O(√N) claim cannot be evaluated.
  3. [Hardware-evaluation paragraph] Hardware-evaluation paragraph: the claim that “at least one classically verified SAT assignment” was recovered is presented without error bars, shot counts, or noise-model analysis, making it impossible to judge whether the 20% probability figure survives realistic device noise.
minor comments (1)
  1. The phrase “practical resource limits” appears without any accompanying table or formula that would allow a reader to reproduce the limit.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. We address each major point below and indicate the revisions made to strengthen the presentation of our results and claims.

read point-by-point responses

  1. Referee: [Abstract and benchmarking section] Abstract and benchmarking section: the reported success is confined to 5-7 variable instances; no qubit counts, circuit depths, or growth rates versus number of variables or unrolling depth are supplied, leaving the central practicality claim for realistic cryptographic circuits unsupported.

    Authors: We agree that the reported results are limited to 5-7 variable instances and that explicit resource metrics would better contextualize the work. The benchmarking section has been revised to report qubit counts and circuit depths for these cases. We have also added a discussion of expected scaling trends derived from the CNF encoding structure. Full growth rates for realistic cryptographic unrolling depths remain outside the scope of the current small-scale demonstration, which focuses on feasibility where classical SAT already encounters difficulties. revision: partial

  2. Referee: [Oracle-construction description] Oracle-construction description (implicit in §3 and the method outline): the paper asserts that the two-trace leakage predicate plus CNF constraints compile to a compact oracle, yet supplies neither an explicit construction nor an asymptotic resource analysis; without this the O(√N) claim cannot be evaluated.

    Authors: We acknowledge that an explicit construction and resource analysis would allow better evaluation of the O(√N) claim. Section 3 has been expanded with a detailed, step-by-step description of how the two-trace leakage predicate and CNF constraints are compiled into the oracle circuit. An asymptotic analysis has also been added, showing that oracle size and depth scale linearly with the number of variables and clauses, thereby preserving the quadratic query advantage of Grover's algorithm. revision: yes

  3. Referee: [Hardware-evaluation paragraph] Hardware-evaluation paragraph: the claim that “at least one classically verified SAT assignment” was recovered is presented without error bars, shot counts, or noise-model analysis, making it impossible to judge whether the 20% probability figure survives realistic device noise.

    Authors: We agree that additional experimental details are needed for proper assessment. The hardware-evaluation paragraph has been revised to report the shot counts (1024 per circuit), error bars obtained from repeated runs, and a comparison against a simple depolarizing noise model. These additions show that the observed probability amplification for marked states remains distinguishable from background noise in the reported experiments. revision: yes

Circularity Check

0 steps flagged

No significant circularity; new quantum encoding proposal tested on external classical SAT benchmarks

full rationale

The paper introduces Q-LEAK as a novel application of Grover's algorithm to side-channel verification by encoding leakage predicates into CNF oracles. The central claims rely on standard quantum amplitude amplification and empirical benchmarking against classical solvers on small instances (5-7 variables), without reducing any prediction to fitted parameters or self-referential definitions. No self-citations are used to justify uniqueness or load-bearing premises, and the derivation chain is independent of the target results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard quantum computing results and modeling choices for leakage; no free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • standard math Grover's algorithm provides quadratic speedup via amplitude amplification for unstructured search problems
    Invoked to achieve O(sqrt(N)) oracle calls for finding satisfying assignments in the leakage CNF.

pith-pipeline@v0.9.1-grok · 5737 in / 1364 out tokens · 31547 ms · 2026-06-29T21:37:31.804667+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

32 extracted references · 4 canonical work pages · 2 internal anchors

  1. [1]

    The em side—channel (s),

    D. Agrawal, B. Archambeault, J. R. Rao, and P. Rohatgi, “The em side—channel (s),” inInternational workshop on cryptographic hardware and embedded systems. Springer, 2002, pp. 29–45

    2002

  2. [2]

    A survey of microarchitectural side-channel vulnerabilities, attacks, and defenses in cryptography,

    X. Lou, T. Zhang, J. Jiang, and Y . Zhang, “A survey of microarchitectural side-channel vulnerabilities, attacks, and defenses in cryptography,”ACM Computing Surveys (CSUR), vol. 54, no. 6, pp. 1–37, 2021

    2021

  3. [3]

    Systematic classification of side-channel attacks: A case study for mobile devices,

    R. Spreitzer, V . Moonsamy, T. Korak, and S. Mangard, “Systematic classification of side-channel attacks: A case study for mobile devices,” IEEE communications surveys & tutorials, vol. 20, no. 1, pp. 465–488, 2017

    2017

  4. [4]

    A survey of side-channel attacks on caches and countermeasures,

    Y . Lyu and P. Mishra, “A survey of side-channel attacks on caches and countermeasures,”Journal of Hardware and Systems Security, vol. 2, no. 1, pp. 33–50, 2018

    2018

  5. [5]

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

    J.-S. Coron, “Formal verification of side-channel countermeasures via elementary circuit transformations,” inInternational Conference on Applied Cryptography and Network Security. Springer, 2018, pp. 65–82

    2018

  6. [6]

    Formal verification of software countermeasures against side-channel attacks,

    H. Eldib, C. Wang, and P. Schaumont, “Formal verification of software countermeasures against side-channel attacks,”ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 24, no. 2, pp. 1–24, 2014

    2014

  7. [7]

    Minisat-a sat solver with conflict-clause minimization,

    N. Een, “Minisat-a sat solver with conflict-clause minimization,”Proc. Theory and Applications of Satisfiability Testing (SAT 05), 2005

    2005

  8. [8]

    Cryptominisat switches-optimization for solving cryptographic instances,

    A.-M. Leventi-Peetz, O. Zendel, W. Lennartz, and K. Weber, “Cryptominisat switches-optimization for solving cryptographic instances,” arXiv preprint arXiv:2112.11484, 2021

    work page arXiv 2021

  9. [9]

    Smt-based verification of software countermeasures against side-channel attacks,

    H. Eldib, C. Wang, and P. Schaumont, “Smt-based verification of software countermeasures against side-channel attacks,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2014, pp. 62–77

    2014

  10. [10]

    Side channel attacks and countermeasures,

    K. Mai, “Side channel attacks and countermeasures,” inIntroduction to hardware security and trust. Springer, 2011, pp. 175–194

    2011

  11. [11]

    Differential power analysis,

    P. Kocher, J. Jaffe, and B. Jun, “Differential power analysis,” inAnnual international cryptology conference. Springer, 1999, pp. 388–397

    1999

  12. [12]

    Examining smart-card security under the threat of power analysis attacks,

    T. S. Messerges, E. A. Dabbish, and R. H. Sloan, “Examining smart-card security under the threat of power analysis attacks,”IEEE transactions on computers, vol. 51, no. 5, pp. 541–552, 2002

    2002

  13. [13]

    Correlation power analysis with a leakage model,

    E. Brier, C. Clavier, and F. Olivier, “Correlation power analysis with a leakage model,” inInternational workshop on cryptographic hardware and embedded systems. Springer, 2004, pp. 16–29

    2004

  14. [14]

    Mangard, E

    S. Mangard, E. Oswald, and T. Popp,Power analysis attacks: Revealing the secrets of smart cards. Springer, 2007

    2007

  15. [15]

    Threshold implementations against side-channel attacks and glitches,

    S. Nikova, C. Rechberger, and V . Rijmen, “Threshold implementations against side-channel attacks and glitches,” inInternational conference on information and communications security. Springer, 2006, pp. 529–545

    2006

  16. [16]

    Towards sound approaches to counteract power-analysis attacks,

    S. Chari, C. S. Jutla, J. R. Rao, and P. Rohatgi, “Towards sound approaches to counteract power-analysis attacks,” inAnnual International Cryptology Conference. Springer, 1999, pp. 398–412

    1999

  17. [17]

    Verified proofs of higher-order masking,

    G. Barthe, S. Bela ¨ıd, F. Dupressoir, P.-A. Fouque, B. Gr ´egoire, and P.-Y . Strub, “Verified proofs of higher-order masking,” inAnnual International Conference on the Theory and Applications of Cryptographic Techniques. Springer, 2015, pp. 457–485

    2015

  18. [18]

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

    R. Bloem, H. Groß, R. Iusupov, B. K¨onighofer, S. Mangard, and J. Winter, “Formal verification of masked hardware implementations in the presence of glitches,” inAnnual International Conference on the Theory and Applications of Cryptographic Techniques. Springer, 2018, pp. 321– 353

    2018

  19. [19]

    Cocoalma: A versatile masking verifier,

    V . Hadzic and R. Bloem, “Cocoalma: A versatile masking verifier,” in 21st International Conference on Formal Methods in Computer-Aided Design: FMCAD 2021, 2021, pp. 14–23

    2021

  20. [20]

    Trusted scalable sat solving with on-the-fly lrat checking,

    D. Schreiber, “Trusted scalable sat solving with on-the-fly lrat checking,” in27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Schloss Dagstuhl–Leibniz-Zentrum f¨ur Informatik, 2024, pp. 25–1

    2024

  21. [21]

    A fast quantum mechanical algorithm for database search,

    L. K. Grover, “A fast quantum mechanical algorithm for database search,” inProceedings of the twenty-eighth annual ACM symposium on Theory of computing, 1996, pp. 212–219

    1996

  22. [22]

    From schr ¨odinger’s equation to the quantum search algorithm,

    ——, “From schr ¨odinger’s equation to the quantum search algorithm,” American Journal of Physics, vol. 69, no. 7, pp. 769–777, 2001

    2001

  23. [23]

    Strengths and weaknesses of quantum computing,

    C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, “Strengths and weaknesses of quantum computing,”SIAM journal on Computing, vol. 26, no. 5, pp. 1510–1523, 1997

    1997

  24. [24]

    Quantum walk speedup of backtracking algorithms

    A. Montanaro, “Quantum walk speedup of backtracking algorithms,” arXiv preprint arXiv:1509.02374, 2015

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  25. [25]

    Efficient quantum circuit synthesis for sat-oracle with limited ancillary qubit,

    S. Yang, W. Zi, B. Wu, C. Guo, J. Zhang, and X. Sun, “Efficient quantum circuit synthesis for sat-oracle with limited ancillary qubit,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 43, no. 3, pp. 868–877, 2023

    2023

  26. [26]

    Finding solutions to the integer case constraint satisfiability problem using grover’s algorithm,

    G. M. Vinod and A. Shaji, “Finding solutions to the integer case constraint satisfiability problem using grover’s algorithm,”IEEE Transactions on Quantum Engineering, vol. 2, pp. 1–13, 2021

    2021

  27. [27]

    A parallel and distributed quantum sat solver based on entanglement and quantum teleportation,

    S.-W. Lin, T.-F. Wang, Y .-R. Chen, Z. Hou, D. San´an, and Y . S. Teo, “A parallel and distributed quantum sat solver based on entanglement and quantum teleportation,”arXiv preprint arXiv:2308.03344, 2023

    work page arXiv 2023

  28. [28]

    Tight bounds on quantum searching,

    M. Boyer, G. Brassard, P. Høyer, and A. Tapp, “Tight bounds on quantum searching,”Fortschritte der Physik: Progress of Physics, vol. 46, no. 4-5, pp. 493–505, 1998

    1998

  29. [29]

    Chi-square test and its application in hypothesis testing,

    R. Rana and R. Singhal, “Chi-square test and its application in hypothesis testing,”Journal of the practice of cardiovascular sciences, vol. 1, no. 1, pp. 69–71, 2015

    2015

  30. [30]

    Probability inequalities for sums of bounded random variables,

    W. Hoeffding, “Probability inequalities for sums of bounded random variables,”Journal of the American statistical association, vol. 58, no. 301, pp. 13–30, 1963

    1963

  31. [31]

    Cadical, gimsatul, isasat and kissat entering the sat competition 2024,

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt, “Cadical, gimsatul, isasat and kissat entering the sat competition 2024,” Proc. of SAT Competition, pp. 8–10, 2024

    2024

  32. [32]

    PennyLane: Automatic differentiation of hybrid quantum-classical computations

    V . Bergholm, J. Izaac, M. Schuld, C. Gogolin, S. Ahmed, V . Ajith, M. S. Alam, G. Alonso-Linaje, B. AkashNarayanan, A. Asadiet al., “Pennylane: Automatic differentiation of hybrid quantum-classical computations,” arXiv preprint arXiv:1811.04968, 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018