| Copyright | (c) 2026 Jared Tobin |
|---|---|
| License | MIT |
| Maintainer | Jared Tobin <jared@ppad.tech> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Vestigia.Diff
Description
Where runs that differ only in a secret differ. Each run is a leakage trace summarised per instruction (the QEMU plugin's dump): how often each instruction ran, how often it transferred to each target, a fingerprint of the addresses it touched, and, for an integer division, a fingerprint of its operands.
A branch whose outcome did not depend on the secret takes each
of its transfers in the same proportion however often it runs; a
branch whose outcomes differ in proportion between runs had its
own condition depend on the secret, and is a control origin
(a loop whose trip count the secret sets is one, though it also
runs a different number of times). So is a branch run as often,
taking each transfer as often, in another order: the plugin keeps
an order-sensitive fingerprint of what followed each instruction.
An instruction run equally often in every run whose addresses
differ computed one from the secret: an address origin. A
division, whose time depends on its operands, run equally often
on other operands is an operand origin. Every
other instruction run a different number of times sits where
control had already diverged: it is downstream. So is a return
whose transfers differ, however often it ran: it goes where the
call before it sent it, so its outcomes differ only because
control had diverged before the call.
Unlike memcheck's taint, this sees what control flow does to data as well as what data does: a value chosen by a secret branch and then used as an index differs between runs, though no undefined bit ever reached it. It sees only what the chosen secrets actually varied.
A difference means the secret only if nothing else differs
between runs. Controls are runs repeating the first run's secret:
an instruction that differs between the first run and a control
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 or operand 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.
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; dividing the same operands, at an operand 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.
Runs recorded under a data-independent-timing contract (Vestigia.Contract) also fingerprint the operands of every instruction outside it. One run equally often on other operands in some declared run is outside the contract on the secret: not an origin, since the contract says nothing either way of its time, but reported beside them, as is how many such instructions ran.
Synopsis
- data Insn = Insn {}
- data Run = Run {
- rnArguments :: ![ByteString]
- rnEnvironment :: !(Integer, Integer)
- rnStatus :: !Integer
- data Dump = Dump {
- dpInsns :: !(Map Integer Insn)
- dpTransfers :: !(Map Integer (Map Integer Integer))
- dpReturns :: !(Set Integer)
- dpOperands :: !(Map Integer Text)
- dpContexts :: !(Map Integer (Integer, Integer))
- dpCallers :: !(Map Integer (Bool, [Integer]))
- dpRun :: !(Maybe Run)
- dpOutside :: !(Map Integer Text)
- dpTexts :: !(Map Integer Text)
- dpIsa :: !(Maybe Text)
- dpContract :: !(Maybe Text)
- dpCpu :: !(Maybe Text)
- readDump :: Text -> Either String Dump
- callsOf :: Dump -> Integer -> [(Maybe Text, Integer)]
- runApart :: Run -> Run -> Maybe String
- data Kind
- data Named = Named {}
- data Origin
- data Divergence = Divergence {
- dvOrigins :: ![(Origin, Insn)]
- dvBehaviour :: !(Map (Origin, Integer) ([[Int]], [Int]))
- dvDownstream :: ![Insn]
- dvUnsteady :: ![Insn]
- dvRuns :: !Int
- dvControls :: !Int
- dvDesigned :: !Int
- dvExecuted :: !(Map Text (Set Integer))
- dvCallers :: !(Map Integer ([[(Maybe Text, Integer)]], Bool))
- dvOutside :: ![Insn]
- dvOutsideBehaviour :: !(Map Integer ([[Int]], [Int]))
- dvWatched :: !(Map Text (Set Integer))
- dvTexts :: !(Map Integer Text)
- dvIsa :: !(Maybe Text)
- dvContract :: !(Maybe Text)
- dvCpu :: !(Maybe Text)
- diffDumps :: [Dump] -> Divergence
- diffControlled :: [Dump] -> [Dump] -> Divergence
- diffDesigned :: [Dump] -> [Dump] -> [Dump] -> Divergence
- restrictTo :: [Text] -> Divergence -> Divergence
- loadBases :: Dump -> Map Text Integer
- layoutApart :: Dump -> Dump -> [(Text, Integer, Integer)]
- divergenceJson :: Text -> [Named] -> Map (Text, Integer) [Place] -> Divergence -> Value
- divergenceSummary :: Map (Text, Integer) [Place] -> Divergence -> Text
Documentation
One instruction of a run: its run-time address, and its object and address there, where the object's program headers place it.
Constructors
| Insn | |
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.
Constructors
| Run | |
Fields
| |
One run: its instructions by address, its transfers by source, each a count per target, the instructions that return, the divisions' operands, fingerprinted, the contexts calls made (each by the context it was made in and the call's address, 0 being the program's own), the contexts each instruction ran in (with whether it ran in more than the plugin kept), and how the run was made, where its dump says.
Constructors
| Dump | |
Fields
| |
readDump :: Text -> Either String Dump Source #
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, or one whose contexts do not chain back to the
program's own. 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. Beside it, M names the guest's ISA, G
the contract the run was recorded under, and P the CPU model
QEMU emulated, where one was named.
callsOf :: Dump -> Integer -> [(Maybe Text, Integer)] Source #
The calls that made a context, innermost first, at most 24 of them (as memcheck keeps): each by its object and address there, or by its run-time address where the run names no object for it.
runApart :: Run -> Run -> Maybe String Source #
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.
What a run is to a comparison: declared, designed for a path, or a control repeating the first run's secret.
Constructors
| DeclaredRun | |
| DesignedRun | |
| ControlRun |
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.
How an origin depended on the secret.
Constructors
| ControlOrigin | |
| AddressOrigin | |
| OperandOrigin |
data Divergence Source #
Where the runs differ: the origins, each an instruction run equally often everywhere, and how many instructions ran a different number of times.
Constructors
| Divergence | |
Fields
| |
Instances
| Show Divergence Source # | |
Defined in Vestigia.Diff Methods showsPrec :: Int -> Divergence -> ShowS # show :: Divergence -> String # showList :: [Divergence] -> ShowS # | |
| Eq Divergence Source # | |
Defined in Vestigia.Diff | |
diffDumps :: [Dump] -> Divergence Source #
Compare runs, uncontrolled.
diffControlled :: [Dump] -> [Dump] -> Divergence Source #
Compare runs, given controls repeating the first run's secret. Every run is set against every other, so an origin is any instruction at which some two runs differ, and which no control shows differing without the secret.
diffDesigned :: [Dump] -> [Dump] -> [Dump] -> Divergence Source #
Compare runs, given controls and runs designed to reach particular paths. The address and operand origins are the declared runs' alone; the control origins and what was executed are every run's.
restrictTo :: [Text] -> Divergence -> Divergence Source #
Only the origins, what was executed, and what ran downstream, in objects whose path contains one of the given texts.
loadBases :: Dump -> Map Text Integer Source #
Where a run loaded each object it executed: any of its instructions' run-time addresses less its address in the object.
layoutApart :: Dump -> Dump -> [(Text, Integer, Integer)] Source #
The objects two runs both executed but loaded at different addresses, each with where the first run put it and where the second did. Runs laid out apart touch other addresses wherever they touch memory, so comparing them says nothing of the secret.
divergenceJson :: Text -> [Named] -> Map (Text, Integer) [Place] -> Divergence -> Value Source #
The report: vestigia/diff-v4. Runs are given the declared,
then the designed, then the controls, and an origin names the
runs alike at it by the first two. An origin's stacks are its own
frames then its calls', innermost first, each frame with the
object and address of the instruction it names, as memcheck's
are in a taint report. The ISA, contract, and CPU model the runs
were recorded under head it; the instructions outside the contract
whose operands differed are given as origins are, and those that
ran, by object, as what was executed is.
divergenceSummary :: Map (Text, Integer) [Place] -> Divergence -> Text Source #
One line per origin, innermost frame first, for a terminal.