commit 200dfd9496267c8d8bae5dd3b45116676348eccf
parent f319ea2c4c6186ac2f244dd58ba9d8125081cb96
Author: Jared Tobin <jared@jtobin.io>
Date: Sun, 18 Oct 2026 12:03:29 +0400
merge impl/designed: runs designed for a path, compared apart
- vestigia diff --designed DUMP (diffOf designed): a run aimed at a
particular path counts toward the control origins and what was
executed, never toward the address origins, which only runs alike
in all but the secret can show. Mixed in with the others, a run
that went elsewhere, or that the root rejected early, left almost
every instruction run a different number of times across the set,
and the address origins vanished (Penumbra spend_auth_sign: 0 of
59).
Diffstat:
6 files changed, 101 insertions(+), 25 deletions(-)
diff --git a/CHANGELOG b/CHANGELOG
@@ -13,8 +13,9 @@
with vestigia's plugin, its leakage trace summarised per
instruction, and where runs differing only in the secret
diverge (vestigia/diff-v1), set against controls repeating a
- secret, with what every run executed in each object; runs are
- recorded with randomisation off and the guest's entropy
- seeded.
+ 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 with
+ randomisation off and the guest's entropy seeded.
* `traceOf` and `diffOf` run either as a derivation;
`nix/lib.nix` holds them for any package set.
diff --git a/README.md b/README.md
@@ -108,6 +108,13 @@ some run executed: what the chosen secrets exercised, to set against
what the code could execute. `--object` keeps origins, and what was
executed, to objects whose path contains the given text.
+`--designed DUMP` names a run aimed at a particular path. It differs
+from the others in where it goes, not only in the secret, so it
+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, which only runs alike in all but the secret can
+show.
+
A difference means the secret only if nothing else differs between
runs. `record` turns address-space randomisation off for itself and
QEMU, and seeds the guest's entropy, so runs lay memory out alike
diff --git a/app/Main.hs b/app/Main.hs
@@ -30,7 +30,7 @@ import qualified System.Process as P
import Paths_vestigia (version)
import Vestigia.Diff
- (diffControlled, divergenceJson, divergenceSummary, dvOrigins,
+ (diffDesigned, divergenceJson, divergenceSummary, dvOrigins,
inObject, inOffset, readDump, restrictTo)
import Vestigia.Json (encode)
import Vestigia.Layout (fixLayout)
@@ -49,6 +49,7 @@ data Opts = Opts {
, oAddr2line :: !(Maybe FilePath)
, oObjects :: ![T.Text]
, oControls :: ![FilePath]
+ , oDesigned :: ![FilePath]
}
main :: IO ()
@@ -85,7 +86,8 @@ usage e = do
, " vestigia record [--qemu PATH] [--plugin PATH] --dump FILE \
\-- PROGRAM [ARG...]"
, " vestigia diff [--out FILE] [--addr2line PATH] \
- \[--object TEXT]... [--control DUMP]... DUMP DUMP..."
+ \[--object TEXT]... [--control DUMP]... [--designed DUMP]... \
+ \DUMP DUMP..."
, ""
, "run executes PROGRAM under memcheck, which reports every"
, "branch and address that depended on bytes the program marked"
@@ -107,7 +109,7 @@ usage e = do
-- options before the program; "--" ends them
options :: [String] -> Either String (Opts, [String])
options = go (Opts Nothing Nothing Nothing Nothing Nothing Nothing
- Nothing [] [])
+ Nothing [] [] [])
where
go o xs = case xs of
("--" : rest) -> Right (o, rest)
@@ -122,6 +124,8 @@ options = go (Opts Nothing Nothing Nothing Nothing Nothing Nothing
go o { oObjects = oObjects o <> [ T.pack t ] } rest
("--control" : p : rest) ->
go o { oControls = oControls o <> [ p ] } rest
+ ("--designed" : p : rest) ->
+ go o { oDesigned = oDesigned o <> [ p ] } rest
(x : _) | take 2 x == "--" -> Left ("unknown option: " <> x)
_ -> Right (o, xs)
@@ -239,7 +243,9 @@ diff o paths = do
addr2line <- tool (oAddr2line o) "VESTIGIA_ADDR2LINE" "addr2line"
dumps <- traverse readOne paths
controls <- traverse readOne (oControls o)
- let dv = restrictTo (oObjects o) (diffControlled controls dumps)
+ designed <- traverse readOne (oDesigned o)
+ let dv = restrictTo (oObjects o)
+ (diffDesigned controls dumps designed)
places <- symbolize addr2line
[ (obj, inOffset i) | (_, i) <- dvOrigins dv
, Just obj <- [ inObject i ] ]
diff --git a/lib/Vestigia/Diff.hs b/lib/Vestigia/Diff.hs
@@ -35,6 +35,14 @@
-- differs without the secret (an entropy source, a clock) and is
-- `unsteady`, counted and excluded from the origins.
--
+-- Runs designed to reach a particular path are compared beside these
+-- but not alike: they differ from the others in where they go, not
+-- only in the secret, so an instruction's addresses differing in one
+-- of them says 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, which only runs alike in all but the secret can show.
+--
-- What every run executed, per object, is reported beside: the
-- instructions the chosen secrets exercised, and so, against what
-- a function could execute, the part of it the comparison saw.
@@ -47,6 +55,7 @@ module Vestigia.Diff (
, Divergence(..)
, diffDumps
, diffControlled
+ , diffDesigned
, restrictTo
, divergenceJson
, divergenceSummary
@@ -116,6 +125,7 @@ data Divergence = Divergence {
, dvUnsteady :: ![Insn]
, dvRuns :: !Int
, dvControls :: !Int
+ , dvDesigned :: !Int
-- | the offsets some run, control or not, executed, by object
, dvExecuted :: !(M.Map T.Text (S.Set Integer))
} deriving (Eq, Show)
@@ -129,7 +139,13 @@ diffDumps = diffControlled []
-- instruction at which some two runs differ, and which no control
-- shows differing without the secret.
diffControlled :: [Dump] -> [Dump] -> Divergence
-diffControlled cs ds = Divergence {
+diffControlled cs ds = diffDesigned cs ds []
+
+-- | Compare runs, given controls and runs designed to reach particular
+-- paths. The address origins are the declared runs' alone; the
+-- control origins and what was executed are every run's.
+diffDesigned :: [Dump] -> [Dump] -> [Dump] -> Divergence
+diffDesigned cs ds xs = Divergence {
dvOrigins = L.sortOn (inPc . snd)
[ o | o@(_, i) <- controls <> addresses
, not (inPc i `S.member` unsteady) ]
@@ -140,9 +156,10 @@ diffControlled cs ds = Divergence {
, Just i <- [ firstInsn pc ] ]
, dvRuns = length ds
, dvControls = length cs
+ , dvDesigned = length xs
, dvExecuted = M.fromListWith S.union
[ (obj, S.singleton (inOffset i))
- | d <- ds <> cs
+ | d <- ds <> xs <> cs
, i <- M.elems (dpInsns d)
, inCount i > 0
, Just obj <- [ inObject i ] ]
@@ -163,26 +180,34 @@ diffControlled cs ds = Divergence {
, fmap sig ia /= fmap sig ib || ta /= tb ]
sig i = (inCount i, inFingerprint i)
- pcs = S.unions (fmap (M.keysSet . dpInsns) ds)
- firstInsn pc = case [ i | d <- ds
+ -- every run, the declared first
+ runs = ds <> xs
+
+ pcs = S.unions (fmap (M.keysSet . dpInsns) runs)
+ firstInsn pc = case [ i | d <- runs
, Just i <- [ M.lookup pc (dpInsns d) ] ] of
(i : _) -> Just i
[] -> Nothing
-- run counts per run, absent counted as never run
- countsAt pc = [ maybe 0 inCount (M.lookup pc (dpInsns d)) | d <- ds ]
- alike xs = case xs of
+ countsIn rs pc =
+ [ maybe 0 inCount (M.lookup pc (dpInsns d)) | d <- rs ]
+ alike ys = case ys of
[] -> True
- (x : rest) -> all (== x) rest
+ (y : rest) -> all (== y) rest
- steady = S.filter (alike . countsAt) pcs
+ -- run equally often in every run, and in every declared run
+ steady = S.filter (alike . countsIn runs) pcs
+ steadyDeclared = S.filter (alike . countsIn ds)
+ (S.unions (fmap (M.keysSet . dpInsns) ds))
-- an instruction's run count and transfers, in each run that ran
-- it
ranAt pc =
[ (inCount i, M.findWithDefault M.empty pc (dpTransfers d))
- | d <- ds, Just i <- [ M.lookup pc (dpInsns d) ], inCount i > 0 ]
- transferSources = S.unions (fmap (M.keysSet . dpTransfers) ds)
+ | d <- runs, Just i <- [ M.lookup pc (dpInsns d) ]
+ , inCount i > 0 ]
+ transferSources = S.unions (fmap (M.keysSet . dpTransfers) runs)
-- outcomes in the same proportion: each target taken as often,
-- relative to the run count, in both
@@ -195,7 +220,9 @@ diffControlled cs ds = Divergence {
[] -> False
controlPcs = S.filter divergent transferSources
- downstream = (pcs `S.difference` steady) `S.difference` controlPcs
+ addressPcs = S.fromList [ inPc i | (_, i) <- addresses ]
+ downstream = ((pcs `S.difference` steady) `S.difference` controlPcs)
+ `S.difference` addressPcs
controls =
[ (ControlOrigin, i)
@@ -204,7 +231,7 @@ diffControlled cs ds = Divergence {
addresses =
[ (AddressOrigin, i)
- | pc <- S.toAscList steady
+ | pc <- S.toAscList steadyDeclared
, let fps = [ fmap inFingerprint (M.lookup pc (dpInsns d))
| d <- ds ]
, not (alike fps)
@@ -241,6 +268,7 @@ divergenceJson version places dv = Object
, ("version", String version) ])
, ("runs", Number (toInteger (dvRuns dv)))
, ("controls", Number (toInteger (dvControls dv)))
+ , ("designed", Number (toInteger (dvDesigned dv)))
, ("summary", Object
[ ("control", count ControlOrigin)
, ("address", count AddressOrigin)
@@ -291,7 +319,10 @@ divergenceSummary places dv = T.unlines $
, maybe "-" base (inObject i) ]
| (o, i) <- dvOrigins dv ]
<> [ T.pack (show (length (dvOrigins dv))) <> " origin(s) over "
- <> T.pack (show (dvRuns dv)) <> " run(s); "
+ <> T.pack (show (dvRuns dv)) <> " run(s)"
+ <> (if dvDesigned dv == 0 then ""
+ else " and " <> T.pack (show (dvDesigned dv)) <> " designed")
+ <> "; "
<> T.pack (show (length (dvDownstream dv)))
<> " instruction(s) downstream; "
<> T.pack (show (length (dvUnsteady dv)))
diff --git a/nix/lib.nix b/nix/lib.nix
@@ -93,9 +93,11 @@ let
# keeps origins in objects whose path contains one of them. The
# first run is repeated as a control, so that what differs
# without the secret is set aside rather than taken for it.
- # A run's own failure leaves its status; a dump vestigia
- # cannot read fails the build.
- diffOf = { name, harness, runs, objects ? [ ] }:
+ # `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 ? [ ] }:
pkgs.runCommand "vestigia-diff-${name}" { } ''
mkdir -p $out
start=$(date +%s%N)
@@ -106,7 +108,16 @@ let
> $out/stdout-${toString k} 2> $out/stderr-${toString k}
echo $? > $out/status-${toString k}
set -e
- '') runs}
+ '') runs}${lib.concatImapStrings (k: args: ''
+ set +e
+ ${vestigia}/bin/vestigia record \
+ --dump $out/designed-${toString k} \
+ -- ${harness} ${lib.escapeShellArgs args} \
+ > $out/stdout-designed-${toString k} \
+ 2> $out/stderr-designed-${toString k}
+ echo $? > $out/status-designed-${toString k}
+ set -e
+ '') designed}
set +e
${vestigia}/bin/vestigia record --dump $out/control-1 \
-- ${harness} ${lib.escapeShellArgs (builtins.head runs)} \
@@ -115,7 +126,8 @@ let
set -e
${vestigia}/bin/vestigia diff --out $out/diff.json \
${lib.concatMapStrings (o: "--object ${lib.escapeShellArg o} ")
- objects} \
+ objects}${lib.concatImapStrings (k: _:
+ "--designed $out/designed-${toString k} ") designed} \
--control $out/control-1 \
$out/dump-* 2> $out/summary
echo $(( ($(date +%s%N) - start) / 1000000 )) > $out/milliseconds
diff --git a/test/Main.hs b/test/Main.hs
@@ -162,6 +162,25 @@ diffTests = testGroup "diff"
@?= [ (ControlOrigin, 0x10) ]
fmap inPc (dvUnsteady dv) @?= [ 0x20 ]
+ , testCase "a designed run moves control, not addresses" $ do
+ a <- either assertFailure pure (readDump dumpA)
+ b <- either assertFailure pure (readDump dumpB)
+ -- a run designed onto another path: 0x10 taken every time, and
+ -- 0x20's addresses its own
+ x <- either assertFailure pure (readDump (T.unlines
+ [ "I 10 4 0 aaaa /lib.so 10", "E 10 30 4"
+ , "I 20 4 4 9999 /lib.so 20", "I 30 4 0 cccc /lib.so 30"
+ , "I 50 1 0 eeee /lib.so 50" ]))
+ let dv = diffDesigned [] [ a, a ] [ x ]
+ fmap (\(o, i) -> (o, inPc i)) (dvOrigins dv)
+ @?= [ (ControlOrigin, 0x10) ]
+ dvDesigned dv @?= 1
+ M.lookup "/lib.so" (dvExecuted dv)
+ @?= Just (S.fromList [ 0x10, 0x20, 0x30, 0x40, 0x50 ])
+ -- a declared run differing there is still an address origin
+ fmap (\(o, i) -> (o, inPc i)) (dvOrigins (diffDesigned [] [ a, b ]
+ [ x ])) @?= [ (ControlOrigin, 0x10), (AddressOrigin, 0x20) ]
+
, testCase "identical runs have no origins" $ do
a <- either assertFailure pure (readDump dumpA)
let dv = diffDumps [ a, a ]