PQC Research Series — Part 5

Leakage-Aware Adversaries: Constant-Time as a Formal Contract in Post-Quantum Systems

Author: Mayckon Giovani
Date: September 29, 2026
Series: PQC Research Series
Tags: PQC, Formal Methods, Cryptography, Systems

TL;DR

A reduction proves security for specified interfaces. A deployed cryptographic service exposes additional observations: instruction latency, memory traffic, power consumption, rejection behavior, scheduling, and residual state. The relevant question is not whether the mathematical primitive remains hard. It is whether the implementation preserves the information boundary assumed by the security game.

Constant-time is a relational property of executions under an explicit observation model. It is not a synonym for fixed wall-clock duration, a property established by the absence of conditional statements, or a guarantee against every physical attack. This article derives a leakage-aware security contract, examines where that contract fails in lattice implementations, and provides a reproducible synthetic experiment showing when repeated timing observations amplify a small signal—and when correlated noise prevents that amplification.

Key takeaways

• Name the observer before claiming noninterference: architectural traces, microarchitectural effects, and physical measurements are different interfaces.
• A quantum-capable adversary can process classical leakage without having coherent quantum access to the device.
• Functional correctness, leakage resistance, and secure erasure require separate proof obligations.
• Negative timing tests are evidence within an experiment, not proofs of observational equivalence.
• Security claims belong to versioned binaries and deployment assumptions, not just algorithm names.

0. Context

Part 4 examined the quantitative loss introduced by security reductions. This part examines a logically prior boundary: whether the real implementation gives the adversary an interface that the reduction can simulate.

A tight reduction cannot compensate for an unmodeled secret-dependent observation. Conversely, an implementation does not become insecure merely because its runtime varies: the variation must be analyzed relative to secrets, public inputs, randomness, and the observer. The task is to replace the ambiguous label “constant-time” with a contract precise enough to survive compilation, concurrency, and hardware execution. Physically observable cryptography provides the foundational reason for doing this: physical observations must be modeled rather than silently excluded from a mathematical security statement. (1)

1. Problem Statement

Let an implementation be described by

where $P$ is source code, $C$ is a compiler configuration, $M$ is the target machine, $\theta$ is the cryptographic parameter set, and $\mathcal E$ is the execution environment. The environment includes the allocator, operating system, scheduler, interrupt behavior, and co-resident processes.

Suppose an idealized scheme admits a reduction bound

where $\mathcal H$ is the underlying hardness problem, $B$ is the reduction-derived solver, and $\mathbf q$ records oracle-query budgets. This statement does not yet bound an adversary that also sees execution-dependent leakage.

The objective is to justify a real-system bound of the form

The additional term is not an arbitrary allowance called “side-channel margin.” It must follow from a defined relation between real observations and the ideal interface. The resources consumed by that relation also affect the resources of $B'$.

Assumptions

The protected service accepts classical requests. An adversary may choose requests adaptively, repeat operations against a persistent key, and combine transcripts with observations allowed by the deployment threat model. It may execute quantum computations and, where the cryptographic proof uses QROM, make coherent queries to the modeled public random oracle. None of those permissions automatically gives it coherent access to a physical signing device.

Remote timing, local cache observation, physical probing, and fault injection are distinct capabilities. This article does not silently equate them. Unrestricted reads of secret memory or arbitrary execution inside the trusted cryptographic boundary trivialize the confidentiality problem and must either be excluded explicitly or addressed by a different isolation architecture.

Non-goals

This is not a proposal for new lattice parameters, a new masking construction, or a replacement for standardized primitives. The experiment below is a synthetic Gaussian observation model, not a benchmark of ML-KEM, ML-DSA, or any processor. The formal statements are definitions and proof sketches; they are not claims of machine-checked verification of a production library.

2. Formal Model

2.1 Execution, observations, and adaptive interaction

Write an execution as

where $p$ is public input, $s$ is secret state, $r$ is internal randomness, $\eta$ is an environment schedule, $o$ is the functional output, $\tau$ is an execution trace, and $\sigma_f$ is final machine state.

An observation function extracts

Different choices of $\mathcal L_M$ define different security questions. An architectural model may expose branch decisions and memory addresses. A physical model may expose noisy power measurements. A post-compromise model may expose selected memory regions after a key is supposed to have been erased.

Not every functional output is public. A signature normally leaves the service; a decapsulated session key normally does not. Let $\operatorname{Visible}(o)$ identify the permitted interface output. Accidentally treating every return value as public can make a leakage proof vacuous.

For a stateful service, the adversary observes a sequence

A one-call argument is therefore insufficient unless it composes under key reuse, adversarial inputs, and state transitions.

2.2 Constant-time as a relational property

For a deterministic program and a fixed admissible environment, a basic constant-time requirement is

Here $\mathcal L_M$ is understood to project the observation from the execution result. The secret states must satisfy the same public preconditions. The quantification over environments must match the deployment: proving this for one scheduler does not establish it for arbitrary interference.

This compares two executions. It is a hyperproperty, not merely a predicate on the output of one execution. Product-program techniques exploit that distinction by reasoning about paired executions; ct-verif is a concrete verification approach in this family, operating on optimized LLVM representations. (2)

Declassification requires an explicit policy $D$. A controlled relaxation permits comparison only when

That policy cannot be chosen after inspecting the code simply to classify every leaked predicate as public. Declaring a secret-dependent rejection flag to be declassified changes the security claim; it does not repair the implementation.

For randomized execution, pointwise equality under identical random coins is often unnecessarily strong. One may instead require equality of observation distributions,

or an explicitly bounded statistical or computational distance. Where public outputs legitimately depend on secrets, a more appropriate formulation is simulation of leakage from the permitted interface, rather than unconditional independence from all secret state.

2.3 Architectural constant-time is a model, not the machine

A common architectural trace contains program-counter transitions, branch decisions, and load/store addresses. Equality of these traces rules out important attacks, but it does not automatically imply equal timing if instruction latency depends on operands.

A more realistic local cost function has the form

To infer timing independence from architectural trace equality, one needs assumptions about this function and about how microstate evolves. Variable-latency arithmetic, speculative execution, and data-dependent prefetching are not eliminated by merely avoiding secret-dependent array indices.

The Jasmin documentation illustrates the need to distinguish contracts: its tooling separates architectural constant-time checks, stronger instruction-timing considerations, and speculative constant-time analysis. Safety is also a prerequisite; a relational argument over executions that invoke undefined behavior is not a deployment guarantee. (3)

2.4 Quantum computation does not make the sensor quantum

Let $L$ denote a classical leakage transcript and $E$ an adversary's quantum side information. Their joint state can be represented as

The device may produce entirely classical measurements while the attacker processes those measurements jointly with quantum state. This is different from granting a unitary oracle for physical execution.

A useful resource vector is

It records classical and quantum time and memory, quantum hash queries, API queries, observation count, sensor bandwidth, and key lifetime. These are not interchangeable budgets. API rate limits can restrict online observations; they cannot prevent offline computation over previously collected traces.

2.5 A simulation contract for leakage

Let $V_{\mathrm{real}}$ contain the actual adaptive transcript and allowed leakage. Let $V_{\mathrm{sim}}$ contain a transcript in which a simulator generates leakage using only the ideal interface and authorized public information.

A computational leakage-simulation contract is

with explicit resource restrictions on both simulator and distinguisher. A sufficient information-theoretic condition, including quantum side information, is

For a single success-event game, replacing the real view by the simulated view changes success probability by at most $\delta_{\mathrm{sim}}$. A security advantage defined as a difference between two challenge experiments may incur two such replacement terms. Constants depend on the exact advantage convention; they should not disappear in prose.

A sequential bound

requires conditional simulation guarantees that remain valid after every reachable history, including correlated side information. It does not follow from separately testing the marginal distribution of each request.

2.6 Why “only a few leaked bits” is not a security assessment

For a classical key $K$ and leakage $L$, define optimal guessing probability and average conditional min-entropy by

If $L$ has at most $2^b$ possible values, then

because each summand is at most $\max_k\Pr[K=k]$. Consequently,

This is an average guessing bound for classical side information. It is not a worst-case guarantee for every observed value, a lattice-reduction theorem, or a statement that each leaked bit subtracts exactly one bit from attack cost. Algebraically structured leakage may be substantially more useful than an equal-length arbitrary string. Quantum side information requires the corresponding quantum conditional-entropy treatment rather than this elementary classical derivation.

3. System Constraints

Memory is part of the adversarial boundary

An admission-control invariant for a constrained service can be written as

This is not a cryptographic theorem, but violating it can invalidate cryptographic assumptions. Workspace pressure can trigger allocator paths, induce spills, force unsafe buffer reuse, or motivate sharing scratch memory across concurrent requests. A shared scratch buffer without an ownership protocol introduces both correctness and confidentiality hazards.

Measurements must cover the actual concurrency level and interrupt configuration, not just one isolated operation. Cortex-M is a family, not one microarchitectural model; cache behavior, instruction timing, and memory placement must be tied to a specific target. The pqm4 work demonstrates the value of platform-specific embedded evaluation, but historical measurements are not current performance claims for a different build. (4)

Rust ownership and Go memory safety address important classes of failures. Neither is a theorem about secret-independent execution time. FFI boundaries, compiler lowering, garbage collection, retained heap objects, and assembly implementations remain part of the contract.

Randomness and deadlines interact

If an operation requires $R_{\mathrm{op}}$ bits from a specified random-generation interface and requests arrive at rate $\nu$, a basic throughput constraint is

This equation says nothing by itself about entropy quality. If a deterministic generator expands a seed, its security, initialization, reseeding, and state-compromise assumptions replace the fiction that all output bits are independent physical entropy.

The dangerous engineering response to a missed deadline is to reuse randomness or masks. Such reuse changes the joint leakage distribution across calls. It is not a performance optimization within the original proof.

Rejection-based algorithms also require probabilistic deadline analysis. Under the illustrative assumption of independent attempts with fixed acceptance probability $p_{\mathrm{acc}}$,

Real algorithms must justify their own distribution rather than inherit this formula by analogy. A timeout can become an observation of acceptance behavior. Whether it leaks a secret depends on the joint distribution; variable attempt count alone is not proof of insecurity.

The network does not erase the processor

Observed latency can be decomposed schematically as

Additional noise can raise sample complexity. It does not establish noninterference. Conversely, observing a laboratory timing difference does not prove a feasible remote attack: query budgets, drift, calibration, and key lifetime determine whether the signal is exploitable.

Observability must respect the same boundary. A metrics label, debug log, or error counter containing a secret-dependent predicate is an additional oracle even if the cryptographic kernel itself satisfies its timing contract.

4. Core Argument / Insight

4.1 Three failures of model preservation

KyberSlash: the instruction contract. KyberSlash analyzed secret-dependent division in Kyber implementations, including operations with public divisor 3329 and secret-dependent numerators. Its results on particular Arm targets show why “public divisor” is not sufficient: operand-dependent timing can survive source-level review and compiler lowering. This is an implementation failure mode, not a break of the LWE assumption or a claim that every ML-KEM implementation is vulnerable. (5)

GoFetch: the observation contract. GoFetch showed how data memory-dependent prefetchers on affected Apple processors can turn data values into microarchitectural activity useful to an attacker. Its evaluation included Kyber and Dilithium implementations. The important distinction is that architectural address independence does not necessarily imply independence of all hardware-generated memory traffic. The attack model includes local microarchitectural observation, not merely arbitrary remote timing. (6)

Hertzbleed: the timing contract. Hertzbleed connected data-dependent power consumption and dynamic voltage/frequency scaling to observable timing. Its cryptographic case study involved SIKE; it should not be relabeled as an ML-KEM exploit. The general lesson is narrower and stronger: instruction-trace reasoning needs additional premises before it can support a wall-clock timing claim. (7)

flowchart TD
    A["Ideal security game"] --> B["Source implementation"]
    B --> C["Compiled binary"]
    C --> D["Processor execution"]
    D --> E["Service environment"]
    E --> F["Adversary observations"]
    X["Operand-dependent latency"] -.-> D
    Y["Prefetching and power"] -.-> D
    Z["Queues and diagnostic logs"] -.-> E
    W["Residual secret copies"] -.-> F

4.2 ML-KEM: implicit rejection is an interface obligation

FIPS 203 specifies an internal ML-KEM decapsulation procedure that decrypts, derives candidate material, re-encrypts, and compares the supplied ciphertext with the reconstructed ciphertext. It also derives a fallback key from secret rejection material and the ciphertext. The internal validity result determines which key is returned; the standard explicitly requires the secret intermediate validity flag not to be exposed. (8)

Abstractly,

The fact that selection has a mathematically defined result does not establish that its implementation hides $b_{\mathrm{valid}}$. The comparison, key selection, cleanup, and wrapper behavior must preserve the same information boundary.

A ciphertext is public input. Intermediate values computed from that ciphertext and a secret key are not therefore public. This distinction is where apparently harmless division, branching, and diagnostic behavior become relevant.

Likewise, rejecting a publicly malformed input length is not the same observation as revealing an internal re-encryption predicate for an otherwise well-formed input. The contract should classify errors rather than insist that every error path in the entire service has identical behavior. At the protocol boundary, externally visible success or failure must also be analyzed under the enclosing security game.

4.3 Signatures: correct output distributions are not complete leakage proofs

ML-DSA descends from Dilithium's Fiat–Shamir-with-aborts design. Rejection sampling is part of the construction's distributional argument; it is not an accidental inefficiency to remove casually. The standard and design specification are the appropriate starting points for understanding that algorithmic contract. (9) (10)

However, a proof about the accepted signature does not, by itself, establish a proof about the accepted signature together with all execution observations.

The logical distinction is immediate. Let $O$ be a uniformly random output bit independent of secret bit $S$, and let leakage be $L=S$. Then

while

This is a counterexample to an inference, not an attack on ML-DSA. An implementation analysis must account for rejection-loop observations and intermediate computations under its actual leakage model. It must not infer insecurity from variable runtime alone, nor infer leakage resistance solely from the final output distribution.

4.4 Reproducible experiment: how a weak signal accumulates

Consider a synthetic secret bit $B\sim\operatorname{Bernoulli}(1/2)$ and observations

Assume the attacker knows $\mu,\Delta,\sigma$, with $\Delta>0$, and gets $N$ observations under the same secret. These calibration and reuse assumptions are essential.

The sample mean has distribution

For equal priors, the optimal threshold classifier selects $B=1$ when $\overline Y_N>\mu+\Delta/2$. Its error probability is

where $\Phi$ is the standard normal cumulative distribution function. To achieve error at most $\varepsilon<1/2$,

The signal-to-noise ratio improves as $\sqrt N$, not linearly. With $\Delta/\sigma=0.02$, the analytic results are:

These numbers do not estimate the query complexity of recovering an ML-KEM key. A real attack needs a relationship between measurements and secret algebraic state, chosen-input control where required, and a reconstruction procedure. The experiment isolates only the accumulation of a specified statistical signal.

Now change the noise model:

where $U,E_1,\ldots,E_N$ are independent standard normal variables, and $U$ is shared across observations within a trial. Then

For $\rho=0.01$ and $\Delta/\sigma=0.02$, the limiting error is approximately $0.4602$. More samples cannot average away the shared offset in this model. Additional calibration observations or a different experimental design could change that conclusion; the floor is not a universal defense.

Figure 1. Analytic curves and 20,000 Monte Carlo trials per sample count and profile, with pointwise 95% Wilson intervals. All values are synthetic; no cryptographic implementation or hardware timing was measured. These intervals have pointwise, not simultaneous, nominal coverage.

The experiment source and generated measurements are available for inspection. The seed is fixed at 20260929. The program samples the exact distribution of the sufficient statistic—the sample mean—rather than explicitly allocating 100,000 observations for every trial.

python3 leakage-experiment.py --output-dir results
python3 leakage-experiment.py --output-dir results --plot

The CSV calculation uses only the Python standard library; plotting additionally requires Matplotlib. Increasing independent random delay raises $\sigma$ and hence the required observations under this model. It does not set $\Delta$ to zero. The engineering decision therefore depends on online-query limits, calibration opportunities, noise structure, and key lifetime—not the assertion that “the network is noisy.”

4.5 Statistical testing is evidence, not noninterference

For two timing populations, a Welch statistic is

Tools such as dudect make statistical timing analysis practical. They are useful for finding discrepancies in the tested implementation and setup; they do not turn an absence of detected differences into a universal proof. (11)

A positive result requires investigation: the cause may be secret dependence, experimental confounding, or an input classification that changes legitimate public work. A negative result is bounded by chosen classes, sample count, measurement quality, and the statistic used.

Mean equality is particularly weak. The distributions $\mathcal N(0,1)$ and $\mathcal N(0,4)$ have the same mean and are distinguishable through their variance. Repeatedly inspecting a test statistic until it crosses a threshold also changes false-positive behavior. Multiple tests and stopping rules belong in the experimental report.

For equal class sizes $N$ in the independent Gaussian model, the population signal relative to the standard error scales approximately as

Failure to detect a small signal at one $N$ cannot justify claiming that the signal is absent at all larger budgets.

4.6 Masking addresses a different observation channel

For Boolean sharing,

choose the first $d$ shares uniformly and set the last share to satisfy the equation. Any subset of at most $d$ initial shares is independent of $s$. That elementary fact does not prove security of a computation performed on the shares.

The probing-model literature formalizes restrictions on which internal wires an adversary may observe and constructs computations secure under those restrictions. Its significance is the explicit observer model, not a blanket claim that splitting a value makes arbitrary machine code safe. (12)

For an appropriately defined internal wire vector $W$, a simplified local obligation is

subject to permitted outputs and the scheme's exact probing definition. Composing gadgets requires additional conditions; the initial-share statement alone supplies none.

Physical transitions, glitches, register reuse, and correlated masks can expose combinations not represented by a naive “one wire, one share” interpretation. Lattice implementations also move between arithmetic and Boolean representations; nonlinear operations and conversions require dedicated constructions and randomness accounting.

Constant-time and masking therefore address different channels. Neither should be advertised as a replacement for the other.

4.7 Compilation must preserve a relational theorem

Ordinary functional compiler correctness relates source and binary results. It need not preserve secrecy of traces.

A required implication is closer to

One can discharge this through a compiler preservation argument, verification of a suitable intermediate representation plus explicit lowering assumptions, or analysis of the final binary. Every route leaves an obligation to connect its observation model to the deployed processor.

flowchart TD
    A["Security game and permitted observations"] --> B["Functional correctness"]
    A --> C["Relational leakage contract"]
    B --> D["Compiler and target assumptions"]
    C --> D
    D --> E["Final binary evidence"]
    E --> F["Wrapper and concurrency analysis"]
    F --> G["Versioned deployment claim"]

Formal methods can also mechanize cryptographic reductions; their scope is not restricted to implementation correctness. The important boundary is that a proof establishes its stated theorem. A functional implementation proof does not automatically strengthen a loose reduction, validate an empirical attack-cost model, or characterize unmodeled hardware.

The same compositional issue appears above the binary. A verified cryptographic kernel inside an unverified wrapper can still expose secret-dependent errors, retries, or logs.

4.8 Erasure is a future-observation property

Suppose a key is retired at time $t$. Secure erasure should mean that an allowed compromise after $t$ reveals no additional information about the retired key beyond what prior authorized observations already permitted.

This is a claim about residual state and future observers. Overwriting one source-level variable does not cover register spills, allocator copies, crash dumps, DMA buffers, or copies retained by another request.

A minimal lifecycle sketch is:

stateDiagram-v2
    [*] --> Allocated
    Allocated --> InUse
    InUse --> Retiring
    Retiring --> Erasing
    Erasing --> Released
    Released --> [*]

The important guards are not visible in the diagram: retirement forbids new borrowers; erasure waits for authorized in-flight uses to finish; release occurs only after the specified regions have been handled. The diagram is a specification sketch, not evidence that those guards hold.

Erasure also cannot retract observations already exfiltrated. Key rotation limits future exposure; it does not make previously recorded leakage disappear.

5. Implications

Security properties and the evidence ledger

A deployment should track at least four distinct claims: correct cryptographic behavior, conformance to a stated observation policy, preservation of that policy under composition, and lifecycle handling of secret state.

Attach those claims to an artifact identity

Changing the compiler, CPU family, build flags, assembly path, concurrency model, or logging behavior should trigger review of affected evidence. This is not a demand to redo every proof on every change. It is a demand to know which theorem and experiment the change invalidates.

Failure modes

What to monitor

Monitor request volume per key, safe aggregate latency distributions, concurrency, workspace exhaustion, RNG health signals, public-input validation errors, and deployed artifact identities. Access to operational data should itself be controlled.

Do not add secret-dependent validity predicates to logs to make diagnosis easier. A production latency dashboard is also not a substitute for controlled leakage tests: workload changes and network noise can hide or create apparent differences.

Rollback plan

If a deployed artifact violates its leakage contract, stop routing new sensitive operations to it and move to an independently validated, compatible implementation. If no such implementation exists, fail closed at the affected boundary rather than silently downgrade the cryptographic protocol.

Assess key exposure according to what observations an adversary could have collected. Rotation, revocation, session invalidation, and incident communication are separate decisions from binary rollback. Preserve enough non-secret evidence to reconstruct affected versions and exposure windows.

For high-integrity infrastructure, the practical deliverable is a proof-obligation ledger: what is proved, what is experimentally supported, and what remains an explicit assumption. Collapsing all three into “constant-time” makes operational decisions less reliable.

6. Continuity Hook

The next problem is composition. Even if a masking gadget satisfies a local probing property, an entire lattice implementation must preserve that property across arithmetic-to-Boolean conversions, nonlinear operations, randomness generation, compiler allocation, and concurrent execution.

Part 6 will examine compositional leakage security: masking, randomness, and the cost of preserving invariants across gadgets. The central question will be whether locally valid protections remain valid when they share a machine, a randomness source, and a lifecycle.

The conclusion of this part is narrower than “side channels break cryptography.” The mathematical assumption may remain intact while the deployed system answers a different security question. High-assurance engineering consists of making that difference explicit—and either proving that the additional observations are harmless or refusing to claim that they are.

7. References

Evidence

The documented implementation failures discussed here are KyberSlash, GoFetch, and Hertzbleed. They concern different observation mechanisms and must not be merged into one universal attack claim. The standards define algorithmic behavior; they are not evidence that an arbitrary implementation satisfies its leakage contract.

The Gaussian experiment, resource equations, and explanatory counterexamples in this article are analytical illustrations. The downloadable CSV records synthetic classification outcomes, not measured device traces. The diagrams describe obligations and interfaces, not verified implementations.

Checklist

• Define public inputs, secret state, authorized outputs, and declassification before reviewing timing.
• Specify the observer, online-query budget, physical access, and key lifetime.
• Separate functional, leakage, compiler, composition, and erasure obligations.
• Inspect the final target artifact and document instruction and hardware assumptions.
• Record statistical-test classes, sample counts, stopping rules, and limitations.
• Validate memory and randomness budgets under actual concurrency.
• Reassess evidence when the artifact or execution environment changes.

Further reading

1. Almeida et al., Verifying Constant-Time Implementations (USENIX Security 2016): relational verification and product-program reasoning.
2. KyberSlash: Exploiting Secret-Dependent Division Timings in Kyber Implementations: concrete instruction-level leakage in lattice code.
3. GoFetch: data memory-dependent prefetchers and the architectural observation boundary.
4. Hertzbleed (USENIX Security 2022): frequency scaling and timing observations.
5. Micali and Reyzin, Physically Observable Cryptography: formal treatment of physical observations.
6. Ishai, Sahai, and Wagner, Private Circuits: probing-model foundations.
7. dudect: practical statistical timing analysis.
8. Jasmin constant-time checking, version 2026.03.2: explicit distinctions among leakage models.
9. pqm4: platform-specific evaluation of post-quantum implementations.
10. FIPS 203: ML-KEM: decapsulation and implicit rejection.
11. FIPS 204: ML-DSA: standardized lattice signatures.
12. CRYSTALS-Dilithium specification, version 3.1: design rationale and rejection sampling.