README.md (5321B)
1 # vestigia 2 3  4 [](https://docs.ppad.tech/vestigia) 5 6 Finds where a program's execution depended on a secret, by running 7 it. 8 9 vestigia runs a harness and reports every instruction that branched 10 on the secret, computed an address from it, or divided by or into it, 11 naming each by function and source line. It has two instruments: 12 taint tracking under valgrind's memcheck, and differential traces 13 under QEMU. 14 15 A clean report is not a proof of constant-time execution. It covers 16 only the paths the harness drove, and the program rather than the 17 hardware: a leak through a prefetcher or a variable-latency 18 multiplier is for a timing instrument such as 19 [censor](https://github.com/ppad-tech/censor). 20 21 ## Marking the secret 22 23 A harness marks the secret before the call under audit, and what the 24 call is meant to reveal after it: 25 26 ```c 27 #include "vestigia.h" 28 29 vestigia_secret(key, 32); 30 derive_public_key(pub, key); 31 vestigia_public(pub, 33); 32 ``` 33 34 Compile `include/vestigia.c` beside it, or call it through an FFI. 35 Outside valgrind the marks are no-ops. A run that marks nothing is 36 refused. 37 38 ## Taint: `run` and `read` 39 40 `run` executes the harness under memcheck with the secret's bytes 41 undefined, and reports each branch, address, and division operand 42 derived from them: 43 44 ``` 45 $ vestigia run --out trace.json -- ./harness 46 control 0x40011a2 branchy harness.c:26 x8 47 address 0x400134b lookup harness.c:31 x1 48 ... 49 3 secret-dependent site(s) over 1 run(s); 0 unrelated; 0 fault(s) 50 ``` 51 52 memcheck sees only the path a run takes, so trace several secrets: 53 `run --dir DIR` keeps a run, and `read DIR...` reports on several as 54 one. `read` also accepts memcheck XML made elsewhere. 55 56 ## Differential: `record` and `diff` 57 58 `record` runs the harness under QEMU with a plugin that summarises 59 each instruction's execution: counts, branch outcomes, addresses 60 touched, and division operands. `diff` compares runs that differ only 61 in the secret and reports where they diverge: 62 63 ``` 64 $ for s in 1 2 3; do 65 > vestigia record --dump run-$s -- ./harness $s 66 > done 67 $ vestigia record --dump control -- ./harness 1 68 $ vestigia diff --control control --out diff.json run-* 69 control 0x11a2 branchy harness.c:26 ... 70 address 0x134b lookup harness.c:31 ... 71 ... 72 ``` 73 74 An *origin* is a branch whose outcomes differ between runs 75 (`control`), an instruction whose addresses differ (`address`), or a 76 division on differing operands (`operand`). Each lists the runs that 77 agreed there and its callers. Instructions that merely ran a 78 different number of times are reported as downstream. 79 80 * `--control DUMP` repeats the first run's secret; what differs 81 between the two is *unsteady* and excluded from the origins. 82 * `--designed DUMP` is a run whose secret was chosen to reach a 83 particular path; it never counts toward address or operand 84 origins. 85 * `--object TEXT` restricts the report to matching objects (also for 86 `run` and `read`). 87 88 `record` disables address-space randomisation and seeds the guest's 89 entropy so that runs lay memory out alike. `diff` refuses runs whose 90 program, argument shape, environment size, or object layout differ. 91 92 ### Contracts 93 94 `record --contract arm-dit` (or `intel-doitm`) additionally 95 fingerprints the operands of every instruction outside that ISA's 96 data-independent-timing contract, in objects matching `--object`. 97 `diff` reports any such instruction seen on differing operands under 98 `outside`, apart from the origins. `vestigia watch` computes the list 99 of such instructions once, for `record --watch FILE` to reuse. 100 101 ## Nix 102 103 The flake's `lib.<system>` provides `traceOf` and `diffOf`, which run 104 either instrument as a derivation over a list of runs: 105 106 ```nix 107 vestigia.lib.x86_64-linux.diffOf { 108 name = "example"; 109 harness = "${harness}/bin/harness"; 110 runs = map (s: [ s ]) [ "1" "2" "3" ]; 111 objects = [ "libexample" ]; 112 } 113 ``` 114 115 `nix/lib.nix` provides the same for a consumer's own nixpkgs. 116 117 ## Caveats 118 119 * Coverage is the harness's. A path no chosen secret reaches is 120 unseen. 121 * Outputs the call is meant to reveal must be marked public, or they 122 are reported. 123 * memcheck propagates secrecy through data, not control; differential 124 traces see only where the chosen secrets made execution differ. 125 Use both. 126 * valgrind and QEMU user mode run on Linux only. `record` runs x86_64 127 or aarch64 harnesses on either host; memcheck needs a native one. 128 * `record` stops a guest that starts a second thread. 129 * A guest reading `/dev/urandom` reads the host's. 130 * An address origin may be a layout moved by an earlier secret 131 branch, rather than an address computed from the secret. 132 * A contract is the ISA's statement, not a given core's. 133 * GHC harnesses want `-with-rtsopts=-xr1G -V0`. GHC's calls and 134 returns are jumps, so its origins have no callers. 135 * Source lines need line tables. 136 137 ## Development 138 139 You'll require [Nix][nixos] with [flake][flake] support enabled. 140 Enter a development shell with `nix develop`, then `cabal build` and 141 `cabal test`. The probe check runs both instruments over 142 `etc/probe/harness.c` on an `x86_64-linux` builder: 143 144 ``` 145 $ nix build .#checks.x86_64-linux.probe 146 ``` 147 148 [nixos]: https://nixos.org/ 149 [flake]: https://nixos.org/manual/nix/unstable/command-ref/new-cli/nix3-flake.html