commit 164ae07e7fb7c0ebb37c7cfdce5662bf1eac4130
parent dbca2b60ce279520826d4c578fcab75e60452541
Author: Jared Tobin <jared@jtobin.io>
Date: Wed, 21 Oct 2026 09:03:58 +0400
record: how a run was made kept in its dump; runs made apart refused
A dump said what the guest executed, not how the run was made, so
diff could not tell runs that differ in the secret alone from runs of
another program, or with a longer argument, or a larger environment,
each of which lays the guest's stack out apart and so differs at every
stack address; nor a control from a run repeating some other secret.
Those were caveats in the README, and diffOf kept each run's exit
status in a file beside its dump.
record now appends to the dump, after QEMU exits, the program and its
arguments (their bytes, in hex), the guest environment's variables and
the bytes they take, and the exit status. diff refuses a dump without
that record, a run whose program, argument count or lengths, or
environment size differ from the first run's, and a control whose
arguments are not the first run's, naming the run. The report becomes
vestigia/diff-v3: `runs` lists each run, declared, designed, or
control, with its arguments and exit status, in place of the counts.
readDump reads the record whole or not at all; runApart says why two
runs cannot be compared. The probe check holds the report's runs to
the ones made, and diff to refusing a control of another secret and a
run with a longer argument.
Diffstat:
7 files changed, 262 insertions(+), 49 deletions(-)
diff --git a/CHANGELOG b/CHANGELOG
@@ -12,19 +12,24 @@
* `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-v2: each origin with the runs alike
- there and the runs that never reached it, a branch taking its
- outcomes in another order an origin too, 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
+ diverge (vestigia/diff-v3: each run with how it was made, each
+ origin with the runs alike there and the runs that never
+ reached it, a branch taking its outcomes in another order an
+ origin too, 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
randomisation off (or not at all) and the guest's entropy,
its getrandom included, seeded, and QEMU's own allocations kept
off the guest's mappings, which under load can otherwise take
the room of a guest library or heap; `diff` refuses runs that
- loaded an object at different addresses. A taint run that
- marked no secret is refused.
+ loaded an object at different addresses, runs of another
+ program or with arguments or an environment of another size
+ than the first run's, and a control that does not repeat the
+ first run's arguments; a guest that starts a second thread is
+ stopped and its dump refused. A taint run that marked no
+ secret is refused.
* `traceOf` and `diffOf` run either as a derivation;
`nix/lib.nix` holds them for any package set, with the version
the command reports.
diff --git a/README.md b/README.md
@@ -96,6 +96,14 @@ arena, large blocks from the heap), and `diff` refuses runs that
loaded an object at different addresses. A guest reading
`/dev/urandom` still reads the host's.
+`record` appends to its dump how the run was made: the program and
+its arguments, the size of the guest's environment, and the exit
+status, which the report gives for each run. `diff` refuses a run of
+another program, or with arguments of another number or length, or an
+environment of another size, than the first run's, each of which lays
+the guest's stack out apart; and a control that does not repeat the
+first run's arguments.
+
### As derivations
The flake's `lib.<system>` holds `traceOf` and `diffOf`, which run
@@ -114,7 +122,7 @@ vestigia.lib.x86_64-linux.diffOf {
```
The output holds `trace.json` (`vestigia/trace-v1`) or `diff.json`
-(`vestigia/diff-v2`), the raw memcheck XML or plugin dumps, what the
+(`vestigia/diff-v3`), the raw memcheck XML or plugin dumps, what the
harness printed, and the wall time.
## Two instruments
@@ -139,7 +147,8 @@ ppad-poly1305, and ppad-secp256k1.
memcheck needs a native host.
* The plugin records one guest thread: a guest that starts a second
is stopped, and its dump refused. Runs compared by `diff` must
- differ only in the secret, argument lengths included.
+ differ only in the secret; it checks their arguments and
+ environments, not what the harness reads beyond them.
* A GHC harness wants `-with-rtsopts=-xr1G -V0`, against the
runtime's terabyte reservation and its interval timer.
* Source lines need line tables.
diff --git a/app/Main.hs b/app/Main.hs
@@ -16,7 +16,10 @@ module Main (
import Control.Exception (IOException, try)
import Control.Monad (unless, when)
import qualified Data.ByteString as BS
+import Data.Foldable (for_)
import Data.Version (showVersion)
+import qualified GHC.Foreign as GF
+import GHC.IO.Encoding (getFileSystemEncoding)
import Numeric (showHex)
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
@@ -32,8 +35,9 @@ import qualified System.Process as P
import Paths_vestigia (version)
import Vestigia.Diff
- (diffDesigned, divergenceJson, divergenceSummary, dvOrigins,
- inObject, inOffset, layoutApart, readDump, restrictTo)
+ (Dump(..), Kind(..), Named(..), Run(..), diffDesigned, divergenceJson,
+ divergenceSummary, dvOrigins, inObject, inOffset, layoutApart,
+ readDump, restrictTo, runApart)
import Vestigia.Json (encode)
import Vestigia.Layout (fixLayout)
import Vestigia.Memcheck (readMemcheck)
@@ -98,9 +102,10 @@ usage e = do
, "--object keeps sites in objects whose path contains TEXT."
, ""
, "record executes PROGRAM under QEMU with vestigia's plugin and"
- , "dumps its leakage trace per instruction; diff compares dumps"
- , "of runs that differ only in a secret and reports where they"
- , "diverge (vestigia/diff-v1), naming sources with addr2line."
+ , "dumps its leakage trace per instruction, with how it was run;"
+ , "diff compares dumps of runs that differ only in a secret and"
+ , "reports where they diverge (vestigia/diff-v3), naming sources"
+ , "with addr2line."
, "--object keeps origins in objects whose path contains TEXT;"
, "--control names a run repeating the first run's secret, and"
, "what differs in it is unsteady, not an origin."
@@ -192,12 +197,13 @@ run o prog progArgs = do
\(vestigia_secret was never called on any bytes); its run \
\says nothing"
exitWith (ExitFailure 2)
- report o (Just (exitCode code)) os xml
+ report o (Just (exitStatus code)) os xml
if temporary then removeFile xml else pure ()
- where
- exitCode c = case c of
- ExitSuccess -> 0
- ExitFailure n -> n
+
+exitStatus :: ExitCode -> Int
+exitStatus c = case c of
+ ExitSuccess -> 0
+ ExitFailure n -> n
readXml :: Opts -> FilePath -> IO ()
readXml o xml = report o Nothing [] xml
@@ -249,22 +255,50 @@ record o prog progArgs = do
let tunables = "GLIBC_TUNABLES"
host = "glibc.malloc.arena_max=1:glibc.malloc.mmap_threshold="
<> "33554432"
+ own = lookup tunables environment
guest = maybe [ "-U", tunables ]
- (\v -> [ "-E", tunables <> "=" <> v ]) (lookup tunables environment)
+ (\v -> [ "-E", tunables <> "=" <> v ]) own
+ others = filter ((/= tunables) . fst) environment
r <- try (withCreateProcess
((proc qemu (guest
<> [ "-seed", "0"
, "-plugin", plugin <> ",out=" <> dump, prog ]
<> progArgs))
- { P.env = Just ((tunables, host)
- : filter ((/= tunables) . fst) environment) })
+ { P.env = Just ((tunables, host) : others) })
(\_ _ _ ph -> waitForProcess ph))
case r of
Left e -> do
hPutStrLn stderr ("vestigia: cannot run " <> qemu <> ": "
<> show (e :: IOException))
exitWith (ExitFailure 2)
- Right c -> exitWith c
+ Right c -> do
+ -- how the run was made, by which diff tells runs that differ
+ -- in the secret alone from runs laid out apart: the guest's
+ -- environment is QEMU's, with its own tunables restored
+ appendRun dump (prog : progArgs)
+ (others <> [ (tunables, v) | Just v <- [ own ] ]) c
+ exitWith c
+
+-- append a run's record to its dump (Vestigia.Diff.readDump): its
+-- arguments' bytes, its environment's variables and the bytes they
+-- take, and its exit status
+appendRun :: FilePath -> [String] -> [(String, String)] -> ExitCode
+ -> IO ()
+appendRun dump args env code = do
+ enc <- getFileSystemEncoding
+ let bytes s = GF.withCStringLen enc s BS.packCStringLen
+ as <- traverse bytes args
+ es <- traverse (\(k, v) -> bytes (k <> "=" <> v)) env
+ appendFile dump $ unlines $
+ [ unwords ("A" : [ concatMap byte (BS.unpack a) | not (BS.null a) ])
+ | a <- as ]
+ <> [ "N " <> showHex (length es) "" <> " "
+ <> showHex (sum (fmap ((+ 1) . BS.length) es)) ""
+ , "X " <> show (exitStatus code) ]
+ where
+ byte w = case showHex w "" of
+ [ d ] -> [ '0', d ]
+ ds -> ds
diff :: Opts -> [FilePath] -> IO ()
diff o paths = do
@@ -272,6 +306,28 @@ diff o paths = do
dumps <- traverse readOne paths
controls <- traverse readOne (oControls o)
designed <- traverse readOne (oDesigned o)
+ -- every run with how it was made: the declared, the designed, then
+ -- the controls. Runs made apart differ by more than the secret,
+ -- and are refused, not compared
+ named <- traverse (\(p, k, d) -> case dpRun d of
+ Just r -> pure (p, Named (T.pack (takeFileName p)) k r)
+ Nothing -> refuse (p <> " holds no record of how it was run \
+ \(vestigia record appends one), so nothing says what it ran"))
+ (zip3 (paths <> oDesigned o <> oControls o)
+ (fmap (const DeclaredRun) paths
+ <> fmap (const DesignedRun) (oDesigned o)
+ <> fmap (const ControlRun) (oControls o))
+ (dumps <> designed <> controls))
+ case named of
+ ((p0, first) : rest) -> for_ rest $ \(p, n) -> do
+ for_ (runApart (nmRun first) (nmRun n)) $ \why ->
+ refuse (p <> " " <> why <> " (" <> p0 <> "); runs compared \
+ \must differ in the secret alone")
+ when (nmKind n == ControlRun
+ && rnArguments (nmRun n) /= rnArguments (nmRun first)) $
+ refuse (p <> " is a control, but does not repeat the \
+ \arguments of " <> p0 <> ", the run it controls")
+ [] -> pure ()
-- runs laid out apart differ wherever they touch memory, not by
-- the secret: such runs are refused, not compared
case zip paths dumps of
@@ -294,17 +350,16 @@ diff o paths = do
places <- symbolize addr2line
[ (obj, inOffset i) | (_, i) <- dvOrigins dv
, Just obj <- [ inObject i ] ]
- -- 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)
+ let doc = encode (divergenceJson (T.pack (showVersion version))
+ (fmap snd named) places dv)
maybe (TIO.putStr doc) (\p -> TIO.writeFile p doc) (oOut o)
TIO.hPutStr stderr (divergenceSummary places dv)
where
readOne p = do
bytes <- BS.readFile p
case readDump (TE.decodeUtf8With TEE.lenientDecode bytes) of
- Left e -> do
- hPutStrLn stderr ("vestigia: " <> p <> ": " <> e)
- exitWith (ExitFailure 2)
+ Left e -> refuse (p <> ": " <> e)
Right d -> pure d
+ refuse e = do
+ hPutStrLn stderr ("vestigia: " <> e)
+ exitWith (ExitFailure 2)
diff --git a/lib/Vestigia/Diff.hs b/lib/Vestigia/Diff.hs
@@ -58,8 +58,12 @@
module Vestigia.Diff (
Insn(..)
+ , Run(..)
, Dump(..)
, readDump
+ , runApart
+ , Kind(..)
+ , Named(..)
, Origin(..)
, Divergence(..)
, diffDumps
@@ -72,11 +76,15 @@ module Vestigia.Diff (
, divergenceSummary
) where
+import qualified Data.ByteString as BS
import qualified Data.List as L
import qualified Data.Map.Strict as M
import qualified Data.Set as S
import qualified Data.Text as T
+import qualified Data.Text.Encoding as TE
+import qualified Data.Text.Encoding.Error as TEE
import Numeric (readHex, showHex)
+import Text.Read (readMaybe)
import Vestigia.Json
import Vestigia.Symbol (Place(..))
@@ -94,24 +102,40 @@ data Insn = Insn {
, inOffset :: !Integer
} deriving (Eq, Show)
--- | One run: its instructions by address, and its transfers by
--- source, each a count per target.
+-- | How a run was made, as `vestigia record` appends it to the
+-- plugin's dump: the program and its arguments, as the bytes it
+-- passed them; the variables of the environment the guest was
+-- given, and the bytes they take; and the run's exit status.
+data Run = Run {
+ rnArguments :: ![BS.ByteString]
+ , rnEnvironment :: !(Integer, Integer)
+ , rnStatus :: !Integer
+ } deriving (Eq, Show)
+
+-- | One run: its instructions by address, its transfers by source,
+-- each a count per target, and how it was made, where its dump
+-- says.
data Dump = Dump {
dpInsns :: !(M.Map Integer Insn)
, dpTransfers :: !(M.Map Integer (M.Map Integer Integer))
+ , dpRun :: !(Maybe Run)
} deriving (Eq, Show)
-- | Read a plugin dump. A dump in which no instruction ran records
-- no run (the plugin writes every instruction the guest executed),
-- and is refused rather than compared as one that did nothing, as
-- is the dump of a guest the plugin stopped for starting a second
--- thread.
+-- thread. The record `vestigia record` appends (an @A@ line per
+-- argument, its bytes in hex; @N@, the environment's variables and
+-- bytes, in hex; @X@, the exit status, in decimal) is read whole or
+-- not at all.
readDump :: T.Text -> Either String Dump
-readDump t = go (T.lines t) M.empty M.empty
+readDump t = go (T.lines t) M.empty M.empty [] Nothing Nothing
where
- go ls is es = case ls of
+ go ls is es as env st = case ls of
[]
- | any ((> 0) . inCount) (M.elems is) -> pure (Dump is es)
+ | any ((> 0) . inCount) (M.elems is) ->
+ Dump is es <$> record (reverse as) env st
| otherwise ->
Left "no instruction ran: the run was not recorded"
(l : rest) -> case T.words l of
@@ -120,20 +144,73 @@ readDump t = go (T.lines t) M.empty M.empty
<*> pure ord
<*> pure (if obj == "-" then Nothing else Just obj)
<*> unhex off
- go rest (M.insert (inPc i) i is) es
+ go rest (M.insert (inPc i) i is) es as env st
[ "E", from, to, n ] -> do
f <- unhex from
k <- unhex to
c <- unhex n
go rest is (M.insertWith M.union f (M.singleton k c) es)
+ as env st
[ "T", _ ] ->
Left "the guest started a second thread, which a trace \
\cannot record: the run was stopped"
- [] -> go rest is es
+ [ "A" ] -> go rest is es (BS.empty : as) env st
+ [ "A", h ] -> do
+ b <- unhexBytes h
+ go rest is es (b : as) env st
+ [ "N", n, b ] -> do
+ v <- (,) <$> unhex n <*> unhex b
+ go rest is es as (Just v) st
+ [ "X", x ] -> case readMaybe (T.unpack x) of
+ Just v -> go rest is es as env (Just v)
+ Nothing -> Left ("not an exit status: " <> T.unpack x)
+ [] -> go rest is es as env st
_ -> Left ("an unreadable dump line: " <> T.unpack l)
+ record as env st = case (as, env, st) of
+ ([], Nothing, Nothing) -> pure Nothing
+ (_ : _, Just e, Just x) -> pure (Just (Run as e x))
+ _ -> Left "an incomplete record of the run"
unhex x = case readHex (T.unpack x) of
[ (v, "") ] -> pure v
_ -> Left ("not hexadecimal: " <> T.unpack x)
+ unhexBytes h
+ | odd (T.length h) = Left ("not hexadecimal bytes: " <> T.unpack h)
+ | otherwise =
+ BS.pack <$> traverse (fmap fromInteger . unhex) (T.chunksOf 2 h)
+
+-- | Why a run cannot be set beside the first as differing from it in
+-- the secret alone, if it cannot: it ran another program, its
+-- arguments differ from the first run's in number or length, or it
+-- was given an environment of another size. Each lays the guest's
+-- stack out apart, and so every address on it.
+runApart :: Run -> Run -> Maybe String
+runApart first r
+ | take 1 (rnArguments r) /= take 1 (rnArguments first) =
+ Just "ran another program than the first run"
+ | fmap BS.length (rnArguments r)
+ /= fmap BS.length (rnArguments first) =
+ Just "has arguments that differ from the first run's in number \
+ \or length"
+ | rnEnvironment r /= rnEnvironment first =
+ Just "was given an environment of another size than the first \
+ \run's"
+ | otherwise = Nothing
+
+-- | What a run is to a comparison: declared, designed for a path, or
+-- a control repeating the first run's secret.
+data Kind =
+ DeclaredRun
+ | DesignedRun
+ | ControlRun
+ deriving (Eq, Show)
+
+-- | A run as the report names it: by its dump's file name, with what
+-- it is to the comparison and how it was made.
+data Named = Named {
+ nmName :: !T.Text
+ , nmKind :: !Kind
+ , nmRun :: !Run
+ } deriving (Eq, Show)
-- | Where a run loaded each object it executed: any of its
-- instructions' run-time addresses less its address in the object.
@@ -336,18 +413,26 @@ originText o = case o of
ControlOrigin -> "control"
AddressOrigin -> "address"
--- | The report: @vestigia/diff-v2@. Runs are named as given, the
--- declared then the designed.
+-- | The report: @vestigia/diff-v3@. Runs are given the declared,
+-- then the designed, then the controls, and an origin names the
+-- runs alike at it by the first two.
divergenceJson
- :: T.Text -> [T.Text] -> M.Map (T.Text, Integer) [Place] -> Divergence
+ :: T.Text -> [Named] -> M.Map (T.Text, Integer) [Place] -> Divergence
-> Value
-divergenceJson version names places dv = Object
- [ ("schema", String "vestigia/diff-v2")
+divergenceJson version runs places dv = Object
+ [ ("schema", String "vestigia/diff-v3")
, ("tool", Object [ ("name", String "vestigia")
, ("version", String version) ])
- , ("runs", Number (toInteger (dvRuns dv)))
- , ("controls", Number (toInteger (dvControls dv)))
- , ("designed", Number (toInteger (dvDesigned dv)))
+ , ("runs", Array
+ [ Object
+ [ ("name", String (nmName r))
+ , ("kind", String (kindText (nmKind r)))
+ , ("arguments", Array
+ [ String (TE.decodeUtf8With TEE.lenientDecode a)
+ | a <- rnArguments (nmRun r) ])
+ , ("status", Number (rnStatus (nmRun r)))
+ ]
+ | r <- runs ])
, ("summary", Object
[ ("control", count ControlOrigin)
, ("address", count AddressOrigin)
@@ -379,6 +464,11 @@ divergenceJson version names places dv = Object
| (o, xs) <- M.toList (dvExecuted dv) ])
]
where
+ names = [ nmName r | r <- runs, nmKind r /= ControlRun ]
+ kindText k = case k of
+ DeclaredRun -> "declared"
+ DesignedRun -> "designed"
+ ControlRun -> "control"
count o = Number (toInteger (length
[ () | (o', _) <- dvOrigins dv, o' == o ]))
named k = case drop k names of
diff --git a/nix/probe.nix b/nix/probe.nix
@@ -64,9 +64,32 @@ pkgs.runCommand "vestigia-probe-check" {
'[.origins[] | [.class, .frames[0].function]] | unique' \
'${builtins.toJSON expected.diff}'
+ # each run as it was made: the declared, then the control
+ check ${diff}/diff.json \
+ '[.runs[] | [.kind, .arguments[1], .status]]' \
+ '${builtins.toJSON (map (s: [ "declared" s 0 ]) secrets
+ ++ [ [ "control" (builtins.head secrets) 0 ] ])}'
+
+ v=${vestigia.vestigia}/bin/vestigia
+
+ # a control must repeat the run it controls, and every run must lay
+ # out as the first: its arguments of one number and length
+ $v record --dump a -- ${probe}/bin/probe 00000005
+ $v record --dump b -- ${probe}/bin/probe 0000003a
+ $v record --dump c -- ${probe}/bin/probe 000000003a
+ if $v diff --control b a a 2> refusal; then
+ echo "probe: a control repeating another secret was taken" >&2
+ exit 1
+ fi
+ grep -q 'does not repeat' refusal
+ if $v diff a c 2> refusal; then
+ echo "probe: a run with a longer argument was compared" >&2
+ exit 1
+ fi
+ grep -q 'number or length' refusal
+
# a guest that starts a second thread is stopped, and its dump
# refused
- v=${vestigia.vestigia}/bin/vestigia
if $v record --dump threads -- ${threads}/bin/threads; then
echo "probe: a guest's second thread was recorded" >&2
exit 1
diff --git a/test/Main.hs b/test/Main.hs
@@ -273,6 +273,31 @@ diffTests = testGroup "diff"
, testCase "a guest stopped for a second thread is refused" $
isLeft (readDump "T 2\n") @? "accepted"
+
+ , testCase "a run's record reads whole" $ do
+ d <- either assertFailure pure (readDump (dumpA <> T.unlines
+ [ "A 2f62696e2f70", "A", "A 3035", "N 2 1a", "X -9" ]))
+ dpRun d @?= Just (Run [ "/bin/p", "", "05" ] (2, 0x1a) (-9))
+ fmap dpRun (readDump dumpA) @?= Right Nothing
+
+ , testCase "an incomplete record is refused" $ do
+ isLeft (readDump (dumpA <> "A 3035\nN 2 1a\n")) @? "no status"
+ isLeft (readDump (dumpA <> "N 2 1a\nX 0\n")) @? "no arguments"
+ isLeft (readDump (dumpA <> "A 305\nN 2 1a\nX 0\n"))
+ @? "half a byte"
+
+ , testCase "runs made apart are told apart" $ do
+ let r = Run [ "/bin/p", "05" ] (2, 0x1a) 0
+ runApart r r { rnArguments = [ "/bin/p", "3a" ], rnStatus = 1 }
+ @?= Nothing
+ isJust (runApart r r { rnArguments = [ "/bin/q", "05" ] })
+ @? "another program"
+ isJust (runApart r r { rnArguments = [ "/bin/p", "005" ] })
+ @? "a longer argument"
+ isJust (runApart r r { rnArguments = [ "/bin/p", "05", "x" ] })
+ @? "another argument"
+ isJust (runApart r r { rnEnvironment = (2, 0x1b) })
+ @? "a larger environment"
]
where
-- 0x10 is a branch run four times, taken twice in A and three
@@ -327,6 +352,11 @@ isLeft e = case e of
Left _ -> True
Right _ -> False
+isJust :: Maybe a -> Bool
+isJust m = case m of
+ Just _ -> True
+ Nothing -> False
+
-- a secret branch, an uninitialised heap read, a bad read, and a
-- leak report
mixed :: T.Text
diff --git a/vestigia.cabal b/vestigia.cabal
@@ -38,6 +38,7 @@ library
, Vestigia.Xml
build-depends:
base >= 4.9 && < 5
+ , bytestring
, containers
, process
, text
