Verification methodology

Claims in the previous chapters are only as strong as the evidence that the code in arcana actually behaves the way those chapters describe. This chapter catalogues the evidence artefacts the project intends to maintain and how they are produced.

The methodology is shared with quantica: the silentops crate provides the verification primitives, and the operator-facing runbook (doc/infra/ctgrind.md) is the same on both sides. The content below is the arcana-specific application.

Two complementary techniques will be used:

ctgrind — Valgrind memcheck client-requests applied to a dedicated test binary. Covers control-flow and memory-access constant-time properties, run on the host CI.
silentops::verify (dudect) — statistical timing test, run on the target hardware. Covers microarchitectural timing properties (cache, branch predictor, variable-latency instructions).

Neither alone is sufficient; both are required for a credible CT assurance story. A third-party evaluator will expect both classes of evidence in the documentation pack.

Current state (2026-04-21)

ctgrind harness: built for quantica (quantica_bench/src/bin/ctgrind.rs). An arcana-side mirror is item T3-A.
dudect harness: silentops::verify is in place; arcana tests have not yet been wired into a per-algorithm harness. Item T3-B.
Release-asm verification: cargo rustc --release ... --emit=asm followed by branch-counting on the curve-arithmetic functions is the current form of arcana CT evidence, executed manually on commit 76191c1. The expected branch counts are documented in ECDSA / ECDH — countermeasures (table: Verification artefact).

ctgrind (Valgrind memcheck) — control-flow CT (`T3-A`)

Methodology 

The technique was first described by Adam Langley in 2010 [Lan10]. A memory buffer holding a secret is marked undefined via the Valgrind make_mem_undefined client request. Any subsequent conditional branch, pointer dereference, or syscall argument that consumes bits of the undefined buffer raises a memcheck error — i.e. any control-flow or addressing decision that depends on the secret is reported.

Because memcheck propagates definedness through pure arithmetic, masked bitwise selects (b ^ (mask & (a ^ b))) do not raise errors; only the downstream use of their result in a branch or load does. A correctly written CT primitive therefore passes ctgrind cleanly; a bug such as a pointer-CMOV → load triggers an error on the load.

A 2024 evaluation [GVR+24] of ctgrind, dudect, MicroWalk and ct-verif concludes that ctgrind has the best effort/discovery ratio of the four — the integration is trivial (one client request per secret buffer; no patches, no custom build) and the false-positive rate is low for properly written code.

Implementation route in arcana 

Mirror the quantica side:

silentops::ct_grind::poison / unpoison already exist and emit the Valgrind client requests via inline asm!. Arcana uses these unchanged.
New arcana_bench companion crate (mirror of quantica_bench) with a src/bin/ctgrind.rs driver. The driver poisons the truly secret portions of each typed key (skipping public components like ek-derived material), runs the full keygen / sign / verify or encrypt / decrypt round-trip per parameter set, then unpoisons before asserting correctness.
tools/ctgrind.sh — already exists workspace-wide; the arcana-side arcana flavour will be added as a new mode (tools/ctgrind.sh arcana running all primitives; tools/ctgrind.sh arcana <algo> for individual runs).
tools/ctgrind.supp — same suppression file format as quantica; each justified suppression carries an inline threat-model paragraph.

Per-primitive scope of the arcana ctgrind run 

Primitive	What is poisoned (= secret)	Expected status (post T1, T2)
`cipher::aes::Aes*`	16/24/32-byte key (after T1-A: round keys derived from the 8-block bitsliced state)	`T1-A` mandatory before this is meaningful
`cipher::modes::Gcm` decrypt	Tag bytes received from the wire	`ct_eq` already in place; expect 0 findings
`cipher::ccm` decrypt	Tag bytes	Same; expect 0 findings
`cipher::xts::AesXts` encrypt/decrypt	The key-pair (data key + tweak key)	Inherits `T1-A` status
`cipher::chacha20poly1305` decrypt	Tag bytes	`ct_eq` already in place; expect 0 findings
`mac::ctx::Mac::sign` / `verify`	Key bytes	HMAC-SHA-2 path: 0 control-flow findings (CDPA is power, not control-flow). Post `T2-D`: same.
`rsa::rsa::rsa_decrypt_raw` (CRT path)	`RsaSecretKey` `BigInt` storage	Pre-T1-C, T1-E: expected findings. Post: 0 (or documented suppressions only)
`ecc::curves::Curve::sign_rfc6979` / `sign_random` / `ecdh`	`SecretKey.bytes`	Post-76191c1, pre-T1-B: spot run pending; expected 0 on the ladder; may surface findings in `rfc6979_k` / `reduce_mod_n`
`ecc::eddsa::ed25519_sign`	`Ed25519SecretKey` 32 bytes	Pre `T1-F`: audit pending; spot run will set the baseline
`ecc::x25519::x25519_ecdh` / `x448::x448_ecdh`	sk 32-byte / 56-byte arrays	Pre `T1-G`: audit pending

Each primitive is run for every parameter set and the result is recorded in doc/analysis/arcana_ctgrind_<date>.md (mirror of the quantica ctgrind-evolution.md artefact).

dudect (statistical timing) — microarchitectural CT (`T3-B`)

Methodology 

The shared silentops::verify module implements the dudect methodology of Reparaz, Balasch & Verbauwhede [RBV17]. The harness:

Calls the cryptographic function in two classes — fixed input and random input — interleaved.
Measures CPU cycles per call via rdtsc (or the equivalent on aarch64 / RISC-V).
Computes a Welch’s t-statistic between the two timing distributions.
A |t| < 4.5 after ~10⁶ samples is considered passing (p < 10⁻⁵).

Per-primitive harnesses planned for arcana 

scalar_mul_point — fixed-vs-random scalar on each of the 7 short-Weierstrass curves. First priority: closes the hardening loop opened by commit 76191c1.
rsa_decrypt_raw (CRT path) — fixed-vs-random ciphertext. Required for T1-C (Aumüller) acceptance.
AEAD decrypt tag-check on each AEAD mode — fixed-vs-random tag. Regression test on the ct_eq chain.
Once T1-A lands: fixsliced AES round function — fixed-vs- random key.

Each harness is a separate example under arcana_bench/examples/dudect_<primitive>.rs and is wired into the tools/ script set.

Microarchitectural caveat 

dudect detects timing leaks on the actual hardware the harness runs on. A pass on x86_64 desktop does not guarantee a pass on Cortex-M0 — the latter has its own pipeline and branch-prediction quirks. A third-party evaluation lab will likely re-run the harness on the target silicon; arcana ships the harness, not the evidence on every target.

Release-asm branch counting (current evidence)

Until T3-A and T3-B land, the project’s CT evidence is release-asm branch counting on key functions, executed manually with:

cargo rustc -p arcana --release --lib -- --emit=asm -C opt-level=3
ASM=target/release/deps/arcana-*.s
for sym in $(grep -oE '_ZN6arcana3ecc5curve[0-9]+[a-z_]+17h[0-9a-f]+E' $ASM | sort -u); do
    n=$(awk "/$sym:/,/^\\.Lfunc_end/" $ASM | grep -cE '\bj(e|ne|z|nz|l|le|g|ge|a|b)\b')
    echo "$n  $sym"
done | sort -rn

Expected counts post-commit 76191c1 (documented in ECDSA / ECDH — countermeasures):

scalar_mul_point: 1 (loop counter only)
point_double: 0
point_add_ct: inlined, 0 point-value branches
point_add (verify, public): 6
double_scalar_mul (verify, public): 2

A regression on these counts (especially the 0 entries) means LLVM has reintroduced a secret-dependent branch and must be investigated immediately — that is the most direct CT regression indicator we currently have.

Forward references 

Shared side-channel primitives — silentops — the silentops side of the verification toolchain (poison/unpoison primitives, dudect surface).
doc/infra/ctgrind.md — the operator runbook (shared with quantica, when arcana adopts it).
Bibliography — references for the verification techniques.