pith. machine review for the scientific record. sign in

arxiv: 2604.06712 · v2 · submitted 2026-04-08 · 💻 cs.CR · cs.SE· quant-ph

Recognition: no theorem link

Broken Quantum: A Systematic Formal Verification Study of Security Vulnerabilities Across the Open-Source Quantum Computing Simulator Ecosystem

Dominik Blain
Authors on Pith no claims yet

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

classification 💻 cs.CR cs.SEquant-ph
keywords quantum computing simulatorssecurity vulnerabilitiesformal verificationstatic analysisZ3 SMT solverQASM injectionsupply chain securityCWE patterns
0
0 comments X

The pith

A formal audit of 45 quantum simulators uncovers 547 security vulnerabilities with all patterns proven exploitable by Z3.

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

The paper performs the first comprehensive formal security audit of the open-source quantum computing simulator ecosystem by applying a custom static analysis engine to 45 frameworks. It identifies 547 security findings across memory corruption, resource exhaustion, code injection, and a novel QASM injection vector, with every one of the 13 patterns formally confirmed as satisfiable through Z3 proofs. A consistent 32-qubit threshold appears in the vulnerability chains, and supply chain tracing shows vulnerabilities moving from a commercial framework into national laboratory infrastructure. This matters because quantum simulators underpin virtually all quantum algorithm research, so flaws here can affect the integrity of experiments and the security of dependent systems.

Core claim

Applying the COBALT QAI static analysis engine backed by the Z3 SMT solver to 45 open-source quantum simulation frameworks from 22 organizations spanning 12 countries identifies 547 security findings (40 CRITICAL, 492 HIGH, 15 MEDIUM) across four vulnerability classes: CWE-125/190 C++ memory corruption, CWE-400 Python resource exhaustion, CWE-502/94 unsafe deserialization and code injection, and CWE-77/22 QASM injection. All 13 vulnerability patterns are formally verified via Z3 satisfiability proofs (13/13 SAT). The 32-qubit boundary emerges as a consistent formal threshold in both C++ and Python vulnerability chains, and supply chain analysis documents the first case of vulnerability转移from

What carries the argument

The COBALT QAI static analysis engine backed by the Z3 SMT solver, which scans the 45 frameworks for the 13 vulnerability patterns and generates formal satisfiability proofs to confirm their presence.

If this is right

  • Nine frameworks score 100/100 under all four scanners and can be treated as free of the identified patterns.
  • The 32-qubit boundary indicates that simulations beyond this size may trigger or evade certain vulnerability classes differently.
  • QASM injection constitutes a quantum-specific attack vector without a direct classical counterpart that requires new defensive measures.
  • Vulnerability transfer through the supply chain means organizations using frameworks that depend on commercial code must audit upstream sources.
  • Popular simulators including Qiskit Aer, Cirq, tequila, and PennyLane score 0/100 and therefore contain at least one of the verified patterns.

Where Pith is reading between the lines

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

  • Quantum algorithm researchers should prefer the nine clean frameworks or add manual checks before running code on the others to avoid relying on potentially compromised simulation results.
  • The presence of a novel quantum-specific vulnerability class suggests that classical security tools alone are insufficient and that domain-specific scanners may be needed for future quantum software.
  • Supply chain risks imply that even closed-source commercial quantum tools can introduce defects into open national laboratory infrastructure when code is shared or forked.
  • Integrating formal verification steps like Z3 checks into the standard development workflow for quantum simulators could prevent similar widespread issues in future releases.

Load-bearing premise

The custom static analysis engine produces sound and complete results with no false positives or missed code paths across all 45 frameworks and that the chosen simulators plus the 13 patterns fully represent the security surface of the ecosystem.

What would settle it

An independent manual code review or dynamic exploit attempt on one of the reported CRITICAL vulnerabilities in a specific framework, such as Qiskit Aer, that shows the pattern cannot be triggered as the analysis claims.

Figures

Figures reproduced from arXiv: 2604.06712 by Dominik Blain.

Figure 1
Figure 1. Figure 1: IBM vulnerability propagation chain to US national laboratory infrastructure [PITH_FULL_IMAGE:figures/full_fig_p019_1.png] view at source ↗
read the original abstract

Quantum computing simulators form the classical software foundation on which virtually all quantum algorithm research depends. We present Broken Quantum, the first comprehensive formal security audit of the open-source quantum computing simulator ecosystem. Applying COBALT QAI -- a four-module static analysis engine backed by the Z3 SMT solver -- we analyze 45 open-source quantum simulation frameworks from 22 organizations spanning 12 countries. We identify 547 security findings (40 CRITICAL, 492 HIGH, 15 MEDIUM) across four vulnerability classes: CWE-125/190 (C++ memory corruption), CWE-400 (Python resource exhaustion), CWE-502/94 (unsafe deserialization and code injection), and CWE-77/22 (QASM injection -- a novel, quantum-specific attack vector with no classical analog). All 13 vulnerability patterns are formally verified via Z3 satisfiability proofs (13/13 SAT). The 32-qubit boundary emerges as a consistent formal threshold in both C++ and Python vulnerability chains. Supply chain analysis identifies the first documented case of vulnerability transfer from a commercial quantum framework into US national laboratory infrastructure (IBM Qiskit Aer to XACC/Oak Ridge National Laboratory). Nine frameworks score 100/100 under all four scanners; Qiskit Aer,Cirq, tequila, PennyLane, and 5 others score 0/100.

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

4 major / 2 minor

Summary. The paper presents the first comprehensive formal security audit of 45 open-source quantum simulators from 22 organizations using a custom four-module static analysis engine (COBALT QAI) backed by the Z3 SMT solver. It reports 547 security findings (40 CRITICAL, 492 HIGH, 15 MEDIUM) in four classes—CWE-125/190 (C++ memory corruption), CWE-400 (Python resource exhaustion), CWE-502/94 (unsafe deserialization/code injection), and CWE-77/22 (novel QASM injection)—with all 13 vulnerability patterns Z3-verified as SAT. A consistent 32-qubit threshold is identified in vulnerability chains, and supply-chain analysis documents vulnerability transfer from IBM Qiskit Aer into XACC at Oak Ridge National Laboratory. Nine frameworks score 100/100 while Qiskit Aer, Cirq, and others score 0/100.

Significance. If the COBALT QAI results are sound, the work would be significant as the first systematic formal audit of the quantum simulator ecosystem that underpins quantum algorithm research. Strengths include broad coverage of 45 frameworks across 12 countries, explicit Z3 satisfiability proofs for every pattern (13/13 SAT), and identification of a quantum-specific attack vector plus a documented supply-chain transfer into national-lab infrastructure. These elements could inform secure development practices and highlight previously unexamined risks in classical foundations of quantum computing.

major comments (4)
  1. [Abstract and §3 (Methodology)] Abstract and COBALT QAI description: the central claim of 547 findings and 13/13 Z3 SAT verifications rests on an unvalidated custom static analyzer; the manuscript provides no encoding details for C++ memory semantics, Python resource limits, QASM parsing, or the 32-qubit threshold, nor any benchmark against CodeQL/Infer or manual audit of even a 5% sample of reports.
  2. [§4 (Vulnerability Patterns and Findings)] Results on vulnerability classes: the assertion that CWE-77/22 QASM injection is a novel quantum-specific vector with no classical analog is load-bearing for the paper's contribution, yet the modeling of QASM parsing and injection paths in the four-module engine is not described, preventing assessment of over-approximation or missed paths.
  3. [§5 (Supply Chain Analysis)] Supply-chain analysis: the claim of the first documented vulnerability transfer from commercial Qiskit Aer into XACC/Oak Ridge National Laboratory is presented as a key result, but no specific code paths, version mappings, or confirmation steps are provided to substantiate the transfer.
  4. [§4.2 (Threshold Analysis)] Threshold and scoring: the 32-qubit boundary is stated to emerge consistently, yet no equations, analysis steps, or per-framework data tables show how this threshold was derived from the Z3 models or scanner outputs.
minor comments (2)
  1. [Results tables] The scoring table for the nine 100/100 frameworks and the zero-scoring ones would benefit from explicit listing of which scanners contributed to each score.
  2. Notation for the four vulnerability classes mixes CWE identifiers with quantum-specific extensions; a brief glossary or mapping table would improve clarity.

Simulated Author's Rebuttal

4 responses · 0 unresolved

We thank the referee for their insightful comments on our manuscript. We address each of the major comments point by point below, providing clarifications and committing to revisions where the manuscript can be strengthened.

read point-by-point responses

  1. Referee: [Abstract and §3 (Methodology)] Abstract and COBALT QAI description: the central claim of 547 findings and 13/13 Z3 SAT verifications rests on an unvalidated custom static analyzer; the manuscript provides no encoding details for C++ memory semantics, Python resource limits, QASM parsing, or the 32-qubit threshold, nor any benchmark against CodeQL/Infer or manual audit of even a 5% sample of reports.

    Authors: We agree that additional details on the COBALT QAI implementation would improve the paper's transparency and reproducibility. In the revised manuscript, we will expand Section 3 to include the specific Z3 encodings for C++ memory operations (e.g., buffer size calculations), Python resource exhaustion models, QASM parsing abstractions, and the formalization of the 32-qubit threshold. We will also add a validation subsection that includes benchmarks against CodeQL and Infer on a representative sample of 5 frameworks, as well as a summary of our internal manual audit of 10% of the reported findings to confirm the static analysis results. revision: yes

  2. Referee: [§4 (Vulnerability Patterns and Findings)] Results on vulnerability classes: the assertion that CWE-77/22 QASM injection is a novel quantum-specific vector with no classical analog is load-bearing for the paper's contribution, yet the modeling of QASM parsing and injection paths in the four-module engine is not described, preventing assessment of over-approximation or missed paths.

    Authors: The novelty of QASM injection stems from its exploitation of the quantum circuit description interface, which allows injection of malicious operations that affect quantum state simulation in ways not possible in purely classical systems. To address the concern, we will revise Section 4 to provide a detailed description of the QASM module in COBALT QAI, including the grammar rules abstracted, the dataflow analysis for injection paths, and discussion of potential over-approximations. This will allow readers to evaluate the soundness of the detection. revision: yes

  3. Referee: [§5 (Supply Chain Analysis)] Supply-chain analysis: the claim of the first documented vulnerability transfer from commercial Qiskit Aer into XACC/Oak Ridge National Laboratory is presented as a key result, but no specific code paths, version mappings, or confirmation steps are provided to substantiate the transfer.

    Authors: The supply chain analysis identifies shared vulnerable code between Qiskit Aer and XACC through static matching of code patterns and dependency graphs. We will update Section 5 with the specific code paths (file names and functions), version mappings (e.g., Aer v0.XX to XACC commit YYY), and the step-by-step confirmation process used, including how the vulnerability was traced across the supply chain. revision: yes

  4. Referee: [§4.2 (Threshold Analysis)] Threshold and scoring: the 32-qubit boundary is stated to emerge consistently, yet no equations, analysis steps, or per-framework data tables show how this threshold was derived from the Z3 models or scanner outputs.

    Authors: The 32-qubit threshold arises from Z3 satisfiability when qubit-dependent size computations exceed integer limits in the modeled semantics. We will revise Section 4.2 to include the relevant Z3 formulas (such as those for buffer allocation: size = qubits * sizeof(complex) > 2^31), the analysis steps, and supplementary tables listing the minimal qubit count for vulnerability activation per framework and class. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical audit of third-party codebases via external SMT solver

full rationale

The manuscript reports results from applying the authors' COBALT QAI static analyzer (backed by Z3) to 45 external open-source quantum simulators. No equations, fitted parameters, self-definitional constructs, or load-bearing self-citations appear in the provided text. The 547 findings, 13 SAT proofs, 32-qubit threshold, and supply-chain observations are outputs of analysis performed on independent codebases rather than quantities defined in terms of the paper's own inputs. This is a standard empirical security study whose central claims do not reduce to the authors' prior work or internal definitions by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on the unverified soundness of a custom static-analysis engine and the representativeness of the 45-framework sample; no independent evidence for either is supplied in the abstract.

axioms (2)
  • domain assumption COBALT QAI static analysis engine accurately detects the listed CWE classes and produces only true positives in quantum simulator codebases.
    All 547 findings and the 13/13 SAT proofs depend on this unexamined tool property.
  • domain assumption The 45 selected open-source frameworks and 22 organizations constitute a representative sample of the quantum simulator ecosystem.
    Selection criteria and coverage claims are not justified in the abstract.
invented entities (1)
  • QASM injection attack vector no independent evidence
    purpose: To classify a novel quantum-specific vulnerability involving unsafe handling of QASM code.
    Presented as new with no classical analog, but no external exploit demonstration or independent confirmation is provided.

pith-pipeline@v0.9.0 · 5542 in / 1713 out tokens · 52814 ms · 2026-05-10T17:51:55.435856+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

33 extracted references · 1 canonical work pages · 1 internal anchor

  1. [1]

    Qiskit contributors.Qiskit: An Open-source Framework for Quantum Computing.https:// github.com/Qiskit/qiskit-aer, 2024

    2024

  2. [2]

    Google Quantum AI.Cirq: A Python library for writing, manipulating, and optimizing quan- tum circuits.https://github.com/quantumlib/Cirq, 2024

    2024

  3. [3]

    PennyLane: Automatic differentiation of hybrid quantum-classical computations

    V. Bergholm et al.PennyLane: Automatic differentiation of hybrid quantum-classical compu- tations. arXiv:1811.04968, 2022

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  4. [4]

    Rigetti Computing.PyQuil: A Python library for quantum programming using Quil.https: //github.com/rigetti/pyquil, 2024

    2024

  5. [5]

    Amazon Web Services.Amazon Braket Default Simulator.https://github.com/ amazon-braket/amazon-braket-default-simulator-python, 2024

    2024

  6. [6]

    McCaskey et al.XACC: A System-Level Software Infrastructure for Heterogeneous Quantum-Classical Computing.Quantum Science and Technology, 5(2):024002, 2020

    A. McCaskey et al.XACC: A System-Level Software Infrastructure for Heterogeneous Quantum-Classical Computing.Quantum Science and Technology, 5(2):024002, 2020

    2020

  7. [7]

    Efthymiou et al.Qibo: A framework for quantum simulation with hardware acceleration

    S. Efthymiou et al.Qibo: A framework for quantum simulation with hardware acceleration. Quantum Science and Technology, 7(1):015018, 2022

    2022

  8. [8]

    Baidu Research.Paddle Quantum: A Quantum Machine Learning Toolkit Based on Pad- dlePaddle.https://github.com/PaddlePaddle/Quantum, 2023

    2023

  9. [9]

    J. S. Kottmann et al.TEQUILA: A platform for rapid development of quantum algorithms. Quantum Science and Technology, 6(2):024009, 2021

    2021

  10. [10]

    Steiger, T

    D. Steiger, T. H¨ aner, M. Troyer.ProjectQ: An Open Source Software Framework for Quantum Computing.Quantum, 2:49, 2018

    2018

  11. [11]

    Zhang et al.TensorCircuit: a Quantum Software Framework for the NISQ Era.Quantum, 7:912, 2023

    S.-X. Zhang et al.TensorCircuit: a Quantum Software Framework for the NISQ Era.Quantum, 7:912, 2023. 27

    2023

  12. [12]

    NVIDIA Corporation.CUDA Quantum: A Platform for Hybrid Quantum-Classical Comput- ing.https://github.com/NVIDIA/cuda-quantum, 2024

    2024

  13. [13]

    Jones, T

    J. Jones, T. Proctor, K. Rudinger, T. Young.QuEST and High Performance Simulation of Quantum Computers.Scientific Reports, 9:10736, 2019

    2019

  14. [14]

    Gheorghiu.Quantum++: A Modern C++ Quantum Computing Library.PLOS ONE, 2018

    V. Gheorghiu.Quantum++: A Modern C++ Quantum Computing Library.PLOS ONE, 2018

    2018

  15. [15]

    https://github.com/mindspore-ai/mindquantum, 2023

    Huawei Technologies.MindQuantum: A High-Performance Quantum Computing Framework. https://github.com/mindspore-ai/mindquantum, 2023

    2023

  16. [16]

    Suzuki et al.Qulacs: a Fast and Versatile Quantum Circuit Simulator for Research Purpose

    Y. Suzuki et al.Qulacs: a Fast and Versatile Quantum Circuit Simulator for Research Purpose. Quantum, 5:559, 2021

    2021

  17. [17]

    de Moura and N

    L. de Moura and N. Bjørner.Z3: An Efficient SMT Solver. InTACAS, LNCS 4963, pp. 337–

  18. [18]

    Blain.COBALT: Formal Verification for Security Vulnerabilities in Systems Software

    D. Blain.COBALT: Formal Verification for Security Vulnerabilities in Systems Software. QreativeLab Inc., 2026

    2026

  19. [19]

    Paradis et al.Unitary Property Testing

    D. Paradis et al.Unitary Property Testing. InPOPL, 2023

    2023

  20. [20]

    Xu et al.Quartz: Superoptimization of Quantum Circuits

    K. Xu et al.Quartz: Superoptimization of Quantum Circuits. InPLDI, 2022

    2022

  21. [21]

    Bravyi et al.Quantum circuits with classical channels.Physical Review A, 2020

    A. Bravyi et al.Quantum circuits with classical channels.Physical Review A, 2020

    2020

  22. [22]

    Bichsel et al.Silq: A High-Level Quantum Language with Safe Uncomputation

    B. Bichsel et al.Silq: A High-Level Quantum Language with Safe Uncomputation. InPLDI, 2020

    2020

  23. [23]

    Krishnamurthy et al.Security of High-Performance Computing Systems.IEEE Security & Privacy, 2020

    S. Krishnamurthy et al.Security of High-Performance Computing Systems.IEEE Security & Privacy, 2020

    2020

  24. [24]

    Virtanen et al.SciPy 1.0: Fundamental algorithms for scientific computing in Python

    P. Virtanen et al.SciPy 1.0: Fundamental algorithms for scientific computing in Python. Nature Methods, 2020

    2020

  25. [25]

    Vu et al.An Empirical Study of the Effects of Programming Languages on Code Quality

    X. Vu et al.An Empirical Study of the Effects of Programming Languages on Code Quality. InMSR, 2022

    2022

  26. [26]

    Sivarajah et al.t|ket⟩: A Retargetable Compiler for NISQ Devices.Quantum Science and Technology, 6(1):014003, 2021

    S. Sivarajah et al.t|ket⟩: A Retargetable Compiler for NISQ Devices.Quantum Science and Technology, 6(1):014003, 2021

    2021

  27. [27]

    Wang et al.Quantumnas: Noise-adaptive Search for Robust Quantum Circuits

    H. Wang et al.Quantumnas: Noise-adaptive Search for Robust Quantum Circuits. InHPCA, 2022

    2022

  28. [28]

    Heurtel et al.Perceval: A Software Platform for Discrete Variable Photonic Quantum Computing.Quantum, 7:1094, 2023

    N. Heurtel et al.Perceval: A Software Platform for Discrete Variable Photonic Quantum Computing.Quantum, 7:1094, 2023

    2023

  29. [29]

    Silverio et al.Pulser: An Open-source Package for the Design of Pulse Sequences in Pro- grammable Neutral-atom Arrays.Quantum, 6:629, 2022

    H. Silverio et al.Pulser: An Open-source Package for the Design of Pulse Sequences in Pro- grammable Neutral-atom Arrays.Quantum, 6:629, 2022

    2022

  30. [30]

    Department of Energy.DOE Quantum Internet Blueprint

    U.S. Department of Energy.DOE Quantum Internet Blueprint. Office of Science, 2020

    2020

  31. [31]

    Bhargavan et al.Formal verification of cryptographic protocols with SMT solvers

    K. Bhargavan et al.Formal verification of cryptographic protocols with SMT solvers. InCCS, 2014. 28

    2014

  32. [32]

    Ball et al.SLAM and Static Driver Verifier

    T. Ball et al.SLAM and Static Driver Verifier. InIFM, 2004

    2004

  33. [33]

    Kazemian et al.Header Space Analysis: Static Checking for Networks

    P. Kazemian et al.Header Space Analysis: Static Checking for Networks. InNSDI, 2012. 29

    2012