Skip to content

verify: Valgrind taint, fuzz targets, Kani harnesses and dudect for ORE v2 - #100

Merged
coderdan merged 35 commits into
feat/ore-v2-chainedfrom
verify/ore-v2-dynamic-evidence
Oct 12, 2026
Merged

coderdan merged 35 commits into
feat/ore-v2-chainedfrom
verify/ore-v2-dynamic-evidence

Conversation

@coderdan

@coderdan coderdan commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Dynamic and formal evidence for the v2 ORE implementation, on top of the chained-scheme PR, so reviewers of the stack have more than the static analyses to read. Four kinds, each reproducible from the repo, plus the write-up in docs/reviews/2026-10-09-ore-v2-dynamic-verification.md with every result. The review of this PR also produced a set of hardening fixes, listed below.

Changes

Evidence

  • Valgrind taint harness (packages/ct-taint, scripts/ct-taint.sh, CI job on x86_64 and aarch64): key and plaintext marked undefined, every v2 encryptor run under memcheck; the job fails on any secret-dependent branch or address not listed, with its reason, in valgrind.supp. The file has no entries. The two classes it once held (the A4 Fisher–Yates swap, and the range check on the plaintext symbol in oblivious_lookup with its callers' Result test) were both removed at the root, the first by the oblivious PRP builder in the base PRs, the second here.
  • Fuzz targets (packages/ore-rs/fuzz, scripts/fuzz.sh, CI job): the chained, Bit6 and legacy parsers (full, left-only and right-only) and raw comparators must never panic on arbitrary bytes, and accepted bytes must round-trip. Seed corpora committed. fuzz.sh builds only the targets it runs, takes the list from cargo fuzz list, and runs every target even after one crashes.
  • Kani harnesses (17, all verified) for the pure building blocks: the constant-time selects equal their indexed versions, oblivious_lookup returns table[i] for every symbol, Symbol::<64>::from_low_bits stays in the domain, the 6-bit decomposition matches its bit specification and is injective and order-preserving for any two lengths, the CMAC block encodings are injective and disjoint over their full domains, gf128_double matches NIST dbl, lemire_draw itself reads the right draw and reduces it into range, the reference builder yields a permutation with a correct inverse, and the SWAR oblivious builder equals the reference (first six draws symbolic). Fifteen run in CI (8 m 50 s on an M1 Max; the job has a 30-minute timeout). The two heaviest, exhaustive-length ct_select_byte and SWAR equivalence, sit behind kani-full and run by hand: the SWAR harness was cancelled on GitHub's runners on five of six runs.
  • Builder equivalence tests: Kani cannot model the NEON and SSSE3 intrinsics, so the shipping builders are tested against the reference on every step with every swap index (2 079 forced draws) plus random and edge streams, on x86_64 (test.yml, SSSE3) and on an aarch64 runner (verify.yml, NEON).
  • dudect benches (packages/ct-dudect, run by hand; a ct-bench feature on ore-rs exposes the PRP builders for the isolated benches). CT_DUDECT_DIT=1 now applies DIT in every bench, checks that the bit stuck, and builds on aarch64 Linux.

Fixes

  • Legacy raw comparator, malformed lengths. OreAes128::compare_raw_slices panicked on two empty slices (nonce-size underflow) and could slice past the end on a partial block; found by the fuzzer on its first run. Now None for any length that is not n·(1 + 16 + 32) + 16. n = 0 (a nonce-only ciphertext of a zero-byte plaintext) is accepted and compares Equal, as the parsed comparator does.
  • First-difference latch everywhere. The legacy comparators (raw and typed) and the Bit6 typed Ord still loaded xt[l], f[l] and right[l] after the scan, indexed by the first differing block: the timing channel of finding 1, already fixed for the Bit6 raw and chained comparators in their PRs. All five latch sites now share width::FirstDiff, which latches during the scan and zeroizes the copies on drop. Wire formats unchanged.
  • Typed in-domain Symbol. Prp::permute, invert and indicator_mask_xor take a Symbol<D> and are infallible, so the lookup has no range branch on the secret. Blocks6 carries 6-bit symbols: decomposition builds it by masking, and callers passing raw symbols to Bit6 OreCipher::encrypt* or chained encrypt_var/encrypt_left_var are checked once at entry (still OreError::PrpError; this replaces a debug_assert). Ciphertexts unchanged.

Findings (details and numbers in the doc)

  1. Comparator timing revealed the first differing block (chained t = −248 over 154 M samples). Fixed: Bit6 raw and chained in their scheme PRs, the legacy and typed comparators here.
  2. The PRP builder's time depended on which permutation it builds (up to t = 83 for particular stream pairs). Fixed by the oblivious builder in the base PRs; fixed-A-versus-B now stays under |t| = 2.
  3. oblivious_lookup's range check was a branch on the plaintext symbol. Fixed here by Symbol; no taint suppressions remain.
  4. Open: prp_build_const_vs_random shows a small residual on the NEON builder (t = +7.7, tau 0.0005). The classes differ only in content, so a content-dependent effect such as the data memory-dependent prefetcher is the candidate; the next step is a DIT run on an M3+ core.

Verification

  • scripts/ct-taint.sh, no suppressions: all four modes pass in an arm64 container (NEON builder) and an amd64 container under emulation (SSSE3 builder), with byte-identical left ciphertexts across the two. Negative control: the commit before the Symbol change, with the same empty suppression file, fails all four modes, every report being the range check.
  • scripts/fuzz.sh 45: 43 M / 37.6 M / 23 M / 16.5 M runs clean (the last after the legacy fix).
  • cargo kani -p ore-rs: the 15 default harnesses verified, 8 m 50 s on an M1 Max; the kani-full pair verified earlier (519 s and 872 s on an M4). Mutation checks: padding the decomposition with ones fails the cross-length order harness and property; reading the Lemire draw big-endian fails the lemire_draw harness.
  • scripts/fuzz.sh 20 in an arm64 container: all four targets clean, 5.7 M to 13.1 M runs each, including the new right-only parses.
  • cargo test -p ore-rs --all-features (lib, wire-vector and integration tests), cargo clippy --workspace --all-targets --all-features -- -D warnings, cargo fmt --check; ct-dudect, ct-taint and the fuzz crate build.
  • ct-dudect builds and runs with DIT on aarch64 Linux; the previous msr DIT, #1 failed to assemble there.

Review notes

Every finding from the review of this PR is addressed. Two of them needed correcting: there is no VarLeft::from_slice (the chained left-only query is read as raw bytes by compare_left_to_full, which chained_compare fuzzes), and the NEON/SSSE3 builders cannot be model-checked, so their coverage is the every-swap tests above.

Still open: the prp_build_const_vs_random residual (finding 4 above); the ct-bench hooks' pin test runs only with --features ct-bench, which test.yml does not pass; and the recorded iso_swap_* timings predate the hooks' switch to lemire_draw, which also wipes its copy of each draw.

@coderdan

coderdan commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Rebased onto the updated #83 (with lease). Two changes:

Finding 2 (PRP builder timing depends on the permutation built) is still open and recorded in 4.2.

@coderdan
coderdan added this pull request to stack #93 October 9, 2026 05:03
@coderdan
coderdan force-pushed the verify/ore-v2-dynamic-evidence branch from c289942 to ead655f Compare October 9, 2026 08:53
@coderdan

coderdan commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Rebased onto the updated #83 (with lease). Finding 2 (PRP builder timing depends on the permutation built) is fixed in #82 and #83; this PR carries the evidence:

  • docs/benchmarks/2026-10-09-oblivious-prp-results.md (ead655f): method, mechanism isolation, builder micro, end-to-end and dudect before/after, all on mains power (a first pass in Low Power Mode gave the same ratios).
  • Verification doc (4e24c19): §4.2 marks finding 2 fixed with the isolation and before/after tables; §1 drops the a4-fisher-yates-secret-indexed-swap Valgrind suppression, since the swap no longer exists. The ct-taint job on this run is the first execution without it; by construction the builders touch memory only at public offsets (stream reads, final stores) and use the draws as register operands, which memcheck tracks as data, not addresses.
  • ct-dudect (5247538): isolation benches (swap-only secret vs public control, fill-only secret vs public) and per-builder benches through from_stream_with, behind ct-bench.
  • Criterion builder bench (77dbcd5), benches/prp_build.rs, --features ct-bench.
  • Kani (ac3f3b1): under cfg(kani) the dispatch goes to SWAR; a new harness proves the SWAR builder equals the reference builder for a bounded symbolic stream (872 s), and the existing permutation proof now targets the reference builder, with the equivalence harness carrying the property over. The default cargo kani run grows by about 18 minutes; if that is too much for CI, the equivalence harness can move behind kani-full.

Open: SSSE3 untimed on real x86; docs/reviews/2026-06-16-constant-time-analysis-pr79.md (CT-3, in #81) now reads as stale on the MemJam residual and should get a one-line pointer to the brief's A4 status.

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🟡 Changes recommended

The legacy comparator rejects valid zero-block ciphertexts produced by the public PlainText<0> API, and the PR description conflicts with the committed verification account.

2 open findings
What changed in this PR

Adds reproducible fuzzing, taint analysis, Kani proofs, and dudect benchmarks for ORE v2, alongside legacy comparator hardening and verification documentation.

Changes:

  • Adds CI-backed Valgrind, fuzzing, and Kani verification.
  • Adds formal harnesses and timing-benchmark hooks.
  • Fixes malformed-length handling in the legacy comparator.
File Description
scripts/​fuzz.sh Runs fuzz targets.
scripts/​ct-taint.sh Runs Valgrind taint checks.
packages/​ore-rs/​src/​scheme/​width.rs Adds selection proofs.
packages/​ore-rs/​src/​scheme/​decompose.rs Adds decomposition proofs.
packages/​ore-rs/​src/​scheme/​bit2.rs Hardens legacy comparison.
packages/​ore-rs/​src/​primitives/​prp/​oblivious.rs Enables Kani and benchmark builders.
packages/​ore-rs/​src/​primitives/​prp.rs Adds PRP proofs and hooks.
packages/​ore-rs/​src/​primitives/​hash.rs Proves GF doubling.
packages/​ore-rs/​src/​primitives/​cmac.rs Proves block encodings.
packages/​ore-rs/​src/​lib.rs Exposes timing hooks.
packages/​ore-rs/​fuzz/​fuzz_targets/​chained_parse.rs Fuzzes chained parsing.
packages/​ore-rs/​fuzz/​fuzz_targets/​chained_compare.rs Fuzzes chained comparison.
packages/​ore-rs/​fuzz/​fuzz_targets/​bit8_parse.rs Fuzzes legacy parsing.
packages/​ore-rs/​fuzz/​fuzz_targets/​bit6_parse.rs Fuzzes Bit6 parsing.
packages/​ore-rs/​fuzz/​corpus/​chained_parse/​d9e816fb2b510edc9434e954a29a1f7a9bfab1b7 Adds parser seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​f4855d9e4dd28214677e20d52b5969d88be8c692 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​de6b6d078e2249a744cb5e103557d22cd9c75dd9 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​d870ec0cc1724a182044c97ba3c7870a2f28da8e Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​c190bddafec30d2016a482c9ae390ac59e1ab36b Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​ae0b7e44403af4ef918f37a4a254c47bc69195b1 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​749e715bf58ab2b3a134353ef1f123611c5ec337 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​712e27f64b93cf7fd2b7c09e7354a3fcf22d4158 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​6f1e8d7fa8c2dc39d5df3248c0fce695b170fb5e Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​4766af07390d4fb62682fd6658fdf3caaeab97f2 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​245f6e3cdedbf18b1a839a9c43c109b1711c9d50 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​chained_compare/​1fd2e9fcf01c1736b15e7226e7676b19c04616c1 Adds comparator seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​f683fb5ae87e6044c802b30a3fb58c0bdcb350be Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​f11684a34515cd7d5c708ae44def7a4163aa1074 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​eaf3021dbdc5feeaba63175d7006d9523d8fc465 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​e7dd041512c660ccd0f4f63daf0414497b8b7be2 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​c77f05e9e9648c99adb66235e1b87715da99309f Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​c6b504a181054b9c9bff07e9461d1a6ea2dafc1b Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​867f9d66dcbce6ae39342dd2fc04ac219dbb2a16 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​79a4d9f793276a51378df429e0ebf837c8aadc07 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​5d3671d6fd79c556777376b9db9eeb1238286cbe Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​5b55ec37559bb110228a6591713076b7fa2ce5e8 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​57b635ecfa2d621d1059ddf560e330fcef2e1ab4 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​4ec9aa556c92fb471e8a47817b673a9a3d1f278f Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​1bc7c470785e9b20b5e6b476a2cab9876a16117b Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit8_parse/​1a1169b85b4da2d2e7d6a40d0a92ea304871c898 Adds legacy seed.
packages/​ore-rs/​fuzz/​corpus/​bit6_parse/​89096f0b81069aba25c5349783bb4861c03c20c2 Adds Bit6 seed.
packages/​ore-rs/​fuzz/​corpus/​bit6_parse/​500083da360656944aa064d1b2c3892f5ce76927 Adds Bit6 seed.
packages/​ore-rs/​fuzz/​Cargo.toml Defines detached fuzz crate.
packages/​ore-rs/​fuzz/​Cargo.lock Locks fuzz dependencies.
packages/​ore-rs/​Cargo.toml Adds verification features and benchmark.
packages/​ore-rs/​benches/​prp_build.rs Benchmarks PRP builders.
packages/​ct-taint/​valgrind.supp Documents accepted reports.
packages/​ct-taint/​src/​main.rs Implements taint harness.
packages/​ct-taint/​Cargo.toml Defines taint crate.
packages/​ct-taint/​Cargo.lock Locks taint dependencies.
packages/​ct-dudect/​src/​main.rs Implements timing tests.
packages/​ct-dudect/​Cargo.toml Defines dudect crate.
packages/​ct-dudect/​Cargo.lock Locks dudect dependencies.
docs/​reviews/​2026-10-09-ore-v2-dynamic-verification.md Records verification results.
docs/​benchmarks/​2026-10-09-oblivious-prp-results.md Records PRP benchmarks.
.gitignore Ignores verification outputs.
.github/​workflows/​verify.yml Adds verification CI jobs.

🧠 Review effort: Balanced


💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

Comment thread packages/ore-rs/src/scheme/bit2.rs Outdated
Comment thread docs/reviews/2026-10-09-ore-v2-dynamic-verification.md
coderdan added a commit that referenced this pull request Oct 9, 2026
… comparators; accept zero-block legacy input

The legacy compare_raw_slices and the typed Ord impls for OreAes128 and
Bit6 still loaded xt[l], f[l] and right[l] after the scan, indexed by the
first differing block l. The right blocks are the one region the scan
never touches, so their cache state reveals l to a timing observer — the
channel measured for chained (t = -248) and already fixed in the Bit6 raw
and chained comparators. All three now latch those values during the scan
with ct_assign_bytes. Wire format unchanged.

The legacy length guard also refused a nonce-only input, which is the
valid ciphertext of a zero-byte plaintext and parses with
CipherText::<_, 0>::from_slice. The raw comparator now returns Equal for
it, matching the typed one; a regression test pins the agreement.

Addresses PR #100 review findings 1 and 2.
coderdan added a commit that referenced this pull request Oct 9, 2026
… comparators; accept zero-block legacy input

The legacy compare_raw_slices and the typed Ord impls for OreAes128 and
Bit6 still loaded xt[l], f[l] and right[l] after the scan, indexed by the
first differing block l. The right blocks are the one region the scan
never touches, so their cache state reveals l to a timing observer — the
channel measured for chained (t = -248) and already fixed in the Bit6 raw
and chained comparators. All three now latch those values during the scan
with ct_assign_bytes. Wire format unchanged.

The legacy length guard also refused a nonce-only input, which is the
valid ciphertext of a zero-byte plaintext and parses with
CipherText::<_, 0>::from_slice. The raw comparator now returns Equal for
it, matching the typed one; a regression test pins the agreement.

Addresses PR #100 review findings 1 and 2.
@coderdan
coderdan force-pushed the verify/ore-v2-dynamic-evidence branch from 9c88299 to e2c646b Compare October 9, 2026 10:22
@coderdan

coderdan commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Rebased (with lease) onto the docs-only sign-off updates in #82 and #83. The comparator-hardening commit that was pushed here (latch in the legacy and Bit6 typed comparators, zero-block legacy input) is kept unchanged in content; it is now re-signed as part of the rebase.

coderdan added a commit that referenced this pull request Oct 9, 2026
…uppressions

oblivious_lookup range-checked the secret plaintext symbol before its
constant-time scan, and every encryptor tested the Result with `?`.
Memcheck reported both as secret-dependent branches, accepted in
valgrind.supp through a glob over every `?` on a Result<u8, PrpError>,
which would also have hidden any future secret-dependent error path
(PR #100 review findings 3 and 15).

Remove the check at its root. Symbol<D> is a byte in the D-element
domain by type; Prp::permute, invert and indicator_mask_xor take one, so
they are infallible and the lookup has no range branch. Blocks6<B> holds
6-bit symbols: Blocks6::decompose masks while packing (no branch on the
plaintext) and feeds the OreEncrypt and string paths; Blocks6::check
validates symbols a caller passes to Bit6 OreCipher::encrypt* or chained
encrypt_var / encrypt_left_var, once at entry, and still returns
OreError::PrpError. That replaces the debug_assert those entry points
had. Ciphertexts are unchanged (wire vectors pass).

valgrind.supp now has no entries. The taint gate passes all four modes
with it on arm64 (NEON builder) and emulated amd64 (SSSE3 builder); the
previous commit with the same empty file fails all four, every report
being the range check.

Kani: the lookup harnesses now prove table[i] for every symbol, a new
harness covers Symbol::<64>::from_low_bits, and the kani-full any-length
lookup harness is dropped since out-of-range lookups are unrepresentable.
coderdan added a commit that referenced this pull request Oct 9, 2026
oblivious::build dispatches to SSSE3 on x86_64 and NEON on aarch64, so
the ct-taint job on ubuntu-latest alone never checked the builder that
ships on Arm (PR #100 review finding 7). Run it as a matrix over
ubuntu-latest and ubuntu-24.04-arm, with a per-arch cache key. Also fix
the kani-full comment: one exhaustive-length harness remains.
coderdan added a commit that referenced this pull request Oct 9, 2026
…t and taint docs

CT_DUDECT_DIT=1 only took effect through the Bit6 and chained cipher
constructors, so the nine prp_build_* and iso_* benches never ran with
DIT (PR #100 review finding 5). Every bench now calls
data_independent_timing() first, which checks FEAT_DIT, sets the bit,
and reads it back. The write uses the generic system register encoding
s3_3_c4_c2_5: `msr DIT, #1` needs the ARMv8.4 `dit` target feature and
failed to assemble on aarch64 Linux (finding 6); it now builds and runs
there.

Docs:
- The prp_build_const_vs_random residual was put down to one repeated
  input against a 256 KB pool, but the Left pool is 512 copies indexed
  at random like the Right pool, so the classes differ only in content
  (finding 4). Marked as unexplained; a DIT run on an M3+ core, where
  DIT disables the data memory-dependent prefetcher, is the next step.
- "Setting DIT changed nothing" did not cover the builder benches.
- Taint section: suppressions removed, runs on both shipping builders,
  negative control; Kani section updated for the Symbol harnesses.
@coderdan
coderdan marked this pull request as ready for review October 9, 2026 23:05
coderdan added a commit that referenced this pull request Oct 9, 2026
from_stream and the ct-bench-only from_stream_with duplicated the length
check and table construction, so a change to one (say, wiping on error)
would not reach the other and the timing hooks would time a different
function from the one the schemes call (PR #100 review finding 14).

from_stream_with is now always compiled and is the only implementation;
from_stream calls it with oblivious::build. The builder is a generic
FnOnce parameter rather than a function pointer, so the scheme path is
monomorphised and the builder still inlines.
coderdan added a commit that referenced this pull request Oct 9, 2026
…e isolation hooks

ct_bench::draw re-implemented oblivious::lemire_draw, and
permutation_for re-ran a copy of the reference builder's swap loop, so a
change to the draw offset or reduction would leave the isolation benches
timing a different permutation from the one the builders produce (PR
#100 review finding 13).

draw now calls lemire_draw (made pub(crate)), and permutation_for calls
oblivious::reference::build. fy_swaps_only keeps its own loop, since it
exists to time the swaps without the fill; a new test pins it and
inverse_fill_only to the reference builder's tables.

lemire_draw wipes its copies of the draw, which the old inline draw did
not, so the iso_swap_* benches now include that work, as the reference
builder always has. Their recorded figures predate this.
coderdan added a commit that referenced this pull request Oct 9, 2026
decompose_6bit_preserves_order only covered equal-length inputs, but the
chained scheme compares strings of different lengths: the first
differing block decides, else the shorter sorts first. That is
lexicographic order over the block arrays, and it holds only if the zero
padding of a shorter input's last block never exceeds the longer input's
real bits (PR #100 review finding 9).

The Kani harness now takes two independent lengths 0..=16 (strictly
stronger than before; 31 s on an M1 Max). Two quickcheck properties
cover unbounded lengths: arbitrary pairs, and b = a ++ tail, the case
padding could break, which random pairs almost never hit.

Mutation check: padding with ones instead of zeros fails both the Kani
harness and the prefix property; the arbitrary-pair property alone does
not catch it, which is why the prefix one is there.
coderdan added a commit that referenced this pull request Oct 9, 2026
No target parsed untrusted bytes as a right-only ciphertext, although
Right::<S, N>::from_slice reads stored bytes for both fixed-width
schemes (PR #100 review finding 10). bit6_parse and bit8_parse now parse
every input as a right half too, at the same widths, and require an
accepted one to re-encode to itself.

The finding also named VarLeft::from_slice, which does not exist: the
chained left-only query is consumed as raw bytes by compare_left_to_full,
which chained_compare already fuzzes. The doc says so.

20 s per target in an arm64 container: all four clean, 5.7 M to 13.1 M
runs.
coderdan added a commit that referenced this pull request Oct 9, 2026
… after a crash

`cargo fuzz build` with no target builds all of them, so each of the four
CI matrix jobs compiled every target; and with `set -e` the first
crashing target ended a local all-targets run (PR #100 review finding
12).

Each target is now built and run on its own (`cargo fuzz build <target>`
passes `--bin <target>`), failures are collected, and the script exits 1
at the end naming them. The target list comes from `cargo fuzz list`, so
a new target needs no edit here, and a failing listing stops the script
rather than yielding an empty run. Portable to macOS's bash 3.2.

Checked: all targets clean in a Linux container; a run where every
build fails reports all four and exits 1.
coderdan added a commit that referenced this pull request Oct 9, 2026
…uilders on their targets

The Lemire Kani harness proved an inline restatement of the formula, so a
wrong draw offset or byte order in oblivious::lemire_draw would pass it;
and the NEON and SSSE3 builders, which ship, are never model-checked
because Kani cannot model their intrinsics and dispatches to SWAR (PR
#100 review finding 8).

- lemire_draw_in_range calls oblivious::lemire_draw on a fully symbolic
  504-byte stream for every step 1..64 and checks it returns
  (x * (i + 1)) >> 64 <= i of the right little-endian draw. 113 s on an
  M1 Max. Mutation check: reading the draw big-endian fails it.
- builders_match_reference_for_every_swap forces every (i, j) with
  j <= i (2 079 draws, each inside an otherwise varied full build)
  through the dispatched, SWAR and reference builders and requires equal
  tables. This is the strongest evidence the intrinsic builders can get.
- A new verify.yml job runs the PRP tests on ubuntu-24.04-arm, where the
  dispatcher picks NEON; test.yml runs them on x86_64 only (SSSE3).
…kani-full

They prove ct_select_byte and oblivious_lookup for every table length up
to 256 and take about 16 of the full run's 22 minutes; the lengths in use
are proved by the neighbouring harnesses in seconds. CI runs without the
feature.
CT_DUDECT_POOL=4 keeps every input in L1, which separates a cache-driven
timing difference from an arithmetic one; the default 512 reflects
inputs arriving from memory.
Records the Valgrind taint run and its documented exceptions, the fuzz
results (including the legacy comparator panic they found), the 18 Kani
harnesses, and the dudect timing measurements: the chained comparator's
resolution step revealed the first differing block through an l-indexed
load that missed cache (t = -248 over 154 M samples), and the PRP
builder's time depended on the permutation it builds (small, but
measurable in-process with no SMT), which the A4 one-cache-line argument
does not cover.

Both are fixed in the stack. For the builder, isolation benches put the
whole signal in the Fisher-Yates swaps (|t| 18 to 50 against controls
under 3; the inverse fill shows none), the oblivious builder removes it
(fixed A versus fixed B from |t| 17-83 to under 2, mains power), and the
taint suppression for the swap is gone.
Times the reference builder (textbook Fisher-Yates, secret-indexed), the
byte-at-a-time and SWAR oblivious builders, and the target's dispatched
oblivious builder, each over a rotating pool of 256 random 512-byte
streams. Needs the ct-bench feature, which exposes the builders.
Mechanism isolation (the Fisher-Yates swaps carry the timing signal, the
inverse fill does not), the NEON, SSSE3 and SWAR oblivious builders, their
cost alone and end to end, and dudect before and after. Measured on an M4
on mains power with Low Power Mode off; a first pass in Low Power Mode on
battery gave the same ratios.
… comparators; accept zero-block legacy input

The legacy compare_raw_slices and the typed Ord impls for OreAes128 and
Bit6 still loaded xt[l], f[l] and right[l] after the scan, indexed by the
first differing block l. The right blocks are the one region the scan
never touches, so their cache state reveals l to a timing observer — the
channel measured for chained (t = -248) and already fixed in the Bit6 raw
and chained comparators. All three now latch those values during the scan
with ct_assign_bytes. Wire format unchanged.

The legacy length guard also refused a nonce-only input, which is the
valid ciphertext of a zero-byte plaintext and parses with
CipherText::<_, 0>::from_slice. The raw comparator now returns Equal for
it, matching the typed one; a regression test pins the agreement.

Addresses PR #100 review findings 1 and 2.
Each comparator latched xt, f and the right block of the first differing
block into plain stack arrays that were never cleared. Pull the latch and
the resolution step into width::FirstDiff<R>, which derives
ZeroizeOnDrop, so the copies are wiped on every return path including the
early Equal return.

All five latch sites use it: legacy and Bit6 compare_raw_slices and typed
Ord, and chained compare_views (shared by compare_raw_slices and
compare_left_to_full). The now-unused free get_bit helpers in bit2 and
bit2_w6 are removed; FirstDiff::resolve keeps the domain debug_assert.
…uppressions

oblivious_lookup range-checked the secret plaintext symbol before its
constant-time scan, and every encryptor tested the Result with `?`.
Memcheck reported both as secret-dependent branches, accepted in
valgrind.supp through a glob over every `?` on a Result<u8, PrpError>,
which would also have hidden any future secret-dependent error path
(PR #100 review findings 3 and 15).

Remove the check at its root. Symbol<D> is a byte in the D-element
domain by type; Prp::permute, invert and indicator_mask_xor take one, so
they are infallible and the lookup has no range branch. Blocks6<B> holds
6-bit symbols: Blocks6::decompose masks while packing (no branch on the
plaintext) and feeds the OreEncrypt and string paths; Blocks6::check
validates symbols a caller passes to Bit6 OreCipher::encrypt* or chained
encrypt_var / encrypt_left_var, once at entry, and still returns
OreError::PrpError. That replaces the debug_assert those entry points
had. Ciphertexts are unchanged (wire vectors pass).

valgrind.supp now has no entries. The taint gate passes all four modes
with it on arm64 (NEON builder) and emulated amd64 (SSSE3 builder); the
previous commit with the same empty file fails all four, every report
being the range check.

Kani: the lookup harnesses now prove table[i] for every symbol, a new
harness covers Symbol::<64>::from_low_bits, and the kani-full any-length
lookup harness is dropped since out-of-range lookups are unrepresentable.
oblivious::build dispatches to SSSE3 on x86_64 and NEON on aarch64, so
the ct-taint job on ubuntu-latest alone never checked the builder that
ships on Arm (PR #100 review finding 7). Run it as a matrix over
ubuntu-latest and ubuntu-24.04-arm, with a per-arch cache key. Also fix
the kani-full comment: one exhaustive-length harness remains.
…t and taint docs

CT_DUDECT_DIT=1 only took effect through the Bit6 and chained cipher
constructors, so the nine prp_build_* and iso_* benches never ran with
DIT (PR #100 review finding 5). Every bench now calls
data_independent_timing() first, which checks FEAT_DIT, sets the bit,
and reads it back. The write uses the generic system register encoding
s3_3_c4_c2_5: `msr DIT, #1` needs the ARMv8.4 `dit` target feature and
failed to assemble on aarch64 Linux (finding 6); it now builds and runs
there.

Docs:
- The prp_build_const_vs_random residual was put down to one repeated
  input against a 256 KB pool, but the Left pool is 512 copies indexed
  at random like the Right pool, so the classes differ only in content
  (finding 4). Marked as unexplained; a DIT run on an M3+ core, where
  DIT disables the data memory-dependent prefetcher, is the next step.
- "Setting DIT changed nothing" did not cover the builder benches.
- Taint section: suppressions removed, runs on both shipping builders,
  negative control; Kani section updated for the Symbol harnesses.
from_stream and the ct-bench-only from_stream_with duplicated the length
check and table construction, so a change to one (say, wiping on error)
would not reach the other and the timing hooks would time a different
function from the one the schemes call (PR #100 review finding 14).

from_stream_with is now always compiled and is the only implementation;
from_stream calls it with oblivious::build. The builder is a generic
FnOnce parameter rather than a function pointer, so the scheme path is
monomorphised and the builder still inlines.
…e isolation hooks

ct_bench::draw re-implemented oblivious::lemire_draw, and
permutation_for re-ran a copy of the reference builder's swap loop, so a
change to the draw offset or reduction would leave the isolation benches
timing a different permutation from the one the builders produce (PR
#100 review finding 13).

draw now calls lemire_draw (made pub(crate)), and permutation_for calls
oblivious::reference::build. fy_swaps_only keeps its own loop, since it
exists to time the swaps without the fill; a new test pins it and
inverse_fill_only to the reference builder's tables.

lemire_draw wipes its copies of the draw, which the old inline draw did
not, so the iso_swap_* benches now include that work, as the reference
builder always has. Their recorded figures predate this.
decompose_6bit_preserves_order only covered equal-length inputs, but the
chained scheme compares strings of different lengths: the first
differing block decides, else the shorter sorts first. That is
lexicographic order over the block arrays, and it holds only if the zero
padding of a shorter input's last block never exceeds the longer input's
real bits (PR #100 review finding 9).

The Kani harness now takes two independent lengths 0..=16 (strictly
stronger than before; 31 s on an M1 Max). Two quickcheck properties
cover unbounded lengths: arbitrary pairs, and b = a ++ tail, the case
padding could break, which random pairs almost never hit.

Mutation check: padding with ones instead of zeros fails both the Kani
harness and the prefix property; the arbitrary-pair property alone does
not catch it, which is why the prefix one is there.
No target parsed untrusted bytes as a right-only ciphertext, although
Right::<S, N>::from_slice reads stored bytes for both fixed-width
schemes (PR #100 review finding 10). bit6_parse and bit8_parse now parse
every input as a right half too, at the same widths, and require an
accepted one to re-encode to itself.

The finding also named VarLeft::from_slice, which does not exist: the
chained left-only query is consumed as raw bytes by compare_left_to_full,
which chained_compare already fuzzes. The doc says so.

20 s per target in an arm64 container: all four clean, 5.7 M to 13.1 M
runs.
… after a crash

`cargo fuzz build` with no target builds all of them, so each of the four
CI matrix jobs compiled every target; and with `set -e` the first
crashing target ended a local all-targets run (PR #100 review finding
12).

Each target is now built and run on its own (`cargo fuzz build <target>`
passes `--bin <target>`), failures are collected, and the script exits 1
at the end naming them. The target list comes from `cargo fuzz list`, so
a new target needs no edit here, and a failing listing stops the script
rather than yielding an empty run. Portable to macOS's bash 3.2.

Checked: all targets clean in a Linux container; a run where every
build fails reports all four and exits 1.
…uilders on their targets

The Lemire Kani harness proved an inline restatement of the formula, so a
wrong draw offset or byte order in oblivious::lemire_draw would pass it;
and the NEON and SSSE3 builders, which ship, are never model-checked
because Kani cannot model their intrinsics and dispatches to SWAR (PR
#100 review finding 8).

- lemire_draw_in_range calls oblivious::lemire_draw on a fully symbolic
  504-byte stream for every step 1..64 and checks it returns
  (x * (i + 1)) >> 64 <= i of the right little-endian draw. 113 s on an
  M1 Max. Mutation check: reading the draw big-endian fails it.
- builders_match_reference_for_every_swap forces every (i, j) with
  j <= i (2 079 draws, each inside an otherwise varied full build)
  through the dispatched, SWAR and reference builders and requires equal
  tables. This is the strongest evidence the intrinsic builders can get.
- A new verify.yml job runs the PRP tests on ubuntu-24.04-arm, where the
  dispatcher picks NEON; test.yml runs them on x86_64 only (SSSE3).
Follows c5a436e (PR #100 review finding 9): the decompose_6bit order
harness now covers any two lengths up to 16 bytes.
The Kani job ran with no timeout and has failed on five of the last six
Verify runs: the SWAR-builder equivalence harness (872 s on an M4) is
cancelled 26 to 32 minutes into its run on ubuntu-latest every time, and
the one success took 57 minutes. The 335 s from_stream length harness
(552 s in CI) proved 504 concrete cases (PR #100 review finding 11).

- The SWAR equivalence harness joins the exhaustive ct_select_byte
  harness behind kani-full, run by hand. Every CI run still tests SWAR
  against the reference on every (step, swap index) pair.
- The from_stream length check is an exhaustive unit test instead.
- timeout-minutes: 30 on the job.

The default set is now 15 harnesses: 8 m 50 s on an M1 Max, all
verified, so about 15 minutes in CI.
Four alternating 150 s continuous runs on the M4 at daf0344: DIT off
+20.4/+19.6 (tau 0.0013/0.0012), DIT on +21.6/+21.8 (tau 0.0016/0.0016).
The data memory-dependent prefetcher does not explain it; it stays open.
The fixed A vs fixed B control stays under 2.5 both ways. The original
commit (6760707), rerun in the same session, gave +31.4, so the larger
figures are the session's, not the code's.
…ilder benches

prp_build_const_vs_random's residual (+7.7 to +31 on the M4, +55 on an
M1 Max, unchanged by DIT) came from the bench, not the builder:

- Placement. Each class read from its own heap allocation. In one shared
  pool, moving the fixed stream from the even to the odd slots flips the
  sign (-12.6 to +23.5).
- Reporting. dudect's max t is the largest |t| over 101 tests, 100 of
  them cropped at runtime percentiles. A one-build sample (about 200 ns)
  takes only a handful of values on Apple's 24 MHz timer, the percentiles
  sit on those values, and where the classes differ in spread the cropped
  tests report a large t with no mean difference: +27.7 reported against
  +1.10 uncropped.

prp_build_const_vs_random now draws both classes from one pool with the
slots assigned at random each batch, and times 16 builds per sample;
prp_build_fixed_a_vs_fixed_b also times 16. On the M1 Max the corrected
bench gives uncropped t = -0.04 over 7.3 M samples per class (dudect
-1.8). The old bench stays as prp_build_const_vs_random_separate_pools,
with prp_build_const_vs_random_interleaved_even/_odd as layout controls.

scripts/dudect-uncropped.sh runs a bench continuously, streams every
sample through a FIFO into per-class histograms, and prints the
uncropped Welch t, means, spreads and tick-bin shares next to dudect's
figure. dudect-bencher writes every sample with class 0, so the classes
are recovered from row order.
Record the controls that traced prp_build_const_vs_random's residual to
input placement and dudect's percentile cropping on a coarse timer, and
the corrected bench's result (uncropped t = -0.04 on an M1 Max). The M4
rerun of the corrected bench is pending. Note that the encryptor
const_vs_random benches share the old layout and have not been rerun.
Six 150 s runs of the corrected bench at b5c8233, DIT off and on:
uncropped t +1.10, -0.61, -1.23, -0.27, +0.18, +0.47. The controls
behave as on the M1 Max: separate pools +30.4 cropped / +0.52 uncropped;
interleaved even/odd -47.3/+47.3 cropped, -2.43/+4.14 uncropped, with
mirror-image bin shifts; fixed A vs fixed B +0.59.

With DIT on only, three runs show a small repeatable tick-bin shift
(|z| up to 6.4, mean effect under 1 ns) and cropped t of +4.4 to +9.3;
recorded as unexplained.
encrypt_var and encrypt_left_var checked every symbol's domain before
encrypt_blocks enforced the u16 block limit, so oversized input cost a
scan of its whole length and could report PrpError instead of
TooManyBlocks. Check the length first.
The ct_bench module and its isolation-equivalence test compile only with
the ct-bench feature. The clippy step builds them but plain cargo test
never ran them.
…oints

The gate had no positive control. taint() discarded mark_memory's
result, and valgrind.supp was empty, so a run in which nothing was
tainted (a request that returned NoValgrind, crabgrind built without its
valgrind feature, a key kept in a register past the mark) passed exactly
like a clean one.

scripts/ct-taint.sh now sets CT_TAINT_GATE, under which:
- a taint request that fails is fatal (exit 3);
- each mode reads its output's V bits before untainting it and fails if
  every byte is defined (exit 4), so every run shows that the taint
  reached the ciphertext;
- a canary mode branches on a tainted byte and indexes a table with it,
  and the script requires memcheck to fail it.
With crabgrind's requests compiled to no-ops, every mode now fails with
exit 4 and the canary check fails. The marks also take a mutable pointer.

Coverage: the modes ran Bit6 on one u64 and the chained scheme on one
string. They now add Bit6 i64, f64 and u32 through OreEncrypt (each runs
its own to_orderable_bytes transform on the secret; u32 has 6 blocks, not
11), and the raw-block entry points of both schemes. Those report the one
branch in Blocks6::check, which is now the single named suppression, with
its reason. Blocks6::check is #[inline(never)] so that the branch has the
same frame on every target; x86_64 inlined it into a closure. The legacy
encryptor is out of scope, and verify.yml and the verification doc now say
so.

Clean on arm64 (NEON) and amd64 (SSSE3, emulated), with the canary failing
on both.
test.yml ran only on x86_64, and the one aarch64 job in verify.yml ran
only primitives::prp. So CI never ran hardware AES (--cfg aes_armv8), the
NEON lsb_mask_256 and gt_mask_xor_256 kernels, or the compat vector tests
on Arm. On x86_64, lsb_mask_dispatched_matches_scalar compares scalar with
scalar. A change that flipped a hash bit in a NEON kernel would have left
every job green while Arm hosts wrote right ciphertexts that do not
compare with x86_64 ones.

The test job now runs on ubuntu-latest and ubuntu-24.04-arm, with the
cache keyed by architecture. verify.yml's prp-builders-aarch64 job is
covered by it and removed.
Each scheme has two comparators, compare_raw_slices on bytes and Ord on
a parsed CipherText, and this stack rewrote both. The fuzz targets only
checked that the raw one does not panic. If the two disagree, a database
index and an application order the same rows differently.

bit8_parse and bit6_parse now assert, whenever both inputs parse as full
ciphertexts, that compare_raw_slices(a, b) == Some(a.cmp(&b)), at both of
each scheme's widths. Random pairs almost never both parse, so each run
also checks a against a copy of itself with b written over everything
after the header, both ways round. Antisymmetry is not asserted: it holds
only for genuine ciphertexts.

Reversing the typed comparison in the assertion makes both targets fail
within 60 seconds; the real targets ran clean for 13.8M (bit8) and 9.8M
(bit6) iterations.
ct-taint and the fuzz crate keep their own lockfiles. Rebasing onto main
moved the workspace's orderable-bytes from 0.1.1 to 0.2.0.
The verification doc named the commit the M4 runs were made at by SHA,
and every rebase of the stack rewrites it. Name it by subject instead.
@coderdan
coderdan force-pushed the verify/ore-v2-dynamic-evidence branch from 0a94d35 to 2ca0ecc Compare October 12, 2026 05:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants