IMPL1.md (3923B)
1 # IMPL1: vestigia, the leakage trace in act 2 3 ## End 4 5 Decide, for an execution of an audited function, which of its 6 instructions branched on a secret or computed an address from one, 7 and say where each sits in the source. This is the constant-time 8 discipline read off a running program: exact on the paths executed, 9 free of timing noise, and localised to the instruction. (synthesis 10 `plans/REDESIGN.md` gives the reasons.) 11 12 ## Means 13 14 valgrind's memcheck already tracks, bit by bit, which values are 15 defined. A harness marks the secret's bytes undefined before calling 16 the function (`VALGRIND_MAKE_MEM_UNDEFINED`, a no-op outside 17 valgrind) and marks its outputs defined after. memcheck then reports 18 every conditional branch whose condition, and every load or store 19 whose address, depends on a marked byte, and `--track-origins` names 20 the client request as the origin. This is the ctgrind technique. 21 22 vestigia supplies: 23 24 - `include/vestigia.h`: `vestigia_secret` and `vestigia_public`, the 25 two marks, for harness writers. 26 - `vestigia run -- PROGRAM ARGS`: runs the harness under memcheck 27 with fixed settings and writes a report. 28 - `vestigia read FILE.xml`: the same report from memcheck's XML. 29 - The report (`vestigia/trace-v1`, JSON): secret-dependent sites, 30 one per instruction and class (`control`, `address`, `syscall`), 31 with function, file, line, count, and caller stacks; errors whose 32 origin is not a secret, kept apart; and the run's provenance. 33 - A nix function that runs a harness as a derivation, so a trace 34 for x86_64-linux runs on whatever builds for it. 35 36 ## Spikes 37 38 The tool earns its place only if it reproduces known results: 39 40 1. Penumbra on x86_64-linux: the audit library rebuilt with line 41 tables (its `.text` checked identical to the audited build), a C 42 harness calling the three roots on random secrets. Do the 43 findings cover elenchus's leaks (ark-ff modulus compares, 44 decaf377 invsqrt table lookups, the double-and-add)? 45 2. ppad-poly1305 with the planted mutants, and ppad-secp256k1 as a 46 constant-time control: are the planted leaks found, and does 47 the GHC runtime stay quiet once origins are filtered? 48 49 ## Constraints 50 51 - Haskell2010, boot libraries only (base, bytestring, containers, 52 text, process, directory, filepath); tasty for tests. 53 - memcheck XML is parsed by a small reader of our own; JSON is 54 written by a small encoder of our own. 55 - valgrind enters through nix as a tool. It does not run on Darwin; 56 traces there need a Linux cell. 57 58 ## Outcome 59 60 Two instruments, not one. memcheck taint (`vestigia run`) sees any 61 dependence of a branch or address on a secret's data, even where 62 the outcome never varies, but not through control flow: after a 63 secret-dependent branch, what the branch builds from public data is 64 defined. Differential traces under a QEMU plugin (`vestigia record` 65 and `diff`) see what control does to data as well, on any ISA QEMU 66 runs, but only what the chosen secrets actually varied, and need 67 runs laid out alike (randomisation off). Neither needs a model. 68 69 - Penumbra (`etc/spike/penumbra/RESULTS.md`): elenchus's 79 leaks 70 fall in thirteen functions, each with a vestigia site in it and 71 its source line; one to two seconds per root. 72 - ppad-poly1305 (`etc/spike/poly1305/RESULTS.md`): every planted 73 leak found, no decoy flagged; release clean but for the harness's 74 use of the comparison result. One leak (an early-exit compare) 75 needs designed inputs for the differential instrument. 76 - ppad-secp256k1 (`etc/spike/secp256k1/RESULTS.md`): S1 found; S2 77 and S3 absent from x86's machine code, verified by its branches; 78 release clean but for validation and declassified outputs. 79 80 Open: aarch64 traces (an aarch64-linux build of the harness for the 81 differential instrument, a native host for memcheck); line tables 82 for GHC builds; the explain step, which separates a leak from a 83 declassified result (a tag comparison, a validity check).