commit 8a8465281e50c54f7930b0e7e029882790b78776
parent dd561dc3aeea8b244fe48229f71e8d6033499e75
Author: Jared Tobin <jared@jtobin.io>
Date: Tue, 27 Oct 2026 11:19:04 +0400
nix: diffOf under a contract, and the probe's floating-point division
diffOf takes a contract, and the command finds llvm-objdump through
VESTIGIA_OBJDUMP. The probe divides its secret in floating point,
outside either contract, and checks each differential trace under
its ISA's contract finds it there and nothing more.
Diffstat:
3 files changed, 63 insertions(+), 16 deletions(-)
diff --git a/etc/probe/harness.c b/etc/probe/harness.c
@@ -8,8 +8,10 @@
* Its secret, the first argument in hex (of one width for every
* secret, so that runs lay out alike), reaches a loop's bound, a
* table index, which of two calls a helper returns to, a dividend,
- * a divisor, and, on a path the third secret alone takes, another
- * table index; a constant-time select reaches none of them.
+ * a divisor, a floating-point division (outside either ISA's
+ * data-independent-timing contract), and, on a path the third secret
+ * alone takes, another table index; a constant-time select reaches
+ * none of them.
*/
#include <stdio.h>
#include <stdlib.h>
@@ -72,6 +74,12 @@ __attribute__((noinline)) unsigned divide_memory(unsigned s) {
#endif
}
+/* a secret divided in floating point, which neither Arm's DIT nor
+ Intel's DOITM covers */
+__attribute__((noinline)) unsigned fpdivide(unsigned s) {
+ return (unsigned)((double)s / 7.0);
+}
+
/* a table index on a path one secret takes */
__attribute__((noinline)) unsigned rare(unsigned s) {
if ((s & 0xffu) == 0xc3u) return table[(s >> 1) & 0xffu];
@@ -85,7 +93,7 @@ __attribute__((noinline)) unsigned ct(unsigned s, unsigned p) {
int main(int argc, char **argv) {
unsigned s = (unsigned)strtoul(argc > 1 ? argv[1] : "0", NULL, 16);
- unsigned out[7];
+ unsigned out[8];
for (int i = 0; i < 256; i++) table[i] = (unsigned char)i;
vestigia_secret(&s, sizeof s);
out[0] = branchy(s);
@@ -95,8 +103,9 @@ int main(int argc, char **argv) {
out[4] = divide_memory(s);
out[5] = rare(s);
out[6] = ct(s, 1);
+ out[7] = fpdivide(s);
vestigia_public(out, sizeof out);
- printf("%u %u %u %u %u %u %u\n", out[0], out[1], out[2], out[3],
- out[4], out[5], out[6]);
+ printf("%u %u %u %u %u %u %u %u\n", out[0], out[1], out[2], out[3],
+ out[4], out[5], out[6], out[7]);
return 0;
}
diff --git a/nix/lib.nix b/nix/lib.nix
@@ -67,6 +67,8 @@ let
"${plugin}/lib/libvestigia-qemu.so"
"--set-default VESTIGIA_ADDR2LINE"
"${pkgs.llvm}/bin/llvm-addr2line"
+ "--set-default VESTIGIA_OBJDUMP"
+ "${pkgs.llvm}/bin/llvm-objdump"
])}
ln -s ${include}/include $out/include
'';
@@ -111,16 +113,26 @@ let
# without the secret is set aside rather than taken for it.
# `designed` runs, aimed at particular paths, are compared beside
# them for control and coverage but not for addresses (vestigia
- # diff --designed). A run's own failure leaves its status; a dump
- # vestigia cannot read fails the build.
- diffOf = { name, harness, runs, objects ? [ ], designed ? [ ] }:
+ # diff --designed). Under a `contract` (arm-dit or intel-doitm, the
+ # harness's ISA's), every run also fingerprints the operands of the
+ # instructions outside it in `objects` (vestigia record --contract).
+ # A run's own failure leaves its status; a dump vestigia cannot read
+ # fails the build.
+ diffOf = { name, harness, runs, objects ? [ ], designed ? [ ]
+ , contract ? null }:
+ let
+ watch = lib.optionalString (contract != null)
+ ("--contract ${lib.escapeShellArg contract} "
+ + lib.concatMapStrings (o: "--object ${lib.escapeShellArg o} ")
+ objects);
+ in
pkgs.runCommand "vestigia-diff-${name}" { } ''
mkdir -p $out
start=$(date +%s%N)
${lib.concatImapStrings (k: args: ''
set +e
${vestigia}/bin/vestigia record --dump $out/dump-${toString k} \
- -- ${harness} ${lib.escapeShellArgs args} \
+ ${watch}-- ${harness} ${lib.escapeShellArgs args} \
> $out/stdout-${toString k} 2> $out/stderr-${toString k}
echo $? > $out/status-${toString k}
set -e
@@ -128,7 +140,7 @@ let
set +e
${vestigia}/bin/vestigia record \
--dump $out/designed-${toString k} \
- -- ${harness} ${lib.escapeShellArgs args} \
+ ${watch}-- ${harness} ${lib.escapeShellArgs args} \
> $out/stdout-designed-${toString k} \
2> $out/stderr-designed-${toString k}
echo $? > $out/status-designed-${toString k}
@@ -136,7 +148,7 @@ let
'') designed}
set +e
${vestigia}/bin/vestigia record --dump $out/control-1 \
- -- ${harness} ${lib.escapeShellArgs (builtins.head runs)} \
+ ${watch}-- ${harness} ${lib.escapeShellArgs (builtins.head runs)} \
> $out/stdout-control-1 2> $out/stderr-control-1
echo $? > $out/status-control-1
set -e
diff --git a/nix/probe.nix b/nix/probe.nix
@@ -2,7 +2,9 @@
# site and origin it should show found where it should be, and
# nothing else in the harness. On an x86_64 host, the same harness
# built for aarch64 is traced differentially too, under QEMU; memcheck
-# needs a native host.
+# needs a native host. Each differential trace is repeated under its
+# ISA's data-independent-timing contract, which finds the floating-
+# point division outside it and changes no origin.
{ pkgs, vestigia }:
let
@@ -41,13 +43,16 @@ let
inherit objects;
};
- diffOf = name: harness: vestigia.diffOf {
- inherit name objects;
+ diffOf = name: harness: contract: vestigia.diffOf {
+ inherit name objects contract;
harness = "${harness}/bin/probe";
runs = map (s: [ s ]) secrets;
};
- diff = diffOf "probe" probe;
- diffCross = diffOf "probe-aarch64" cross;
+ native = if x86_64 then "intel-doitm" else "arm-dit";
+ diff = diffOf "probe" probe null;
+ diffCross = diffOf "probe-aarch64" cross null;
+ diffContract = diffOf "probe-contract" probe native;
+ diffCrossContract = diffOf "probe-aarch64-contract" cross "arm-dit";
# each report's (class, function) pairs in the harness, sorted
expected = {
@@ -98,6 +103,27 @@ pkgs.runCommand "vestigia-probe-check" {
'${builtins.toJSON expected.diff}'
''}
+ # under a contract, the floating-point division is outside it, and
+ # the origins are those found without one
+ for d in ${diffContract} ${lib.optionalString x86_64
+ "${diffCrossContract}"}; do
+ check $d/diff.json '[.outside[] | .frames[0].function] | unique' \
+ '["fpdivide"]'
+ check $d/diff.json \
+ '[.origins[] | [.class, .frames[0].function]] | unique' \
+ '${builtins.toJSON expected.diff}'
+ check $d/diff.json '.summary.watched > 0' 'true'
+ check $d/diff.json '[.outside[] | .instruction | type] | unique' \
+ '["string"]'
+ done
+ check ${diffContract}/diff.json '[.contract.name, .isa]' \
+ '${builtins.toJSON [ native (if x86_64 then "x86_64" else "aarch64") ]}'
+ check ${diff}/diff.json '.contract' 'null'
+ ${lib.optionalString x86_64 ''
+ check ${diffCrossContract}/diff.json '[.contract.name, .isa]' \
+ '["arm-dit","aarch64"]'
+ ''}
+
# each origin's stack runs from its own function to the call in
# main that reached it
for d in ${diff} ${lib.optionalString x86_64 "${diffCross}"}; do
