commit 5570e76dd4246b6fd6eb59a9091ddb6a347cfd23
parent cc5c97fb59c911df9f6727b21cb6e29df071f70a
Author: Jared Tobin <jared@jtobin.io>
Date: Wed, 21 Oct 2026 09:37:20 +0400
memcheck: a division's undefined operand reported, at its instruction
memcheck propagates an undefined operand into a division's quotient
and says nothing, so a taint run missed a division of or by a secret
as the differential one did until the last commit.
nix/memcheck-operand.patch, applied to the valgrind vestigia runs,
adds an error kind, UninitOperand ("Integer division depends on
uninitialised value(s)"), with its origin tracked, and reports it for
each undefined operand of every integer division VEX lifts guest code
to: x86_64's DIV and IDIV, aarch64's UDIV and SDIV, and the rest.
Unlike memcheck's checks before an address or a branch, it leaves the
operands undefined after reporting them, so what is reported
downstream is as it was. Vestigia.Trace reads a client-request
UninitOperand as an `operand` site.
memcheck keeps the instruction pointer exact only where an
instruction touches memory, by default, so a division by a register
was reported at the memory access before it. `run` now passes
--px-file-backed=allregs-at-each-insn, which keeps every register
exact at each instruction of the program's own code, so such a site
is named by its own address. The probe check finds both divisions
under taint and holds them to the addresses the differential trace
gives.
Diffstat:
7 files changed, 360 insertions(+), 18 deletions(-)
diff --git a/CHANGELOG b/CHANGELOG
@@ -6,9 +6,11 @@
a foreign function interface too and records where the loader
put each object):
* `vestigia run`: the harness under memcheck with the secret's
- bytes undefined, reporting each branch and address computed
- from them (vestigia/trace-v1); `vestigia read` reports from
- memcheck's XML.
+ bytes undefined, reporting each branch, address, and integer
+ division operand computed from them, the last through a
+ memcheck patch, each at its own instruction
+ (vestigia/trace-v1); `vestigia read` reports from memcheck's
+ XML.
* `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
diff --git a/README.md b/README.md
@@ -6,8 +6,8 @@ A Haskell tool that finds where a program's execution depended on a
secret, by running it.
vestigia executes a harness, reports every instruction that branched
-on the secret or computed an address from it, and names each by
-function and source line.
+on the secret, computed an address from it, or divided by or into
+it, and names each by function and source line.
A clean report is not a proof of constant-time execution. It
covers only the paths the harness drove, and the discipline
@@ -39,8 +39,9 @@ can time the same harness. A run that marks nothing is refused.
### Taint: `vestigia run`
`run` executes the harness under valgrind's memcheck with the marked
-bytes undefined, and reports every branch and address that descends
-from them:
+bytes undefined, and reports every branch, address, and integer
+division operand that descends from them (memcheck reports the last
+through vestigia's patch, `nix/memcheck-operand.patch`):
```
$ vestigia run --out trace.json -- ./harness public_key 4
diff --git a/app/Main.hs b/app/Main.hs
@@ -143,8 +143,12 @@ options = go (Opts Nothing Nothing Nothing Nothing Nothing Nothing
-- the settings every trace runs under: origins tracked so a
-- secret's descendants are known as such, no limit on contexts,
--- the precise definedness checks optimised code needs, and no
--- leak report
+-- the precise definedness checks optimised code needs, every
+-- register (the instruction pointer among them) brought up to date
+-- at each instruction of a program's own code, so that a site that
+-- touches no memory, a division by a register, is named by its own
+-- address rather than the last memory access before it, and no leak
+-- report
memcheckArgs :: FilePath -> [String]
memcheckArgs xml =
[ "--tool=memcheck"
@@ -154,6 +158,7 @@ memcheckArgs xml =
, "--error-limit=no"
, "--num-callers=24"
, "--expensive-definedness-checks=yes"
+ , "--px-file-backed=allregs-at-each-insn"
, "--leak-check=no"
, "--child-silent-after-fork=yes"
]
diff --git a/lib/Vestigia/Trace.hs b/lib/Vestigia/Trace.hs
@@ -11,11 +11,12 @@
-- whose undefined value was created by a client request descends
-- from a byte the harness marked secret, so it is a site where the
-- execution depended on the secret: a branch (`control`), an
--- address computed from it (`address`), or a system call handed
--- it (`syscall`). Every other uninitialised read is kept apart as
--- `unrelated`, and memory errors as `faults`: neither says
--- anything about the secret. Leak reports say nothing about the
--- execution and are dropped.
+-- address computed from it (`address`), an integer division's
+-- operand (`operand`, from vestigia's patched memcheck), or a
+-- system call handed it (`syscall`). Every other uninitialised read
+-- is kept apart as `unrelated`, and memory errors as `faults`:
+-- neither says anything about the secret. Leak reports say nothing
+-- about the execution and are dropped.
module Vestigia.Trace (
Class(..)
@@ -43,6 +44,7 @@ import Vestigia.Memcheck
data Class =
Control
| Address
+ | Operand
| Syscall
deriving (Eq, Ord, Show)
@@ -71,6 +73,7 @@ classText :: Class -> T.Text
classText c = case c of
Control -> "control"
Address -> "address"
+ Operand -> "operand"
Syscall -> "syscall"
-- what a secret-originated error says about the execution
@@ -78,12 +81,14 @@ classify :: MemError -> Maybe Class
classify e = case (meOrigin e, meKind e) of
(ClientRequest _, "UninitCondition") -> Just Control
(ClientRequest _, "UninitValue") -> Just Address
+ (ClientRequest _, "UninitOperand") -> Just Operand
(ClientRequest _, "SyscallParam") -> Just Syscall
_ -> Nothing
uninitialised :: MemError -> Bool
uninitialised e =
- meKind e `elem` [ "UninitCondition", "UninitValue", "SyscallParam" ]
+ meKind e `elem`
+ [ "UninitCondition", "UninitValue", "UninitOperand", "SyscallParam" ]
-- | The run's leakage. Sites are one per instruction and class:
-- memcheck reports one context per distinct stack, and the
@@ -179,6 +184,7 @@ traceJson version exit tr = Object
, ("summary", Object
[ ("control", count Control)
, ("address", count Address)
+ , ("operand", count Operand)
, ("syscall", count Syscall)
, ("unrelated", Number (toInteger (length (trUnrelated tr))))
, ("faults", Number (toInteger (length (trFaults tr))))
diff --git a/nix/lib.nix b/nix/lib.nix
@@ -16,9 +16,12 @@ let
});
# memcheck runs on Linux only; elsewhere the command can still
- # read a run's XML
+ # read a run's XML. It reports an integer division's undefined
+ # operands (memcheck-operand.patch)
linux = pkgs.stdenv.hostPlatform.isLinux;
- valgrind = pkgs.valgrind;
+ valgrind = pkgs.valgrind.overrideAttrs (o: {
+ patches = (o.patches or [ ]) ++ [ ./memcheck-operand.patch ];
+ });
# the QEMU plugin recording a run's leakage trace per
# instruction, and the QEMU that runs a harness under it, for
diff --git a/nix/memcheck-operand.patch b/nix/memcheck-operand.patch
@@ -0,0 +1,316 @@
+memcheck lets an undefined operand flow into a division's quotient
+without a word: it reports an undefined value only where it decides a
+branch or forms an address. An integer division takes a time that
+depends on its operands, so a division of or by a secret leaks it,
+and a taint trace should say so.
+
+This adds an error kind, UninitOperand ("Integer division depends on
+uninitialised value(s)", suppressed as "Operand"), with its origin
+tracked as a condition's is, and reports it for each undefined
+operand of every integer division the guest's code is lifted to:
+DivModU/S128to64, 64to32, 64to64, and 32to32 (x86_64's DIV and IDIV
+among them), DivU/S32 and 64 and their E forms (aarch64's UDIV and
+SDIV), and the 128-bit divisions and modulos. Unlike the checks
+before an address or a branch, it leaves the operands undefined
+after reporting them, so the quotient's undefinedness, and what is
+reported downstream of it, is as it would have been.
+
+--- a/memcheck/mc_errors.c
++++ b/memcheck/mc_errors.c
+@@ -63,6 +63,7 @@
+ enum {
+ Err_Value,
+ Err_Cond,
++ Err_Operand,
+ Err_CoreMem,
+ Err_Addr,
+ Err_Jump,
+@@ -108,6 +109,14 @@
+ ExeContext* origin_ec; // filled in later
+ } Cond;
+
++ // Use of an undefined value as an operand of an integer
++ // division, whose time depends on its operands.
++ struct {
++ // Origin info
++ UInt otag; // origin tag
++ ExeContext* origin_ec; // filled in later
++ } Operand;
++
+ // Addressability error in core (signal-handling) operation.
+ // It would be good to get rid of this error kind, merge it with
+ // another one somehow.
+@@ -527,6 +536,26 @@
+ }
+ break;
+
++ case Err_Operand:
++ MC_(any_value_errors) = True;
++ if (xml) {
++ emit( " <kind>UninitOperand</kind>\n" );
++ emit( " <what>Integer division depends"
++ " on uninitialised value(s)</what>\n" );
++ VG_(pp_ExeContext)( VG_(get_error_where)(err) );
++ if (extra->Err.Operand.origin_ec)
++ mc_pp_origin( extra->Err.Operand.origin_ec,
++ extra->Err.Operand.otag & 3 );
++ } else {
++ emit( "Integer division depends"
++ " on uninitialised value(s)\n" );
++ VG_(pp_ExeContext)( VG_(get_error_where)(err) );
++ if (extra->Err.Operand.origin_ec)
++ mc_pp_origin( extra->Err.Operand.origin_ec,
++ extra->Err.Operand.otag & 3 );
++ }
++ break;
++
+ case Err_RegParam:
+ MC_(any_value_errors) = True;
+ if (xml) {
+@@ -936,6 +965,18 @@
+ VG_(maybe_record_error)( tid, Err_Cond, /*addr*/0, /*s*/NULL, &extra );
+ }
+
++void MC_(record_operand_error) ( ThreadId tid, UInt otag )
++{
++ MC_Error extra;
++ tl_assert( MC_(clo_mc_level) >= 2 );
++ if (otag > 0)
++ tl_assert( MC_(clo_mc_level) == 3 );
++ extra.Err.Operand.otag = otag;
++ extra.Err.Operand.origin_ec = NULL; /* Filled in later */
++ VG_(maybe_record_error)( tid, Err_Operand, /*addr*/0, /*s*/NULL,
++ &extra );
++}
++
+ /* --- Called from non-generated code --- */
+
+ /* This is for memory errors in signal-related memory. */
+@@ -1214,6 +1255,7 @@
+ case Err_IllegalMempool:
+ case Err_Overlap:
+ case Err_Cond:
++ case Err_Operand:
+ case Err_ReallocSizeZero:
+ case Err_UnsafeZeroSize:
+ return True;
+@@ -1423,6 +1465,10 @@
+ update_origin( &extra->Err.Cond.origin_ec,
+ extra->Err.Cond.otag );
+ return sizeof(MC_Error);
++ case Err_Operand:
++ update_origin( &extra->Err.Operand.origin_ec,
++ extra->Err.Operand.otag );
++ return sizeof(MC_Error);
+ case Err_RegParam:
+ update_origin( &extra->Err.RegParam.origin_ec,
+ extra->Err.RegParam.otag );
+@@ -1557,6 +1603,9 @@
+ // Undefined value error in conditional.
+ CondSupp,
+
++ // Undefined value error in an integer division's operand.
++ OperandSupp,
++
+ // Unaddressable read/write attempt at given size
+ Addr1Supp, Addr2Supp, Addr4Supp, Addr8Supp, Addr16Supp, Addr32Supp,
+
+@@ -1593,6 +1642,7 @@
+ else if (VG_STREQ(name, "Overlap")) skind = OverlapSupp;
+ else if (VG_STREQ(name, "Mempool")) skind = MempoolSupp;
+ else if (VG_STREQ(name, "Cond")) skind = CondSupp;
++ else if (VG_STREQ(name, "Operand")) skind = OperandSupp;
+ else if (VG_STREQ(name, "Value0")) skind = CondSupp; /* backwards compat */
+ else if (VG_STREQ(name, "Value1")) skind = Value1Supp;
+ else if (VG_STREQ(name, "Value2")) skind = Value2Supp;
+@@ -1739,6 +1789,9 @@
+ case CondSupp:
+ return (ekind == Err_Cond);
+
++ case OperandSupp:
++ return (ekind == Err_Operand);
++
+ case Addr1Supp: su_szB = 1; goto addr_case;
+ case Addr2Supp: su_szB = 2; goto addr_case;
+ case Addr4Supp: su_szB = 4; goto addr_case;
+@@ -1822,6 +1875,7 @@
+ case Err_Overlap: return "Overlap";
+ case Err_Leak: return "Leak";
+ case Err_Cond: return "Cond";
++ case Err_Operand: return "Operand";
+ case Err_FishyValue: return "FishyValue";
+ case Err_ReallocSizeZero: return "ReallocZero";
+ case Err_BadAlign: return "BadAlign";
+--- a/memcheck/mc_include.h
++++ b/memcheck/mc_include.h
+@@ -551,6 +551,7 @@
+ void MC_(record_address_error) ( ThreadId tid, Addr a, Int szB,
+ Bool isWrite );
+ void MC_(record_cond_error) ( ThreadId tid, UInt otag );
++void MC_(record_operand_error) ( ThreadId tid, UInt otag );
+ void MC_(record_value_error) ( ThreadId tid, Int szB, UInt otag );
+ void MC_(record_jump_error) ( ThreadId tid, Addr a );
+
+@@ -773,6 +774,7 @@
+ VG_REGPARM(1) void MC_(helperc_value_check4_fail_w_o) ( UWord );
+ VG_REGPARM(1) void MC_(helperc_value_check1_fail_w_o) ( UWord );
+ VG_REGPARM(1) void MC_(helperc_value_check0_fail_w_o) ( UWord );
++VG_REGPARM(1) void MC_(helperc_operand_check_fail_w_o) ( UWord );
+
+ /* And call these ones instead to report an uninitialised value error
+ but with no origin available. */
+@@ -781,6 +783,7 @@
+ VG_REGPARM(0) void MC_(helperc_value_check4_fail_no_o) ( void );
+ VG_REGPARM(0) void MC_(helperc_value_check1_fail_no_o) ( void );
+ VG_REGPARM(0) void MC_(helperc_value_check0_fail_no_o) ( void );
++VG_REGPARM(0) void MC_(helperc_operand_check_fail_no_o) ( void );
+
+ /* V-bits load/store helpers */
+ VG_REGPARM(1) void MC_(helperc_STOREV64be) ( Addr, ULong );
+--- a/memcheck/mc_main.c
++++ b/memcheck/mc_main.c
+@@ -5751,6 +5751,11 @@
+ }
+
+ VG_REGPARM(1)
++void MC_(helperc_operand_check_fail_w_o) ( UWord origin ) {
++ MC_(record_operand_error) ( VG_(get_running_tid)(), (UInt)origin );
++}
++
++VG_REGPARM(1)
+ void MC_(helperc_value_check1_fail_w_o) ( UWord origin ) {
+ MC_(record_value_error) ( VG_(get_running_tid)(), 1, (UInt)origin );
+ }
+@@ -5775,6 +5780,11 @@
+ VG_REGPARM(0)
+ void MC_(helperc_value_check0_fail_no_o) ( void ) {
+ MC_(record_cond_error) ( VG_(get_running_tid)(), 0/*origin*/ );
++}
++
++VG_REGPARM(0)
++void MC_(helperc_operand_check_fail_no_o) ( void ) {
++ MC_(record_operand_error) ( VG_(get_running_tid)(), 0/*origin*/ );
+ }
+
+ VG_REGPARM(0)
+--- a/memcheck/mc_translate.c
++++ b/memcheck/mc_translate.c
+@@ -1772,6 +1772,57 @@
+ }
+
+
++/* Check the supplied *original* atoms, the operands of an integer
++ division, for undefinedness, and emit a complaint for each that is
++ undefined. A division takes a time that depends on its operands,
++ so an undefined operand is reported as its own kind of error
++ (Err_Operand), apart from a value used as an address or a
++ condition. Unlike complainIfUndefined, the atoms are not then
++ marked defined: the quotient carries its operands' undefinedness
++ on, as it would had nothing been reported. */
++static void complainIfOperandsUndefined ( MCEnv* mce,
++ IRAtom* atom1, IRAtom* atom2 )
++{
++ IRAtom* atoms[2] = { atom1, atom2 };
++ Int k;
++
++ if (MC_(clo_mc_level) == 1)
++ return;
++
++ for (k = 0; k < 2; k++) {
++ IRAtom* vatom;
++ IRAtom* origin;
++ IRDirty* di;
++
++ tl_assert(isOriginalAtom(mce, atoms[k]));
++ vatom = expr2vbits( mce, atoms[k], HuOth );
++ tl_assert(isShadowAtom(mce, vatom));
++
++ if (MC_(clo_mc_level) == 3) {
++ origin = schemeE( mce, atoms[k] );
++ if (mce->hWordTy == Ity_I64) {
++ origin = assignNew( 'B', mce, Ity_I64,
++ unop(Iop_32Uto64, origin) );
++ }
++ di = unsafeIRDirty_0_N(
++ 1, "MC_(helperc_operand_check_fail_w_o)",
++ VG_(fnptr_to_fnentry)(
++ &MC_(helperc_operand_check_fail_w_o) ),
++ mkIRExprVec_1(origin) );
++ } else {
++ di = unsafeIRDirty_0_N(
++ 0, "MC_(helperc_operand_check_fail_no_o)",
++ VG_(fnptr_to_fnentry)(
++ &MC_(helperc_operand_check_fail_no_o) ),
++ mkIRExprVec_0() );
++ }
++ di->guard = mkPCastTo( mce, Ity_I1, vatom );
++ setHelperAnns( mce, di );
++ stmt( 'V', mce, IRStmt_Dirty(di) );
++ }
++}
++
++
+ /*------------------------------------------------------------*/
+ /*--- Shadowing PUTs/GETs, and indexed variants thereof ---*/
+ /*------------------------------------------------------------*/
+@@ -4153,6 +4204,7 @@
+ case Iop_ModU128:
+ case Iop_ModS128:
+ /* I128 x I128 -> I128 */
++ complainIfOperandsUndefined(mce, atom1, atom2);
+ return mkLazy2(mce, Ity_V128, vatom1, vatom2);
+
+ case Iop_QNarrowBin64Sto32Sx4:
+@@ -4687,10 +4739,12 @@
+
+ case Iop_DivModU64to32:
+ case Iop_DivModS64to32:
++ complainIfOperandsUndefined(mce, atom1, atom2);
+ return mkLazy2(mce, Ity_I64, vatom1, vatom2);
+
+ case Iop_DivModU128to64:
+ case Iop_DivModS128to64:
++ complainIfOperandsUndefined(mce, atom1, atom2);
+ return mkLazy2(mce, Ity_I128, vatom1, vatom2);
+
+ case Iop_8HLto16:
+@@ -4703,6 +4757,7 @@
+ case Iop_DivModU64to64:
+ case Iop_DivModS64to64: {
+ IRAtom* vTmp64 = mkLazy2(mce, Ity_I64, vatom1, vatom2);
++ complainIfOperandsUndefined(mce, atom1, atom2);
+ return assignNew('V', mce, Ity_I128,
+ binop(Iop_64HLto128, vTmp64, vTmp64));
+ }
+@@ -4718,6 +4773,7 @@
+ case Iop_DivModU32to32:
+ case Iop_DivModS32to32: {
+ IRAtom* vTmp32 = mkLazy2(mce, Ity_I32, vatom1, vatom2);
++ complainIfOperandsUndefined(mce, atom1, atom2);
+ return assignNew('V', mce, Ity_I64,
+ binop(Iop_32HLto64, vTmp32, vTmp32));
+ }
+@@ -4745,11 +4801,14 @@
+ return assignNew('V', mce, Ity_I16, binop(Iop_8HLto16, vHi8, vLo8));
+ }
+
+- case Iop_Sad8Ux4: /* maybe we could do better? ftm, do mkLazy2. */
+ case Iop_DivS32:
+ case Iop_DivU32:
+ case Iop_DivU32E:
+ case Iop_DivS32E:
++ complainIfOperandsUndefined(mce, atom1, atom2);
++ return mkLazy2(mce, Ity_I32, vatom1, vatom2);
++
++ case Iop_Sad8Ux4: /* maybe we could do better? ftm, do mkLazy2. */
+ case Iop_QAdd32S: /* could probably do better */
+ case Iop_QSub32S: /* could probably do better */
+ return mkLazy2(mce, Ity_I32, vatom1, vatom2);
+@@ -4758,6 +4817,7 @@
+ case Iop_DivU64:
+ case Iop_DivS64E:
+ case Iop_DivU64E:
++ complainIfOperandsUndefined(mce, atom1, atom2);
+ return mkLazy2(mce, Ity_I64, vatom1, vatom2);
+
+ case Iop_Add32:
diff --git a/nix/probe.nix b/nix/probe.nix
@@ -52,7 +52,8 @@ let
# each report's (class, function) pairs in the harness, sorted
expected = {
trace = [ [ "address" "lookup" ] [ "control" "branchy" ]
- [ "control" "calls" ] ];
+ [ "control" "calls" ] [ "operand" "divide" ]
+ [ "operand" "divide_memory" ] ];
diff = [ [ "address" "lookup" ] [ "control" "branchy" ]
[ "control" "calls" ] [ "operand" "divide" ]
[ "operand" "divide_memory" ] ];
@@ -74,6 +75,14 @@ pkgs.runCommand "vestigia-probe-check" {
check ${diff}/diff.json \
'[.origins[] | [.class, .frames[0].function]] | unique' \
'${builtins.toJSON expected.diff}'
+
+ # both instruments name each instruction they both saw by one
+ # address: a division memcheck reports where it divides, not at the
+ # memory access before it
+ check ${trace}/trace.json \
+ '[.sites[] | select(.class == "operand") | .offset] | sort' \
+ "$(jq -c '[.origins[] | select(.class == "operand") | .offset]
+ | sort' ${diff}/diff.json)"
${lib.optionalString x86_64 ''
check ${diffCross}/diff.json \
'[.origins[] | [.class, .frames[0].function]] | unique' \
