RESULTS.md (3844B)
1 # Spike 1: Penumbra on x86_64-linux 2 3 Target: Penumbra's audit library (research/corpus/penumbra/harness), 4 the engagement's own build and the same build with line tables. The 5 harness calls each root on random secrets (`harness.c`). Ground 6 truth: elenchus's verdicts on the same roots (442 subjects; 79 7 leaks, 330 benign, 20 validation, 12 negligible, 1 unresolved; about 8 $32, then $16 more on the 887-subject x86 extension, unfinished). 9 10 ## Cost 11 12 Every run is a derivation built on pollux. 13 14 - memcheck taint (`vestigia run`, four calls per root): about one 15 second per root. 16 - Differential traces (`vestigia record` and `diff`, three 17 processes of two calls each, differing only in the secrets): about 18 two seconds per root. 19 - No model calls. 20 21 ## What each instrument found 22 23 memcheck taint (12, 12, and 18 secret-dependent sites; none on an 24 address): 25 26 - `MontConfig::from_bigint` (montgomery_backend.rs:359) and the 27 BigInt `cmp` / `ge` it reaches (mod.rs:565, 475): the modulus 28 compares, in the secret's decoding and in `Fr::add` and `Fr::mul` 29 when signing. 30 - `mul_projective`'s bit iterator (bits.rs:32, skip_while.rs:50): 31 the double-and-add, about 245 secret-dependent iterations per 32 scalar multiplication. 33 - `Fr::from_bytes_checked` (fr.rs:102): the secret's canonicality 34 check. 35 36 Differential traces (44, 45, and 72 origins; about 1380 37 instructions downstream; with the guest's entropy seeded and a 38 control repeating the first secret, none unsteady, so the 39 `invsqrt` lookups are the secret's and not hashbrown's random 40 seeding): 41 42 - The double-and-add (bits.rs:25, 32; skip_while.rs:50). 43 - The modulus compares inside every field operation on the point's 44 coordinates: `Fq::mul`, `square`, `add`, `sub`, the projective 45 `add_assign` and `double_in_place` (mod.rs:475, 565; group.rs:192; 46 wrapper.rs). 47 - decaf377's `invsqrt` lookups (invsqrt.rs:113-152, through 48 hashbrown's `get_inner`) as address origins. 49 - `vartime_compress_to_field` (sign.rs, mod.rs:702). 50 - `from_le_bytes_mod_order` and `Fr::add`. 51 52 ## Against elenchus 53 54 elenchus's 79 leaks fall in thirteen functions: hashbrown 55 `get_inner` (17), projective `add_assign` (9), the encoding (9), 56 `double_in_place` (8), `from_bigint` (6), `Fr::add` (6), `Fr::mul` 57 (5), `Fq::mul` (5), `Fq::square` (4), `from_le_bytes_mod_order` 58 (3 + 3), `mul_projective` (2), `sqrt_ratio` (2). Each has a 59 vestigia site in the same function, with its source line; the 60 union of the two instruments covers all of them. 61 62 ## What the two instruments are 63 64 - memcheck propagates secrecy through data, not control. After the 65 double-and-add branches on secret bits, the point it builds from 66 public multiples is defined, so nothing downstream of it is 67 flagged: the field operations' compares and the `invsqrt` lookups 68 go unseen. The first secret-dependent branch masks the leaks 69 after it. 70 - Differential traces see what control flow does to data, but only 71 what the chosen secrets vary: the canonicality check takes the 72 same direction for every valid secret, so no two runs differ 73 there, though its condition reads the secret. 74 - An origin is a branch whose outcomes differ in proportion between 75 runs (a loop whose trip count the secret sets is one) or an 76 instruction run equally often whose addresses differ. A 77 count-only rule missed the double-and-add, whose loop runs a 78 different number of times. 79 80 ## Caveats 81 82 - The line-table build is not byte-identical to the audited one: 83 the debug setting enters the crate's metadata hash, renaming 84 symbols and shifting inlining in 16 of 546 functions. Both builds 85 give the same findings by function; source lines come from the 86 line-table build. The audited artifact should itself carry line 87 tables. 88 - x86_64 only. QEMU runs aarch64 code on pollux too, for the 89 differential traces; memcheck needs a native aarch64-linux host.