commit eb4aa5947f7848b4eb9c54965468a3fe4a107ec8
parent 806a148127eee54b9b2fc5f7e3f68e3147300439
Author: Jared Tobin <jared@jtobin.io>
Date: Wed, 21 Oct 2026 10:42:15 +0400
readme, changelog: the gaps closed, and the caveats left
The README says what the probe check is and how to run it, gives the
caveats the branch leaves open (an address origin may be an address a
secret branch moved; only divisions are read for operands; GHC's
calls and returns are jumps), and the CHANGELOG's entry for 0.1.0 is
regrouped by command now that it says more.
Diffstat:
| M | CHANGELOG | | | 79 | ++++++++++++++++++++++++++++++++++++++++++------------------------------------- |
| M | README.md | | | 28 | ++++++++++++++++++++-------- |
2 files changed, 62 insertions(+), 45 deletions(-)
diff --git a/CHANGELOG b/CHANGELOG
@@ -4,43 +4,48 @@
* Initial version, with two instruments over a harness that marks
its secret (`vestigia.h`, defined by `vestigia.c`, which serves
a foreign function interface too and records where the loader
- put each object):
- * `vestigia run`: the harness under memcheck with the secret's
- bytes undefined, reporting each branch, address, and integer
- division operand computed from them, the last through a
- memcheck patch, each at its own instruction; `--dir` keeps the
- run, and `vestigia read` reports on several kept runs, or
- memcheck XML made elsewhere, as one (vestigia/trace-v2: each
- run with its command, exit, and objects, each site with the
- runs that reached it).
- * `vestigia record` and `vestigia diff`: the harness under QEMU
- with vestigia's plugin, its leakage trace summarised per
- instruction, and where runs differing only in the secret
- diverge (vestigia/diff-v3: each run with how it was made, each
- origin with the runs alike there and the runs that never
- reached it, a branch taking its outcomes in another order an
- origin too, a return never one, an integer division on other
- operands an `operand` origin, each origin with the calls that
- reached it, and what ran downstream listed per object), set
- against controls repeating a secret, with
- what every run executed in each object, and runs designed to
- reach particular paths compared for control and coverage alone
- (`--designed`);
- runs are recorded, an x86_64 or aarch64 harness on either
- host, with randomisation off (or not at all) and the guest's
- entropy, its getrandom included, seeded, and QEMU's own
- allocations kept off the guest's mappings, which under load
- can otherwise take the room of a guest library or heap; `diff`
- refuses runs that loaded an object at different addresses,
- runs of another program or with arguments or an environment
- of another size than the first run's, and a control that does
- not repeat the first run's arguments; a guest that starts a
- second thread is stopped and its dump refused. A taint run
- that marked no secret is refused.
- * `traceOf` and `diffOf` run either as a derivation, over a list
- of runs;
- `nix/lib.nix` holds them for any package set, with the version
- the command reports.
+ put each object). A taint run that marked no secret is refused.
+ * `vestigia run`: the harness under memcheck with the secret's
+ bytes undefined, reporting each branch, address, and integer
+ division operand computed from them (the last through a memcheck
+ patch, `nix/memcheck-operand.patch`), each at its own
+ instruction. `--dir` keeps a run, and `vestigia read` reports on
+ several kept runs, or memcheck XML made elsewhere, as one
+ (vestigia/trace-v2: each run with its command, exit, and
+ objects; each site with the runs that reached it).
+ * `vestigia record` and `vestigia diff`: the harness under QEMU
+ with vestigia's plugin, its leakage trace summarised per
+ instruction, and where runs differing only in the secret diverge
+ (vestigia/diff-v3):
+ * each run with how it was made, its arguments and exit status;
+ * the origins: a branch taking its outcomes in another proportion
+ or order, an instruction touching other addresses, and an
+ integer division on other operands, a return never one; each
+ with the runs alike there, the runs that never reached it, and
+ the calls that reached it;
+ * what ran downstream, and what every run executed, per object;
+ * controls repeating a secret, what differs in them set apart as
+ unsteady, and runs designed to reach particular paths, compared
+ for control and coverage alone (`--designed`).
+ * `record` runs an x86_64 or aarch64 harness on either host, with
+ randomisation off (or not at all), the guest's entropy, its
+ getrandom included, seeded, and QEMU's own allocations kept off
+ the guest's mappings, which under load can otherwise take the
+ room of a guest library or heap. The plugin names each
+ instruction by its address in its object, and stops a guest that
+ starts a second thread.
+ * `diff` refuses runs that loaded an object at different
+ addresses; runs of another program, or with arguments or an
+ environment of another size, than the first run's; a control
+ that does not repeat the first run's arguments; and a stopped
+ guest's dump. It names sources with LLVM's addr2line.
+ * `traceOf` and `diffOf` run either as a derivation, over a list of
+ runs; `nix/lib.nix` holds them for any package set, with the
+ version the command reports.
* `--object` keeps a taint run's sites (`run`, `read`, and
`traceOf`'s `objects`) to objects whose path contains the given
text, as it keeps a differential run's origins.
+ * The flake's probe check (`checks.<system>.probe`, on Linux) holds
+ both instruments' reports on a known harness to what it does, and
+ on an x86_64 host the differential one on the same harness built
+ for aarch64.
diff --git a/README.md b/README.md
@@ -84,11 +84,12 @@ An *origin* is a branch whose outcomes differ between runs, in
proportion or in order (`control`), an instruction whose addresses
differ (`address`), or a division, whose time depends on its
operands, on other operands (`operand`). Each names the runs that
-behaved alike there, and the calls that reached it, kept by the
-plugin as a shadow stack, as memcheck gives a site's callers. Instructions that
-merely ran a different number of times are listed as downstream, as
-are returns whose targets differ, which go where their calls sent
-them; and every instruction some run executed is listed as coverage.
+behaved alike there, and the calls that reached it, which the plugin
+keeps as a shadow stack, as memcheck gives a site its callers.
+Instructions that merely ran a different number of times are listed
+as downstream, as are returns whose targets differ, which go where
+their calls sent them; 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.
@@ -161,18 +162,29 @@ ppad-poly1305, and ppad-secp256k1.
is stopped, and its dump refused. Runs compared by `diff` must
differ only in the secret; it checks their arguments and
environments, not what the harness reads beyond them.
+* An address origin can be an address that an earlier secret branch
+ moved, a heap block or stack frame laid out apart, rather than one
+ computed from the secret.
+* Divisions alone are read for their operands. Floating-point
+ division and square root, and multiplication on cores that time it
+ by its operands, are left to a timing instrument.
* A GHC harness wants `-with-rtsopts=-xr1G -V0`, against the
- runtime's terabyte reservation and its interval timer.
+ runtime's terabyte reservation and its interval timer. GHC calls
+ and returns by jumping, so its origins have no callers, and a
+ return to a continuation is not known as a return.
* Source lines need line tables.
## Development
You'll require [Nix][nixos] with [flake][flake] support enabled.
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:
+`cabal test`. The probe check runs `etc/probe/harness.c` under both
+instruments, and the same harness built for aarch64 differentially,
+holding each report to what the harness does; it and the spikes under
+`etc/spike` run on an `x86_64-linux` builder:
```
+$ nix build .#checks.x86_64-linux.probe
$ nix build --impure -f etc/spike/penumbra traces
```
