commit d977ab84713434e4cca65e08c1741fe79aea5513
parent f319ea2c4c6186ac2f244dd58ba9d8125081cb96
Author: Jared Tobin <jared@jtobin.io>
Date: Sun, 18 Oct 2026 12:03:29 +0400
diff: runs designed for a path, compared for control and coverage alone
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 ]
