commit e07799b18a84745a35c7ebd88f25d97cd4a1c265
parent 200dfd9496267c8d8bae5dd3b45116676348eccf
Author: Jared Tobin <jared@jtobin.io>
Date: Mon, 19 Oct 2026 14:19:44 +0400
merge impl/behaviour: each origin names the runs alike at it
- The diff report becomes vestigia/diff-v2. Each origin names how the
runs behaved there: the runs alike, grouped, and the runs that never
reached it, each by its dump's file name, so a reader can tell which
secrets the execution told apart, and whether two secrets a function
accepted differed at a site or only an accepted and a refused one.
- What ran a different number of times only downstream of an origin
is listed per object, and --object restricts it as it restricts
origins. diffOf passes its dumps in run order rather than by glob.
synthesis reads the groups to settle each trace site from the runs
alone (varies, rejects, downstream, steady) before any model reads it.
Diffstat:
7 files changed, 121 insertions(+), 24 deletions(-)
diff --git a/CHANGELOG b/CHANGELOG
@@ -12,7 +12,9 @@
* `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-v1), set against controls repeating a
+ diverge (vestigia/diff-v2: each origin with the runs alike
+ there and the runs that never 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 with
diff --git a/README.md b/README.md
@@ -100,13 +100,16 @@ address 0x152eb Fq::sqrt_ratio_zeta invsqrt.rs:117 ...
An *origin* is a branch whose outcomes differ in proportion between
runs (a loop whose trip count the secret sets is one) or an
-instruction run equally often whose addresses differ. Instructions
-that merely ran a different number of times sit where control had
-already diverged, and are counted as downstream rather than listed.
-The report also lists, per object, the offset of every instruction
-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.
+instruction run equally often whose addresses differ. Each origin
+names the runs that behaved alike there, grouped, and the runs that
+never reached it, each run by its dump's file name: which secrets
+the execution told apart. Instructions that merely ran a different
+number of times sit where control had already diverged, and are
+listed per object as downstream. The report also lists, per
+object, the offset of every instruction some run executed: what the
+chosen secrets exercised, to set against what the code could
+execute. `--object` keeps origins, what ran downstream, 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
@@ -144,7 +147,7 @@ vestigia.lib.x86_64-linux.diffOf {
```
Each run's report is `trace.json` (`vestigia/trace-v1`) or
-`diff.json` (`vestigia/diff-v1`), beside the raw memcheck XML or
+`diff.json` (`vestigia/diff-v2`), beside the raw memcheck XML or
plugin dumps, what the harness printed, and the run's wall time.
## Two instruments
diff --git a/app/Main.hs b/app/Main.hs
@@ -24,6 +24,7 @@ import qualified Data.Text.IO as TIO
import System.Directory (getTemporaryDirectory, removeFile)
import System.Environment (getArgs, getEnvironment, lookupEnv)
import System.Exit (ExitCode(..), exitWith)
+import System.FilePath (takeFileName)
import System.IO (hClose, hPutStrLn, openTempFile, stderr)
import System.Process (proc, waitForProcess, withCreateProcess)
import qualified System.Process as P
@@ -249,8 +250,10 @@ diff o paths = do
places <- symbolize addr2line
[ (obj, inOffset i) | (_, i) <- dvOrigins dv
, Just obj <- [ inObject i ] ]
- let doc = encode
- (divergenceJson (T.pack (showVersion version)) places dv)
+ -- a run is named by its dump's file name, the declared first
+ let names = fmap (T.pack . takeFileName) (paths <> oDesigned o)
+ doc = encode
+ (divergenceJson (T.pack (showVersion version)) names places dv)
maybe (TIO.putStr doc) (\p -> TIO.writeFile p doc) (oOut o)
TIO.hPutStr stderr (divergenceSummary places dv)
where
diff --git a/lib/Vestigia/Diff.hs b/lib/Vestigia/Diff.hs
@@ -46,6 +46,13 @@
-- 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.
+--
+-- Each origin names how the runs behaved there: the runs alike at
+-- it, grouped (taking each transfer in the same proportion, at a
+-- control origin; touching the same addresses, at an address
+-- origin), and the runs that never reached it. Whether two runs
+-- that differed there both had their secrets accepted is the
+-- reader's to say, from what each run returned.
module Vestigia.Diff (
Insn(..)
@@ -121,6 +128,10 @@ data Origin =
-- different number of times.
data Divergence = Divergence {
dvOrigins :: ![(Origin, Insn)]
+ -- | at each origin, the runs alike there, grouped, and the runs
+ -- that never reached it, as indices into the declared runs
+ -- then the designed (an address origin's, the declared alone)
+ , dvBehaviour :: !(M.Map (Origin, Integer) ([[Int]], [Int]))
, dvDownstream :: ![Insn]
, dvUnsteady :: ![Insn]
, dvRuns :: !Int
@@ -146,9 +157,9 @@ diffControlled cs ds = diffDesigned cs ds []
-- 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) ]
+ dvOrigins = L.sortOn (inPc . snd) origins
+ , dvBehaviour = M.fromList
+ [ ((o, inPc i), behaviourAt o (inPc i)) | (o, i) <- origins ]
, dvDownstream = [ i | pc <- S.toAscList downstream
, not (pc `S.member` unsteady)
, Just i <- [ firstInsn pc ] ]
@@ -180,9 +191,33 @@ diffDesigned cs ds xs = Divergence {
, fmap sig ia /= fmap sig ib || ta /= tb ]
sig i = (inCount i, inFingerprint i)
+ origins = [ o | o@(_, i) <- controls <> addresses
+ , not (inPc i `S.member` unsteady) ]
+
-- every run, the declared first
runs = ds <> xs
+ -- how the runs behaved at an origin: those that ran it, grouped
+ -- by what they did there, and those that never ran it. Only the
+ -- declared runs speak to an address.
+ behaviourAt o pc = case o of
+ ControlOrigin ->
+ ( classes proportional
+ [ (k, (inCount i, M.findWithDefault M.empty pc
+ (dpTransfers d)))
+ | (k, d, i) <- ranIn runs ]
+ , absentIn runs )
+ AddressOrigin ->
+ ( classes (==) [ (k, inFingerprint i) | (k, _, i) <- ranIn ds ]
+ , absentIn ds )
+ where
+ ranIn rs = [ (k, d, i) | (k, d) <- zip [ 0 .. ] rs
+ , Just i <- [ M.lookup pc (dpInsns d) ]
+ , inCount i > 0 ]
+ absentIn rs = [ k | (k, d) <- zip [ 0 .. ] rs
+ , maybe True ((== 0) . inCount)
+ (M.lookup pc (dpInsns d)) ]
+
pcs = S.unions (fmap (M.keysSet . dpInsns) runs)
firstInsn pc = case [ i | d <- runs
, Just i <- [ M.lookup pc (dpInsns d) ] ] of
@@ -238,14 +273,14 @@ diffDesigned cs ds xs = Divergence {
, Just i <- [ firstInsn pc ]
, inAccesses i > 0 ]
--- | Only the origins, and what was executed, in objects whose path
--- contains one of the given texts; downstream instructions are
--- kept, to be counted.
+-- | Only the origins, what was executed, and what ran downstream, in
+-- objects whose path contains one of the given texts.
restrictTo :: [T.Text] -> Divergence -> Divergence
restrictTo ps dv
| null ps = dv
| otherwise = dv {
dvOrigins = filter (inside . inObject . snd) (dvOrigins dv)
+ , dvDownstream = filter (inside . inObject) (dvDownstream dv)
, dvExecuted = M.filterWithKey (\o _ -> inside (Just o))
(dvExecuted dv)
}
@@ -259,11 +294,13 @@ originText o = case o of
ControlOrigin -> "control"
AddressOrigin -> "address"
--- | The report: @vestigia/diff-v1@.
+-- | The report: @vestigia/diff-v2@. Runs are named as given, the
+-- declared then the designed.
divergenceJson
- :: T.Text -> M.Map (T.Text, Integer) [Place] -> Divergence -> Value
-divergenceJson version places dv = Object
- [ ("schema", String "vestigia/diff-v1")
+ :: T.Text -> [T.Text] -> M.Map (T.Text, Integer) [Place] -> Divergence
+ -> Value
+divergenceJson version names places dv = Object
+ [ ("schema", String "vestigia/diff-v2")
, ("tool", Object [ ("name", String "vestigia")
, ("version", String version) ])
, ("runs", Number (toInteger (dvRuns dv)))
@@ -283,9 +320,17 @@ divergenceJson version places dv = Object
, ("offset", String (hex (inOffset i)))
, ("count", Number (inCount i))
, ("frames", Array (fmap placeJson (placesOf i)))
+ , ("groups", Array (fmap (Array . fmap named) groups))
+ , ("absent", Array (fmap named absent))
]
- | (o, i) <- dvOrigins dv ])
- , ("downstream", byObject (dvDownstream dv))
+ | (o, i) <- dvOrigins dv
+ , let (groups, absent) = M.findWithDefault ([], []) (o, inPc i)
+ (dvBehaviour dv) ])
+ , ("downstream", Object
+ [ (obj, Array (fmap (String . hex) (S.toAscList offs)))
+ | (obj, offs) <- M.toList (M.fromListWith S.union
+ [ (obj, S.singleton (inOffset i))
+ | i <- dvDownstream dv, Just obj <- [ inObject i ] ]) ])
, ("unsteady", byObject (dvUnsteady dv))
, ("executed", Object
[ (o, Array (fmap (String . hex) (S.toAscList xs)))
@@ -294,6 +339,9 @@ divergenceJson version places dv = Object
where
count o = Number (toInteger (length
[ () | (o', _) <- dvOrigins dv, o' == o ]))
+ named k = case drop k names of
+ (n : _) -> String n
+ [] -> String (T.pack (show k))
byObject is = Object
[ (o, Number (toInteger n))
| (o, n) <- M.toList (M.fromListWith (+)
@@ -344,3 +392,12 @@ divergenceSummary places dv = T.unlines $
hex :: Integer -> T.Text
hex n = "0x" <> T.pack (showHex n "")
+
+-- keys grouped by an equivalence on their values, each group in
+-- order and the groups by their first member
+classes :: (a -> a -> Bool) -> [(Int, a)] -> [[Int]]
+classes eq ys = case ys of
+ [] -> []
+ ((k, y) : rest) ->
+ let (same, other) = L.partition (eq y . snd) rest
+ in (k : fmap fst same) : classes eq other
diff --git a/nix/lib.nix b/nix/lib.nix
@@ -129,7 +129,8 @@ let
objects}${lib.concatImapStrings (k: _:
"--designed $out/designed-${toString k} ") designed} \
--control $out/control-1 \
- $out/dump-* 2> $out/summary
+ ${lib.concatImapStrings (k: _: "$out/dump-${toString k} ")
+ runs}2> $out/summary
echo $(( ($(date +%s%N) - start) / 1000000 )) > $out/milliseconds
'';
in
diff --git a/test/Main.hs b/test/Main.hs
@@ -181,6 +181,36 @@ diffTests = testGroup "diff"
fmap (\(o, i) -> (o, inPc i)) (dvOrigins (diffDesigned [] [ a, b ]
[ x ])) @?= [ (ControlOrigin, 0x10), (AddressOrigin, 0x20) ]
+ , testCase "an origin names the runs alike at it" $ do
+ a <- either assertFailure pure (readDump dumpA)
+ b <- either assertFailure pure (readDump dumpB)
+ 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" ]))
+ -- at the branch, the first and third runs alike; the designed
+ -- run is a control origin's to group, and the address origin
+ -- speaks only of the declared runs
+ let dv = diffDesigned [] [ a, b, a ] [ x ]
+ M.lookup (ControlOrigin, 0x10) (dvBehaviour dv)
+ @?= Just ([ [ 0, 2 ], [ 1 ], [ 3 ] ], [])
+ M.lookup (AddressOrigin, 0x20) (dvBehaviour dv)
+ @?= Just ([ [ 0, 2 ], [ 1 ] ], [])
+ -- the designed run never reaches 0x40
+ M.lookup (ControlOrigin, 0x10)
+ (dvBehaviour (diffDesigned [] [ a, a ] [ x ]))
+ @?= Just ([ [ 0, 1 ], [ 2 ] ], [])
+
+ , testCase "downstream is kept to the objects under audit" $ do
+ a <- either assertFailure pure (readDump dumpA)
+ b <- either assertFailure pure (readDump (T.unlines
+ [ "I 10 4 0 aaaa /lib.so 10", "E 10 30 3"
+ , "I 20 4 4 bbbb /lib.so 20", "I 30 3 0 cccc /lib.so 30"
+ , "I 40 1 1 dddd /lib.so 40", "I 60 2 0 ffff /libc.so 60" ]))
+ let dv = diffDumps [ a, b ]
+ fmap inPc (dvDownstream dv) @?= [ 0x30, 0x60 ]
+ fmap inPc (dvDownstream (restrictTo [ "lib.so" ] dv))
+ @?= [ 0x30 ]
+
, testCase "identical runs have no origins" $ do
a <- either assertFailure pure (readDump dumpA)
let dv = diffDumps [ a, a ]
diff --git a/vestigia.cabal b/vestigia.cabal
@@ -56,6 +56,7 @@ executable vestigia
base
, bytestring
, directory
+ , filepath
, process
, text
, vestigia
