RESULTS.md (1761B)
1 # Spike 3: ppad-secp256k1 on x86_64-linux 2 3 Target: ppad-secp256k1 0.5.8 (fdb80d5), GHC 9.10.3 with LLVM, as 4 released and with the elenchus vector's mutants: S1 a direct, 5 secret-indexed window load in `mul_wnaf#`; S2 a branch on each 6 ladder scalar bit (GHC's compilation of a Bool-to-choice helper on 7 aarch64); S3 a zero-byte shortcut on the key in Schnorr's xor. The 8 harness derives a public key, signs (Schnorr and ECDSA, with and 9 without a precomputed context), and runs ECDH, under fresh secret 10 keys and auxiliary randomness. 11 12 ## Cost 13 14 About 3.8 seconds per memcheck trace (two keys, every root) and 15 3.1 seconds per three-run diff, on pollux. 16 17 ## Findings 18 19 - release: no differential origin in the harness binary. memcheck 20 reports 17 sites, each a validation or declassification the 21 vector labels as such: scalar range and result checks in `mul`, 22 `mul_wnaf`, and the signers, `even_y_vartime` on points that 23 become public, ECDH's `z == 0` result, and the harness's own case 24 analysis of Maybe results. 25 - mutants: 26 - S1: 24 address sites in `mul_wnaf`, by both instruments. 27 - S2 and S3: absent, and rightly. `mul` has ten conditional 28 jumps in both builds (the bit test compiled branch-free), and 29 the Schnorr signer has fewer in the mutant than in release (185 30 against 192: LLVM folded `if x == 0 then y else x ^ y` into the 31 XOR it equals). Their leaks are in aarch64's machine code, where 32 the vector was labelled, not x86's. 33 34 ## What this says 35 36 vestigia judges the machine code built, as the audit must: 37 compiler-level leaks are per ISA. Seeing S2 and S3 needs aarch64 38 traces. QEMU runs aarch64 code on pollux, so differential traces 39 need only an aarch64-linux build of the harness; memcheck needs a 40 native aarch64-linux host.