Verifying an eSIM attestation, from the ML-DSA arithmetic up

Amar Akshat · github.com/amarshat

Post-quantum signatures are going into secure elements before the implementations have settled. A one-character change in a deployed ML-DSA crate’s hint decoder, < to <=, made it accept non-canonical signatures. It passed the test vectors and became CVE-2026-24850. That is the gap between “tested” and “correct on all inputs”, and it is why we check the code against the spec instead of trusting the vectors.

We are building Q-SEAL, an eSIM attestation layer: a key inside the secure element signs a challenge-bound statement, and the suite is hybrid, ECDSA P-256 and ML-DSA-44, both required. The point of this post is that more of the path is checked than just the signature primitive. Everything below is in the repository and reproduces from a make target.

What is proved

The ML-DSA reference C (PQClean, unmodified) computes the FIPS 204 forward and inverse NTT. The proof runs from the C through SAW to a Cryptol model, then cryptol-to-isabelle lifts that model into Isabelle, and Isabelle shows the lifted model equals the FIPS 204 transform. No sorry, oops, or admit in the transform theorems. It is the toolchain Apple used on corecrypto, pointed at the reference C that everyone else derives their understanding from rather than at our own code.

On top of that, all seven protocol properties in the spec’s verification-targets list. Six are a Cryptol model of a spec rule, a C reference written to be verifiable, and a SAW proof that the C equals the model, each carrying an injected mutant the proof rejects (a sensitivity check that the proof depends on the clause it checks). The seventh is a reachability property and is checked in ProVerif instead. Each runs in a second or two:

A few are worth a sentence. The transcript is fixed-length with no optional fields, and the proof is that its serializer is injective: two different transcripts can never produce the same bytes. That is an analogous property, one layer up from where CVE-2026-24850 lived. The hybrid check leaves the two signature verifiers uninterpreted and proves the accept logic equal to “both verify, over the same transcript”; a variant that accepts on either signature fails the same proof, so the hybrid cannot quietly degrade to classical-only. The single-use proof is the first stateful one: a request whose request_id was already consumed is rejected, and a verifier that drops the consume step is shown to accept the same request twice. The evidence proof is a round-trip: splitting a blob into response fragments and reassembling recovers exactly the original bytes, while a dropped fragment fails closed rather than being silently zero-filled. The last one is different in kind: the observed-action assertion type is meant to come only from a trusted internal callback, never a handset command, so it is a reachability question. In ProVerif, with the host APDU channel attacker-controlled and the internal callback private, an observed-type signing provably happens only after the internal callback; drop the host-path guard and ProVerif finds the attack. The hybrid one, verbatim from make qseal-hybrid:

Proof succeeded! qseal_hybrid_accept
VERIFIED: qseal_hybrid_accept == vE(pk_c,tbs,sig_c) AND vM(pk_pq,tbs,sig_pq) -- both required, same transcript
MUTATION CAUGHT: the downgrade variant (accept on either signature) is REJECTED by the both-required spec

Catching the CVE

All of the above holds a design of mine to targets of mine, so here is the same method pointed at the actual bug this post opened with. CVE-2026-24850 lived in the FIPS 204 hint encoding: a decoder that used <= where the spec requires a strict < on the indices within a polynomial block, so it accepted a non-canonical signature with a repeated index. The rule is FIPS 204’s, not Q-SEAL’s. I model the decoder’s accept/reject predicate in Cryptol, write a verifiable C reference of it, and prove them equal; then the <= variant is shown to fail that same proof, on a concrete encoding with a repeated index. That is the exact defect, machine-checked and rejected (make cve-anchor):

VERIFIED: qseal_hint_canonical == Cryptol canonical (FIPS 204 hint-decode canonicity)
CVE CAUGHT: qseal_hint_canonical_lax (<= instead of <) is REJECTED by the canonical spec -- this is CVE-2026-24850 / GHSA-5x2r-hc65-25f9

The honest boundary: this checks a verifiable reference decoder of the FIPS rule, not the shipped Rust crate, whose slice access defeats the symbolic simulator. So the claim is that the method catches the CVE-2026-24850 class on a faithful reference of the same rule, not that it verifies the deployed code.

What I am not claiming

These are scoped results, and the scope matters more than the count.

The inverse NTT equivalence is proved under a non-negative input window, coefficients in [0, Q), which does not cover the signed, centered coefficients the reference actually feeds it. Extending that is open. The hybrid proof abstracts the verifiers, so it is about the acceptance logic, not whether ECDSA or ML-DSA verification is itself correct. One step in the ML-DSA chain, that the -fwrapv build has no signed-overflow undefined behavior, is argued from a machine-checked bound rather than mechanized as one theorem.

On the protocol side: the single-use proof is safety only (no double-accept), on a fixed, small store that fails closed when full and has no expiry-based eviction, and it is the sequential case, so the check-and-consume race under concurrency is assumed away, not verified. The validation proof rejects out-of-enumeration field values; it does not cover length parsing of the incoming APDU (that is upstream of the typed request it starts from) or cross-field constraints. It does now reject the one authorization case the reachability property (5) cares about: the verified C refuses a profile-observed assertion type (0x04) on the host path, which is the guard property 5 proves necessary. But property 5 itself is a symbolic (Dolev-Yao) model of the command surface, with cryptography idealized and no C == model link: it assumes the host channel is what the attacker controls and the internal callback is private, and it abstracts the applet to the assertion-type dispatch, so the code-level check and the reachability argument meet only at that one guard, not through a shared model. The evidence proof is the byte-level reassembly identity, not the APDU transport state machine and not the evidence content (that the reassembled transcript and signatures are the ones the applet signed is the binding and hybrid properties, not re-checked there). The mutants above are hand-injected, not bugs found in the wild, so catching them shows sensitivity to one clause, not adequacy. To measure adequacy I ran a systematic pass (make qseal-mutants): apply the CVE’s operator class (< vs <=, == vs !=, && vs ||, and so on) to each C reference, one mutation at a time, and rerun the matching proof. The proofs kill 39 of 41 such mutants; the two survivors are equivalent mutants (a loop bound whose extra iteration a downstream guard makes a no-op), so no proof or test could kill them. And the C references are written to be verifiable; the shipped Rust deserializer, where the CVE lived, is outside the verified set because of a tool limit on how it slices memory, so that path is covered by tests, not a proof, and the repo says so. The CVE anchor above checks the FIPS rule on a reference decoder, which is why it catches the bug class rather than the exact crate.

Everything above reproduces from a make target. The primitive chain has 341 Isabelle lemmas (most are supporting lemmas), 12 SAW proofs on the C, and 37 on the Rust.

Try it

The runnable demo needs only Rust, no proof toolchain. It signs the verified transcript with real ECDSA P-256 and ML-DSA-44 and walks six outcomes: a valid attestation accepts; a tampered transcript rejects; a downgrade (valid classical signature, no valid post-quantum one) rejects; a replayed request rejects; a malformed request is refused before signing; and fragmented evidence reassembles exactly, while a dropped fragment is rejected. The demo binary is not itself verified; each piece is a Rust twin of a rule proved in the SAW scripts.

git clone https://github.com/amarshat/pqc-assay
cd pqc-assay/qseal/demo
cargo run

The proofs reproduce from make targets (make qseal-tbs qseal-ref qseal-assert qseal-hybrid qseal-nonce qseal-validate qseal-evidence, a second or two each, need cryptol and SAW). The ML-DSA primitive chain (make verify) needs the pinned SAW + Isabelle toolchain; see the repo’s setup script.