A rewind test for secrets in quantum programs

What counts as a leak?

The researchers divide a program’s variables into two groups: High, containing confidential information, and Low, accessible to an attacker. These labels describe access, not whether a variable is classical or quantum.

Their first security definition extends a classical idea called noninterference. Take two possible inputs that look identical to someone who can access only Low variables. After running the program, those accessible outputs must still look identical. Changing the hidden information must not create an observable difference.

For quantum programs, looking identical means having the same reduced density operator: the mathematical description left after the inaccessible variables are disregarded. Crucially, the definition also accommodates entangled information outside the program itself. Checking an isolated output is not enough if an attacker possesses another quantum system correlated with it.

The paper then offers a second definition with an explicit attacker. Confidential classical information can first be encoded into a joint classical–quantum state. An attacker subsequently operates only on accessible variables and tries to recover it. Security requires that an attacker without the program’s execution can do at least as well, using the accessible information already present. The comparison uses a worst-case recovery measure defined through fidelity, a measure of overlap between states.

The authors prove these two definitions equivalent. That connects a compact mathematical requirement to an operational question: did executing the program make the secret more recoverable?

Why running two copies does not suffice

A familiar classical verification technique compares a program with a renamed copy of itself. If their accessible inputs agree, a proof checks that their accessible outputs agree too.

The direct quantum translation breaks down. The authors show that no quantum observable can both accept every pair of identical unknown pure states with certainty and reject every pair of orthogonal pure states with certainty. The obstruction resembles the no-cloning theorem, although the immediate problem here is comparing states rather than copying them.

Their alternative, self-conjugation, replaces comparison with restoration.

First, the program is translated into a larger reversible circuit. Classical variables receive quantum representations, while extra environmental variables retain information that assignments, resets and measurements would otherwise discard. This is a mathematical construction: it does not claim that an ordinary measurement can simply be undone after its record has been lost.

The verification circuit runs that enlarged circuit, swaps its Low outputs into fresh variables, and then runs the enlarged circuit’s reverse. For an already reversible quantum circuit, the intuition is straightforward: secret information moved into the swapped-out outputs is no longer available to restore the original hidden state.

General programs require a more qualified condition. The environmental variables start in a designated zero state; the proof requires restoration of the High information in the component where those environmental variables also return to zero. Reference systems initially maximally entangled with the High variables make that restoration expressible as a formal assertion.

The authors prove that the resulting condition is equivalent to noninterference. They express it in quantum Hoare logic, a framework for proving that operations take states satisfying one assertion into states satisfying another. Verification is mathematical reasoning that can be performed on a classical computer, not a requirement to execute the rewind circuit on quantum hardware.

Examples—and boundaries

The demonstrations include the quantum one-time pad, whose randomly selected operations conceal a quantum message. This illustrates why examining individual instructions can mislead: a secret key controls operations on an accessible qubit, yet the complete encryption program preserves confidentiality.

Two further examples address syndrome records in a three-qubit bit-flip error-correcting code with a fixed error, and broadcast-message anonymity in a simplified four-party entanglement protocol. The latter assumes honest parties; it is not a demonstration against arbitrary malicious participants.

The work is theoretical and presented as an arXiv preprint. It supplies definitions, proofs and worked examples, not hardware measurements or an implemented verification tool. Its language is loop-free, although fixed-bound loops can be unrolled. Mechanizing the framework and extending self-conjugation to general loops and recursion remain future work.

Its contribution is therefore a precise route from a confidentiality claim to proof obligations—not a blanket guarantee that a quantum application, device or implementation is secure.