commit 2e498fe4ab06c7d1b09e53c671056b5919da6ae7
parent ea2106c74490e26a040f0f3a2bd040e78dd0df0c
Author: Jared Tobin <jared@jtobin.io>
Date: Tue, 20 Oct 2026 13:18:24 +0400
readme: trimmed to what a user needs
Diffstat:
| M | README.md | | | 221 | +++++++++++++++++++++++++------------------------------------------------------ |
1 file changed, 69 insertions(+), 152 deletions(-)
diff --git a/README.md b/README.md
@@ -5,31 +5,22 @@
A Haskell tool that finds where a program's execution depended on a
secret, by running it.
-Constant-time code is held to a discipline: no branch, memory
-address, or variable-latency operand may depend on a secret. Whether
-a program keeps it is a fact about its *leakage trace* (the
-instructions it executes and the addresses it touches), and a
-running program has that trace in full: concrete values, concrete
-addresses, the path actually taken. vestigia reads it off the
-execution of a harness, reports every instruction that branched on
-the secret or computed an address from it, and names each by its
-function and source line. It is exact on the paths executed, needs
-no timing statistics, and judges the machine code as built, so a
-branch the compiler introduced is found and one it removed is not.
+vestigia executes a harness, reports every instruction that branched
+on the secret or computed an address from it, and names each by
+function and source line. It needs no timing statistics, is exact on
+the paths executed, and judges the machine code as built.
A clean report is not a proof of constant-time execution. It covers
-the paths the harness drove the program down, under the inputs it
-chose, and the discipline rather than the hardware: a leak through a
-data-dependent prefetcher or a variable-latency multiplier is for a
-timing instrument such as ppad's censor to find.
+only the paths the harness drove, and the discipline rather than the
+hardware: a leak through a prefetcher or a variable-latency
+multiplier is for a timing instrument such as ppad's censor.
## Usage
### Marking the secret
-A harness calls the code under audit, marks the secret's bytes
-before the call, and marks what the call is meant to reveal (a
-signature, a public key) after it:
+A harness marks the secret before calling the code under audit, and
+what the call is meant to reveal after it:
```c
#include "vestigia.h"
@@ -41,52 +32,34 @@ penumbra_audit_public_key(ws);
vestigia_public(ws + 32, 32); /* the public key it derives */
```
-The harness compiles `include/vestigia.c` beside it, which defines
-the marks; a harness that reaches them through a foreign function
-interface (a Haskell `foreign import ccall`) compiles the same file.
-Outside valgrind the marks are no-ops, so the same harness can be
-timed by censor unchanged. On Linux the first secret mark of any
-bytes also writes where the loader put each object, for `vestigia
-run` to name every site by its object and its address in it. A run
-that marked nothing found nothing because nothing was secret, and
-`run` refuses it.
+Compile `include/vestigia.c` beside it, or reach it through a foreign
+function interface. Outside valgrind the marks are no-ops, so censor
+can time the same harness. A run that marks nothing is refused.
### Taint: `vestigia run`
`run` executes the harness under valgrind's memcheck with the marked
-bytes made undefined. memcheck tracks definedness bit by bit, so
-every branch whose condition, and every load or store whose address,
-descends from a marked byte is reported, with the mark as its
-origin; everything else memcheck says is kept apart. Penumbra's
-public-key derivation, on x86-64 (function names shortened):
+bytes undefined, and reports every branch and address that descends
+from them:
```
$ vestigia run --out trace.json -- ./harness public_key 4
control 0x4875cd2 MontConfig::from_bigint montgomery_backend.rs:359 x8
control 0x4875cf9 cmp<4> mod.rs:565 x4
-control 0x4875d42 ge<BigInt<4>, BigInt<4>> mod.rs:475 x4
...
-control 0x486ffbd Fr::from_bytes_checked fr.rs:102 x4
-control 0x4878d7a without_leading_zeros skip_while.rs:50 x42
control 0x4878d4d next<&[u64]> bits.rs:32 x982
12 secret-dependent site(s); 0 unrelated; 0 fault(s)
```
-Here the modulus compares in decoding the secret scalar, its
-canonicality check, and the double-and-add of the scalar
-multiplication, which iterates about 245 times per call on the
-secret's bits. `vestigia read FILE.xml` gives the same report from a
-memcheck run made elsewhere. `--object TEXT` keeps the sites in
-objects whose path contains the given text, as it keeps a
-differential run's origins.
+`vestigia read FILE.xml` reports on a memcheck run made elsewhere.
+`--object TEXT` keeps the sites in objects whose path contains TEXT.
### Differential traces: `vestigia record` and `vestigia diff`
-`record` runs the harness under QEMU with vestigia's plugin, which
-summarises the leakage trace per instruction: how often it ran, how
-often it transferred to each target, and a fingerprint of the
-addresses it touched. Run the harness several times, differing only
-in the secret, and `diff` reports where the runs diverge:
+`record` runs the harness under QEMU with a plugin that summarises,
+per instruction, how often it ran, where it branched, and which
+addresses it touched. Record several runs differing only in the
+secret, and `diff` reports where they diverge:
```
$ for s in 1 2 3; do
@@ -97,58 +70,35 @@ $ vestigia diff --object libpenumbra_audit --control control \
> --out diff.json run-*
control 0xe9d6 Element::vartime_compress_to_field sign.rs:11 ...
address 0x152c8 Fq::sqrt_ratio_zeta invsqrt.rs:113 ...
-address 0x152eb Fq::sqrt_ratio_zeta invsqrt.rs:117 ...
...
44 origin(s) over 3 run(s); 1383 instruction(s) downstream; 0 unsteady ...
```
-An *origin* is a branch whose outcomes differ in proportion between
-runs (a loop whose trip count the secret sets is one), a branch
-taking the same outcomes as often in another order, or an
-instruction run equally often whose addresses differ. Each origin
-names the runs that behaved alike there, grouped, and the runs that
-never reached it, each run by its dump's file name: which secrets
-the execution told apart. Instructions that merely ran a different
-number of times sit where control had already diverged, and are
-listed per object as downstream. The report also lists, per
-object, the offset of every instruction some run executed: what the
-chosen secrets exercised, to set against what the code could
-execute. `--object` keeps origins, what ran downstream, and what
-was executed, to objects whose path contains the given text.
-
-`--designed DUMP` names a run aimed at a particular path: the same
-harness with the same arguments, differing from the others only in a
-secret chosen to reach that path. A run whose public inputs differ
-is not designed but another experiment, and its differences say
-nothing about the secret. A designed run counts toward the control
-origins (a branch whose outcomes shift under it chose by the
-secret) and what was executed, never toward the address origins:
-it goes where the others do not, so an instruction's addresses
-differing in it need not mean an address computed from the secret.
-
-A difference means the secret only if nothing else differs between
-runs. `record` turns address-space randomisation off for itself and
-QEMU, refusing to run where it cannot, and seeds the guest's
-entropy, so runs lay memory out alike and a hash table seeded from
-the system's randomness is laid out alike too. The pinned QEMU
-fills the guest's `getrandom` from that seeded generator, the host
-still checking its flags and choosing its length
-(`nix/qemu-getrandom.patch`); a guest reading `/dev/urandom` still
-reads the host's. `--control DUMP` names a run repeating the first run's
-secret: whatever differs between the two (a clock read, a
-scheduler's choice) is *unsteady*, counted and kept out of the
-origins.
+An *origin* is a branch whose outcomes differ between runs, in
+proportion or in order, or an instruction whose addresses differ.
+Each names the runs that behaved alike there. Instructions that
+merely ran a different number of times are listed as downstream, and
+every instruction some run executed is listed as coverage.
+
+* `--control DUMP` repeats the first run's secret; whatever differs
+ between the two is *unsteady* and kept out of the origins.
+* `--designed DUMP` is a run whose secret was chosen to reach a
+ particular path. It counts toward control origins and coverage,
+ never toward address origins.
+* `--object TEXT` keeps the report to matching objects.
+
+`record` disables address-space randomisation and seeds the guest's
+entropy, `getrandom` included (`nix/qemu-getrandom.patch`), so runs
+lay memory out alike. A guest reading `/dev/urandom` still reads the
+host's.
### As derivations
-The flake's `lib.<system>` holds `traceOf` and `diffOf`, which run a
-harness under either instrument as a derivation: a run for
-`x86_64-linux` then executes on whatever builds for that system, and
-its report is cached like any other output. Either takes `objects`,
-the texts `--object` is given. `diffOf` repeats the first run as its
-control. `nix/lib.nix` holds the same definitions for one package
-set, for a consumer that pins vestigia and builds traces with its own
-nixpkgs, beside `version`, the version the command reports.
+The flake's `lib.<system>` holds `traceOf` and `diffOf`, which run
+either instrument as a derivation; an `x86_64-linux` run executes on
+any builder for that system, and its report is cached. `diffOf`
+repeats the first run as its control. `nix/lib.nix` holds the same
+for a consumer's own nixpkgs, beside `version`.
```nix
vestigia.lib.x86_64-linux.diffOf {
@@ -159,76 +109,43 @@ vestigia.lib.x86_64-linux.diffOf {
}
```
-Each run's report is `trace.json` (`vestigia/trace-v1`) or
-`diff.json` (`vestigia/diff-v2`), beside the raw memcheck XML or
-plugin dumps, what the harness printed, and the run's wall time.
+The output holds `trace.json` (`vestigia/trace-v1`) or `diff.json`
+(`vestigia/diff-v2`), the raw memcheck XML or plugin dumps, what the
+harness printed, and the wall time.
## Two instruments
-Each sees what the other cannot:
-
-* memcheck propagates secrecy through data, not control. Once a
- program branches on a secret, what it builds from public data on
- either arm is defined, so the leaks downstream of the first
- secret-dependent branch go unseen. On Penumbra it found the
- double-and-add but not the field operations on the point it
- builds, nor decaf377's table lookups on that point.
-* Differential traces see what control does to data, since a value
- chosen by a secret branch differs between runs. But they see only
- what the chosen secrets actually varied: a validity check that
- every valid secret passes takes the same direction in every run,
- though its condition reads the secret.
-
-Run both. On Penumbra their union covers every function in which
-elenchus found a leak; see `etc/spike/*/RESULTS.md` for Penumbra,
-ppad-poly1305's planted mutants, and ppad-secp256k1.
+memcheck propagates secrecy through data, not control: what a
+program builds from public data on either arm of a secret branch
+counts as public, so leaks downstream of it go unseen. Differential
+traces see those, but only where the chosen secrets made execution
+differ: a check that every valid secret passes looks alike in every
+run. Run both; `etc/spike/*/RESULTS.md` compares them on Penumbra,
+ppad-poly1305, and ppad-secp256k1.
## Caveats
-Coverage is the harness's. Only the paths its inputs drive are
-traced, and a differential trace sees a leak only where its secrets
-make the execution differ: an early-exit tag comparison is invisible
-to random candidate tags, which all mismatch at the first byte, and
-plain to candidates sharing a prefix with the true tag.
-
-What a function is meant to reveal must be marked public, or it is
-reported: a comparison's result, a validity check, a public key
-before it is serialised. Telling those from leaks is a reading of
-the code, not a measurement.
-
-valgrind and QEMU's user mode run on Linux; elsewhere vestigia only
-reads reports made there. The differential traces run any ISA QEMU
-emulates, so an aarch64 build is traced on an x86-64 host, but
-memcheck needs a native one. The plugin assumes a single-threaded
-guest, and runs compared by `diff` must differ in nothing but the
-secret, including the length of their arguments.
-
-A GHC harness wants `-with-rtsopts=-xr1G -V0`: the runtime's default
-terabyte address-space reservation makes memcheck crawl, and its
-interval timer makes runs schedule differently.
-
-Source lines need line tables in the code under audit, and sites are
-named on the assumption that an object's executable file offsets are
-its virtual addresses, as GNU ld and lld emit them.
+* Coverage is the harness's. An early-exit tag comparison is
+ invisible to random candidate tags, which all mismatch at the
+ first byte.
+* What a function is meant to reveal (a comparison's result, a
+ public key) must be marked public, or it is reported.
+* valgrind and QEMU's user mode run on Linux; elsewhere vestigia only
+ reads their reports. QEMU traces other ISAs differentially, but
+ memcheck needs a native host.
+* The plugin assumes a single-threaded guest, and runs compared by
+ `diff` must differ only in the secret, argument lengths included.
+* A GHC harness wants `-with-rtsopts=-xr1G -V0`, against the
+ runtime's terabyte reservation and its interval timer.
+* Source lines need line tables, and sites assume an object's file
+ offsets are its virtual addresses, as GNU ld and lld emit them.
## Development
You'll require [Nix][nixos] with [flake][flake] support enabled.
-Enter a development shell with:
-
-```
-$ nix develop
-```
-
-Then do e.g.:
-
-```
-$ cabal build
-$ cabal test
-```
-
-The spikes under `etc/spike` build their targets and run on an
-`x86_64-linux` builder:
+Enter a development shell with `nix develop`, then `cabal build` and
+`cabal test`. The spikes under `etc/spike` run on an `x86_64-linux`
+builder:
```
$ nix build --impure -f etc/spike/penumbra traces
