vestigia

Detect where execution depends on secrets.
git clone git://git.ppad.tech/vestigia.git
Log | Files | Refs | README | LICENSE

commit d8e416b049070463033e5564ee2b3f88cead8a69
parent 9113a280893f9493a01519d7af1510dbc4a36f62
Author: Jared Tobin <jared@jtobin.io>
Date:   Wed, 21 Oct 2026 08:44:55 +0400

checks: a probe harness under both instruments, on Linux

etc/probe/harness.c takes its secret in hex and lets it reach a loop's
bound and a table index, beside a constant-time select that reaches
neither. nix/probe.nix builds it, runs it under traceOf and diffOf,
and holds each report's (class, function) pairs in the harness to the
expected ones exactly: a site or origin missing, or one more, fails
the check. The flake exposes it as checks.<system>.probe on Linux,
where both instruments run.

Diffstat:
Aetc/probe/harness.c | 45+++++++++++++++++++++++++++++++++++++++++++++
Mflake.nix | 8+++++++-
Anix/probe.nix | 58++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
3 files changed, 110 insertions(+), 1 deletion(-)

diff --git a/etc/probe/harness.c b/etc/probe/harness.c @@ -0,0 +1,45 @@ +/* + * harness.c: the harness the flake's probe check runs under both + * instruments. + * + * Copyright (c) 2026 Jared Tobin + * License: MIT + * + * Its secret, the first argument in hex (of one width for every + * secret, so that runs lay out alike), reaches a loop's bound and a + * table index; a constant-time select reaches neither. + */ +#include <stdio.h> +#include <stdlib.h> + +#include "vestigia.h" + +static unsigned char table[256]; + +__attribute__((noinline)) unsigned branchy(unsigned s) { + unsigned r = 0; + for (unsigned i = 0; i < (s & 7); i++) r += i; + return r; +} + +__attribute__((noinline)) unsigned lookup(unsigned s) { + return table[s & 0xff]; +} + +__attribute__((noinline)) unsigned ct(unsigned s, unsigned p) { + unsigned m = 0u - (p & 1u); + return (s & m) | (~s & ~m); +} + +int main(int argc, char **argv) { + unsigned s = (unsigned)strtoul(argc > 1 ? argv[1] : "0", NULL, 16); + unsigned out[3]; + for (int i = 0; i < 256; i++) table[i] = (unsigned char)i; + vestigia_secret(&s, sizeof s); + out[0] = branchy(s); + out[1] = lookup(s); + out[2] = ct(s, 1); + vestigia_public(out, sizeof out); + printf("%u %u %u\n", out[0], out[1], out[2]); + return 0; +} diff --git a/flake.nix b/flake.nix @@ -35,7 +35,13 @@ inherit (v) traceOf diffOf valgrindDev version; }; - checks.default = hpkgs.vestigia; + checks = { + default = hpkgs.vestigia; + } + # both instruments run Linux programs + // lib.optionalAttrs linux { + probe = import ./nix/probe.nix { inherit pkgs; vestigia = v; }; + }; devShells.default = hpkgs.shellFor { packages = p: [ p.vestigia ]; diff --git a/nix/probe.nix b/nix/probe.nix @@ -0,0 +1,58 @@ +# The probe check: etc/probe/harness.c under both instruments, each +# site and origin it should show found where it should be, and +# nothing else in the harness. +{ pkgs, vestigia }: + +let + lib = pkgs.lib; + + probe = pkgs.runCommandCC "vestigia-probe" { + buildInputs = [ vestigia.valgrindDev ]; + } '' + mkdir -p $out/bin + cc -O0 -g -fPIE -pie -I${vestigia.include}/include \ + -o $out/bin/probe ${../etc/probe/harness.c} \ + ${vestigia.include}/include/vestigia.c + ''; + + secrets = [ "00000005" "0000003a" "000000c3" ]; + objects = [ "/bin/probe" ]; + + trace = vestigia.traceOf { + name = "probe"; + harness = "${probe}/bin/probe"; + args = [ (builtins.head secrets) ]; + inherit objects; + }; + + diff = vestigia.diffOf { + name = "probe"; + harness = "${probe}/bin/probe"; + runs = map (s: [ s ]) secrets; + inherit objects; + }; + + # each report's (class, function) pairs in the harness, sorted + expected = { + trace = [ [ "address" "lookup" ] [ "control" "branchy" ] ]; + diff = [ [ "address" "lookup" ] [ "control" "branchy" ] ]; + }; +in +pkgs.runCommand "vestigia-probe-check" { + nativeBuildInputs = [ pkgs.jq ]; +} '' + check() { + got=$(jq -c "$2" "$1") + if [ "$got" != "$3" ]; then + echo "probe: $1: expected $3, got $got" >&2 + exit 1 + fi + } + check ${trace}/trace.json \ + '[.sites[] | [.class, .function]] | unique' \ + '${builtins.toJSON expected.trace}' + check ${diff}/diff.json \ + '[.origins[] | [.class, .frames[0].function]] | unique' \ + '${builtins.toJSON expected.diff}' + touch $out +''