###################################################################
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.

.. contents::
   :local:
   :depth: 2

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 :doc:`countermeasures/ecdsa_ecdh` (table:
  *Verification artefact*).

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

Methodology
-----------

The technique was first described by Adam Langley in 2010
:cite:`langley2010ctgrind`. 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
:cite:`geimer2024_ct_tools_usability` 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:

1. ``silentops::ct_grind::poison`` / ``unpoison`` already exist
   and emit the Valgrind client requests via inline ``asm!``.
   Arcana uses these unchanged.
2. 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.
3. ``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).
4. ``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
---------------------------------------------

.. list-table::
   :header-rows: 1
   :widths: 25 50 25

   * - 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
:cite:`reparaz2017dudect`. 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:

.. code-block:: bash

   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
:doc:`countermeasures/ecdsa_ecdh`):

* ``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
==================

* :doc:`primitives` — the silentops side of the verification
  toolchain (poison/unpoison primitives, dudect surface).
* :file:`doc/infra/ctgrind.md` — the operator runbook (shared with
  quantica, when arcana adopts it).
* :doc:`biblio` — references for the verification techniques.