commit d6d86b943a2ac2d3b97686c8911d08655f420bbf
parent 8d46e7117f4f6961f0c197430a3a055b1c01ad75
Author: Jared Tobin <jared@jtobin.io>
Date: Sat, 17 Oct 2026 21:32:37 +0400
spikes: ppad-poly1305 and ppad-secp256k1, and the FFI marks
Diffstat:
15 files changed, 755 insertions(+), 0 deletions(-)
diff --git a/app/Main.hs b/app/Main.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE OverloadedStrings #-}
-- |
@@ -14,6 +15,8 @@ module Main (
) where
import Control.Exception (IOException, try)
+import Control.Monad (when)
+import Foreign.C.Types (CInt(..))
import qualified Data.ByteString as BS
import Data.Version (showVersion)
import qualified Data.Text as T
@@ -35,6 +38,11 @@ import Vestigia.Memcheck (readMemcheck)
import Vestigia.Symbol (symbolize)
import Vestigia.Trace (trace, traceJson, traceSummary)
+-- address-space randomisation off, for this process and its
+-- children; nonzero where it cannot be (cbits/norandom.c)
+foreign import ccall unsafe "vestigia_no_randomize"
+ c_noRandomize :: IO CInt
+
data Opts = Opts {
oValgrind :: !(Maybe FilePath)
, oXml :: !(Maybe FilePath)
@@ -188,6 +196,11 @@ tool opt var dflt = do
record :: Opts -> FilePath -> [String] -> IO ()
record o prog progArgs = do
dump <- maybe (usage "record: --dump FILE is needed") pure (oDump o)
+ -- runs to be compared must lay memory out alike
+ fixed <- c_noRandomize
+ when (fixed /= 0) $ hPutStrLn stderr
+ "vestigia: address randomisation is still on; runs may differ \
+ \in layout, and so everywhere"
qemu <- tool (oQemu o) "VESTIGIA_QEMU" "qemu-x86_64"
plugin <- tool (oPlugin o) "VESTIGIA_PLUGIN" "libvestigia-qemu.so"
r <- try (withCreateProcess
diff --git a/cbits/norandom.c b/cbits/norandom.c
@@ -0,0 +1,23 @@
+/*
+ * norandom.c: address-space randomisation off for this process and
+ * every process it starts.
+ *
+ * Copyright (c) 2026 Jared Tobin
+ * License: MIT
+ *
+ * Runs compared to find where a secret mattered must lay memory out
+ * alike, or every address differs between them and none of the
+ * differences means anything. The personality is inherited across
+ * fork and exec, so setting it before starting QEMU covers the guest.
+ */
+#ifdef __linux__
+#include <sys/personality.h>
+
+int vestigia_no_randomize(void) {
+ int p = personality(0xffffffff);
+ if (p == -1) return -1;
+ return personality((unsigned long)p | ADDR_NO_RANDOMIZE) == -1 ? -1 : 0;
+}
+#else
+int vestigia_no_randomize(void) { return -1; }
+#endif
diff --git a/etc/spike/poly1305/Harness.hs b/etc/spike/poly1305/Harness.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE ForeignFunctionInterface #-}
+
+-- | ppad-poly1305 under vestigia: each run draws a fresh one-time
+-- key, marked secret, and MACs a fixed set of public messages,
+-- comparing each tag with a public candidate.
+--
+-- usage: harness [RUNS [SEED]]
+--
+-- SEED (hex) seeds the keys alone; the messages and candidates
+-- come from a fixed stream, so runs that differ in SEED differ
+-- only in their keys.
+
+module Main (
+ main
+ ) where
+
+import Control.Monad (forM_)
+import qualified Crypto.MAC.Poly1305 as P
+import Data.Bits (shiftR, xor)
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Unsafe as BU
+import Data.IORef (modifyIORef', newIORef, readIORef, writeIORef)
+import Data.Word (Word64)
+import Foreign.C.Types (CSize(..))
+import Foreign.Ptr (Ptr, castPtr)
+import Numeric (readHex)
+import System.Environment (getArgs)
+
+foreign import ccall unsafe "vestigia_secret_c"
+ c_secret :: Ptr () -> CSize -> IO ()
+
+foreign import ccall unsafe "vestigia_public_c"
+ c_public :: Ptr () -> CSize -> IO ()
+
+mark :: (Ptr () -> CSize -> IO ()) -> BS.ByteString -> IO ()
+mark f bs =
+ BU.unsafeUseAsCStringLen bs (\(p, n) -> f (castPtr p) (fromIntegral n))
+
+splitmix :: Word64 -> (Word64, Word64)
+splitmix s0 =
+ let s = s0 + 0x9e3779b97f4a7c15
+ z1 = (s `xor` (s `shiftR` 30)) * 0xbf58476d1ce4e5b9
+ z2 = (z1 `xor` (z1 `shiftR` 27)) * 0x94d049bb133111eb
+ in (z2 `xor` (z2 `shiftR` 31), s)
+
+bytes :: Int -> Word64 -> (BS.ByteString, Word64)
+bytes n s0 = go n s0 []
+ where
+ go 0 s acc = (BS.pack (reverse acc), s)
+ go k s acc =
+ let (x, s') = splitmix s in go (k - 1) s' (fromIntegral x : acc)
+
+-- message lengths around the 16-byte block: empty, short final
+-- chunks, exact blocks
+lengths :: [Int]
+lengths = [ 0, 1, 15, 16, 17, 31, 32, 33, 64, 100 ]
+
+main :: IO ()
+main = do
+ args <- getArgs
+ let runs = case args of
+ (r : _) | [ (n, "") ] <- reads r -> n
+ _ -> 2 :: Int
+ seed = case args of
+ (_ : s : _) | [ (n, "") ] <- readHex s -> n
+ _ -> 1
+ let (messages, _) = foldr
+ (\l (ms, s) -> let (m, s') = bytes l s in (m : ms, s'))
+ ([], 0x0123456789abcdef) lengths
+ candidates = [ fst (bytes 16 (0xfeed + fromIntegral k))
+ | k <- [ 0 .. length lengths - 1 ] ]
+ secrets <- newIORef seed
+ matches <- newIORef (0 :: Int)
+ forM_ [ 1 .. runs ] $ \_ -> do
+ s <- readIORef secrets
+ let (key, s') = bytes 32 s
+ writeIORef secrets s'
+ mark c_secret key
+ forM_ (zip messages candidates) $ \(m, c) -> case P.mac key m of
+ Just t -> do
+ let ok = t == P.MAC c
+ modifyIORef' matches (+ fromEnum ok)
+ Nothing -> pure ()
+ n <- readIORef matches
+ putStrLn (show runs <> " run(s), " <> show n <> " match(es)")
diff --git a/etc/spike/poly1305/RESULTS.md b/etc/spike/poly1305/RESULTS.md
@@ -0,0 +1,49 @@
+# Spike 2: ppad-poly1305 on x86_64-linux
+
+Target: ppad-poly1305 0.4.6 (173e478), GHC 9.10.3 with LLVM, as
+released and with each of the elenchus vectors' mutant sets
+(`mutants-1.patch`, `mutants-2.patch`). The harness MACs ten public
+messages (empty, short final chunks, exact blocks) under fresh
+secret keys and compares each tag with a public candidate. Sites
+are named by the harness binary's symbols (no line tables).
+
+## Cost
+
+About 1.6 seconds per memcheck trace (four keys) and 1.9 seconds
+per three-run diff, on pollux.
+
+## Findings
+
+- release: one memcheck site, the harness's branch on the result of
+ `(==)` (whether the tag matched: public by intent). Nothing in
+ the library; no differential origin in the harness binary.
+- mutants-1:
+ - L3, the key-indexed nibble table in clamp: an address site in
+ `$wmac_slow`, x144 (four key bytes, nine non-empty messages,
+ four keys); also a differential address origin.
+ - L1, the variable-time compare in `reduce_full`: control sites
+ in `$wmac`.
+ - L2, the early-exit tag compare: one site where release has its
+ result branch. memcheck alone cannot tell the two apart; the
+ explain step must. The differential traces cannot see L2 at
+ all with random candidates, which mismatch at byte 0 every
+ time: it needs a designed input (a candidate sharing a prefix
+ with the true tag).
+ - D1 and D2, the decoys on the public message: not flagged.
+- mutants-2:
+ - X2, the skip-multiply branch: control sites in `$wmac`.
+ - `(==)` without its barrier: stayed constant time, as on
+ aarch64 (the same result branch as release).
+
+## Lessons for GHC harnesses
+
+- The runtime's default terabyte address-space reservation makes
+ memcheck crawl (ten seconds for a trivial program, apparent hangs
+ for real ones). `-with-rtsopts=-xr1G` fixes it.
+- `-V0` (no interval timer) keeps the scheduler deterministic for
+ differential runs.
+- Address-space randomisation made identical runs differ at 2183
+ places; `vestigia record` now turns it off for itself and QEMU.
+- A seed passed as an argument is decoded by libc, which shows as
+ origins in libc; differential origins are filtered to the
+ harness binary, which holds the whole Haskell program.
diff --git a/etc/spike/poly1305/default.nix b/etc/spike/poly1305/default.nix
@@ -0,0 +1,68 @@
+# Spike 2: ppad-poly1305 under vestigia, on x86_64-linux: the
+# release (173e478) and the elenchus vectors' two mutant sets.
+#
+# nix build --impure -f etc/spike/poly1305 all
+let
+ system = "x86_64-linux";
+ vestigia = builtins.getFlake (toString ../../..);
+ poly = builtins.getFlake ("git+file:///Users/jtobin/src/ppad/poly1305"
+ + "?rev=173e478290ecf9d639f0c85ae625da474a62a6b2");
+ pkgs = import vestigia.inputs.nixpkgs { inherit system; };
+ hlib = pkgs.haskell.lib;
+ llvm = pkgs.llvmPackages_19.llvm;
+ clang = pkgs.llvmPackages_19.clang;
+ withLlvm = p: hlib.addBuildTools (hlib.enableCabalFlag p "llvm")
+ [ llvm clang ];
+
+ variant = name: patches:
+ let
+ hpkgs = pkgs.haskell.packages.ghc910.extend (new: old: {
+ ppad-base16 =
+ withLlvm poly.inputs.ppad-base16.packages.${system}.default;
+ ppad-fixed =
+ withLlvm poly.inputs.ppad-fixed.packages.${system}.default;
+ ppad-poly1305 = withLlvm (hlib.dontCheck (hlib.appendPatches
+ (new.callCabal2nix "ppad-poly1305" poly.outPath { })
+ patches));
+ });
+ ghc = hpkgs.ghcWithPackages (p: [ p.ppad-poly1305 ]);
+ harness = pkgs.runCommandCC "poly1305-${name}-harness" {
+ nativeBuildInputs = [ ghc llvm clang ];
+ } ''
+ mkdir -p $out/bin build
+ cp ${./Harness.hs} build/Harness.hs
+ cp ${vestigia.packages.${system}.include}/include/vestigia-ffi.c build/marks.c
+ cd build
+ # a small address-space reservation, since memcheck pays for
+ # the runtime's default terabyte on every run, and no
+ # interval timer, so runs that differ only in their keys
+ # schedule alike
+ ghc -O2 -rtsopts '-with-rtsopts=-xr1G -V0' Harness.hs marks.c \
+ -I${vestigia.packages.${system}.include}/include \
+ -I${vestigia.lib.${system}.valgrindDev}/include \
+ -o $out/bin/harness
+ '';
+ bin = "${harness}/bin/harness";
+ seeds = [ "1" "2" "3" ];
+ in pkgs.linkFarm "poly1305-${name}" [
+ { name = "trace";
+ path = vestigia.lib.${system}.traceOf {
+ name = "poly1305-${name}";
+ harness = bin;
+ args = [ "4" "1" ];
+ }; }
+ { name = "diff";
+ path = vestigia.lib.${system}.diffOf {
+ name = "poly1305-${name}";
+ harness = bin;
+ runs = map (s: [ "2" s ]) seeds;
+ }; }
+ ];
+in
+{
+ all = pkgs.linkFarm "poly1305-spike" [
+ { name = "release"; path = variant "release" [ ]; }
+ { name = "mutants-1"; path = variant "mutants-1" [ ./mutants-1.patch ]; }
+ { name = "mutants-2"; path = variant "mutants-2" [ ./mutants-2.patch ]; }
+ ];
+}
diff --git a/etc/spike/poly1305/mutants-1.patch b/etc/spike/poly1305/mutants-1.patch
@@ -0,0 +1,116 @@
+From f586b1456b5f154481db567da20bba724ec12cc1 Mon Sep 17 00:00:00 2001
+From: Jared Tobin <jared@jtobin.io>
+Date: Tue, 6 Oct 2026 11:44:42 +0400
+Subject: [PATCH] exp: timing mutants for elenchus baselines
+
+---
+ lib/Crypto/MAC/Poly1305.hs | 53 +++++++++++++++++++++-----------------
+ 1 file changed, 30 insertions(+), 23 deletions(-)
+
+diff --git a/lib/Crypto/MAC/Poly1305.hs b/lib/Crypto/MAC/Poly1305.hs
+index fb0c261..aa919be 100644
+--- a/lib/Crypto/MAC/Poly1305.hs
++++ b/lib/Crypto/MAC/Poly1305.hs
+@@ -27,7 +27,6 @@ module Crypto.MAC.Poly1305 (
+ ) where
+
+ import qualified Crypto.MAC.Poly1305.Arm as Arm
+-import Data.Barrier (barrier)
+ import qualified Data.Bits as B
+ import qualified Data.ByteString as BS
+ import qualified Data.ByteString.Internal as BI
+@@ -131,8 +130,23 @@ shr130 (Wider (# _, _, l2, l3 #)) =
+
+ -------------------------------------------------------------------------------
+
++-- clear the top four bits of r's bytes 3, 7, 11, and 15
++nibble :: BS.ByteString
++nibble = BS.pack [ fromIntegral (j B..&. 0x0f) | j <- [0 .. 255 :: Int] ]
++{-# NOINLINE nibble #-}
++
++clamp_bytes :: BS.ByteString -> BS.ByteString
++clamp_bytes k = BS.pack (fmap byte [0 .. 15])
++ where
++ byte :: Int -> Word8
++ byte i
++ | i B..&. 3 == 3 =
++ BU.unsafeIndex nibble (fromIntegral (BU.unsafeIndex k i))
++ | otherwise = BU.unsafeIndex k i
++
++-- clear the bottom two bits of r's bytes 4, 8, and 12
+ clamp :: Wider -> Wider
+-clamp r = r `W.and` 0x0ffffffc0ffffffc0ffffffc0fffffff
++clamp r = r `W.and` 0xfffffffcfffffffcfffffffcffffffff
+ {-# INLINE clamp #-}
+
+ -- | A Poly1305 message authentication code.
+@@ -156,22 +170,13 @@ instance Eq MAC where
+ -- Runs in variable-time only for invalid inputs.
+ (MAC a@(BI.PS _ _ la)) == (MAC b@(BI.PS _ _ lb))
+ | la /= lb = False
+- | otherwise = go 0 0
++ | otherwise = go 0
+ where
+- -- fused fold: OR the bytewise XORs into an accumulator
+- -- directly, rather than via packZipWith, so no intermediate
+- -- ByteString holding the (secret-derived) difference bytes
+- -- is ever materialised on the heap. The accumulator is routed
+- -- through 'barrier' before the zero-test so the LLVM backend
+- -- cannot recover the array-equality idiom and short-circuit on
+- -- the first mismatch (see "Data.Barrier").
+- go :: Word8 -> Int -> Bool
+- go !acc !i
+- | i == la = barrier acc == 0
+- | otherwise =
+- let !x = BU.unsafeIndex a i
+- !y = BU.unsafeIndex b i
+- in go (acc B..|. B.xor x y) (i + 1)
++ go :: Int -> Bool
++ go !i
++ | i == la = True
++ | BU.unsafeIndex a i /= BU.unsafeIndex b i = False
++ | otherwise = go (i + 1)
+
+ -- | Produce a Poly1305 MAC for the provided message, given the
+ -- provided key.
+@@ -189,10 +194,12 @@ mac
+ -> Maybe MAC -- ^ 128-bit message authentication code
+ mac key@(BI.PS _ _ kl) msg
+ | kl /= 32 = Nothing
++ | BS.null msg = pure $! MAC (BS.copy (BS.drop 16 key))
+ | Arm.poly1305_arm_available =
+ pure $! MAC (Arm.mac key msg)
+ | otherwise =
+- let (clamp . _roll16 -> r, _roll16 -> s) = BS.splitAt 16 key
++ let (clamp . _roll16 . clamp_bytes -> r, _roll16 -> s) =
++ BS.splitAt 16 key
+ in pure $! (MAC (_poly1305_loop r s msg))
+
+ -- p = 2^130 - 5
+@@ -217,10 +224,9 @@ reduce_full h =
+ !hi = shr130 h
+ !h' = lo + 5 * hi
+ !h_5 = h' + 5
+- !reduced = h_5 `W.and` mask130
+- !carry = shr130 h_5
+- !gte = W.lt 0 carry
+- in W.select h' reduced gte
++ in if W.lt_vartime mask130 h_5
++ then h_5 `W.and` mask130
++ else h'
+ {-# INLINE reduce_full #-}
+
+ _poly1305_loop :: Wider -> Wider -> BS.ByteString -> BS.ByteString
+@@ -231,7 +237,8 @@ _poly1305_loop !r !s !msg =
+ let !final = reduce_full (reduce_partial acc)
+ in unroll16 (final + s)
+ | otherwise ->
+- let !n = _roll16 chunk `W.or` set_hi l
++ let !n | BS.all (== 0) chunk = set_hi l
++ | otherwise = _roll16 chunk `W.or` set_hi l
+ !prod = r * (acc + n)
+ !nacc = reduce_partial (reduce_partial prod)
+ in loop nacc etc
+--
+2.55.0
+
diff --git a/etc/spike/poly1305/mutants-2.patch b/etc/spike/poly1305/mutants-2.patch
@@ -0,0 +1,74 @@
+From ab7f9911e3a1817a887adfb43a4bc020fe849c4c Mon Sep 17 00:00:00 2001
+From: Jared Tobin <jared@jtobin.io>
+Date: Tue, 6 Oct 2026 12:18:02 +0400
+Subject: [PATCH] exp: compiler-level timing mutants for elenchus baselines
+
+---
+ lib/Crypto/MAC/Poly1305.hs | 24 ++++++++++++++----------
+ 1 file changed, 14 insertions(+), 10 deletions(-)
+
+diff --git a/lib/Crypto/MAC/Poly1305.hs b/lib/Crypto/MAC/Poly1305.hs
+index fb0c261..fed41ad 100644
+--- a/lib/Crypto/MAC/Poly1305.hs
++++ b/lib/Crypto/MAC/Poly1305.hs
+@@ -27,8 +27,8 @@ module Crypto.MAC.Poly1305 (
+ ) where
+
+ import qualified Crypto.MAC.Poly1305.Arm as Arm
+-import Data.Barrier (barrier)
+ import qualified Data.Bits as B
++import qualified Data.Choice as C
+ import qualified Data.ByteString as BS
+ import qualified Data.ByteString.Internal as BI
+ import qualified Data.ByteString.Unsafe as BU
+@@ -161,13 +161,10 @@ instance Eq MAC where
+ -- fused fold: OR the bytewise XORs into an accumulator
+ -- directly, rather than via packZipWith, so no intermediate
+ -- ByteString holding the (secret-derived) difference bytes
+- -- is ever materialised on the heap. The accumulator is routed
+- -- through 'barrier' before the zero-test so the LLVM backend
+- -- cannot recover the array-equality idiom and short-circuit on
+- -- the first mismatch (see "Data.Barrier").
++ -- is ever materialised on the heap.
+ go :: Word8 -> Int -> Bool
+ go !acc !i
+- | i == la = barrier acc == 0
++ | i == la = acc == 0
+ | otherwise =
+ let !x = BU.unsafeIndex a i
+ !y = BU.unsafeIndex b i
+@@ -206,8 +203,10 @@ mask130 = 0x3ffffffffffffffffffffffffffffffff
+ reduce_partial :: Wider -> Wider
+ reduce_partial x =
+ let !lo = x `W.and` mask130
+- !hi = shr130 x
+- in lo + 5 * hi
++ !hi@(Wider (# Limb h0, Limb h1, _, _ #)) = shr130 x
++ in if Exts.isTrue# (Exts.eqWord# (Exts.or# h0 h1) 0##)
++ then lo
++ else lo + 5 * hi
+ {-# INLINE reduce_partial #-}
+
+ -- [0, 2 ^ 131) -> [0, p)
+@@ -218,11 +217,16 @@ reduce_full h =
+ !h' = lo + 5 * hi
+ !h_5 = h' + 5
+ !reduced = h_5 `W.and` mask130
+- !carry = shr130 h_5
+- !gte = W.lt 0 carry
++ !(Wider (# Limb c, _, _, _ #)) = shr130 h_5
++ !gte = C.from_bit# (bit (Exts.isTrue# (Exts.neWord# c 0##)))
+ in W.select h' reduced gte
+ {-# INLINE reduce_full #-}
+
++-- 1 for True, 0 for False
++bit :: Bool -> Exts.Word#
++bit b = if b then 1## else 0##
++{-# INLINE bit #-}
++
+ _poly1305_loop :: Wider -> Wider -> BS.ByteString -> BS.ByteString
+ _poly1305_loop !r !s !msg =
+ let loop !acc !bs = case BS.splitAt 16 bs of
+--
+2.55.0
+
diff --git a/etc/spike/secp256k1/Harness.hs b/etc/spike/secp256k1/Harness.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ForeignFunctionInterface #-}
+
+-- | ppad-secp256k1 under vestigia: each run draws a fresh secret key
+-- (and Schnorr auxiliary randomness), marked secret, and runs the
+-- library's secret-key roots on fixed public messages: public key
+-- derivation, Schnorr and ECDSA signing (with and without a
+-- precomputed context), and ECDH against a fixed public peer.
+--
+-- usage: harness [RUNS [SEED]]
+--
+-- SEED (hex) seeds the secrets alone, so runs that differ in SEED
+-- differ only in their secrets.
+
+module Main (
+ main
+ ) where
+
+import Control.Monad (forM_)
+import qualified Crypto.Curve.Secp256k1 as S
+import Data.Bits (shiftR, xor, (.&.))
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Unsafe as BU
+import Data.IORef (modifyIORef', newIORef, readIORef, writeIORef)
+import Data.Word (Word64)
+import Foreign.C.Types (CSize(..))
+import Foreign.Ptr (Ptr, castPtr)
+import Numeric (readHex)
+import System.Environment (getArgs)
+
+foreign import ccall unsafe "vestigia_secret_c"
+ c_secret :: Ptr () -> CSize -> IO ()
+
+foreign import ccall unsafe "vestigia_public_c"
+ c_public :: Ptr () -> CSize -> IO ()
+
+mark :: (Ptr () -> CSize -> IO ()) -> BS.ByteString -> IO ()
+mark f bs =
+ BU.unsafeUseAsCStringLen bs (\(p, n) -> f (castPtr p) (fromIntegral n))
+
+splitmix :: Word64 -> (Word64, Word64)
+splitmix s0 =
+ let s = s0 + 0x9e3779b97f4a7c15
+ z1 = (s `xor` (s `shiftR` 30)) * 0xbf58476d1ce4e5b9
+ z2 = (z1 `xor` (z1 `shiftR` 27)) * 0x94d049bb133111eb
+ in (z2 `xor` (z2 `shiftR` 31), s)
+
+bytes :: Int -> Word64 -> (BS.ByteString, Word64)
+bytes n s0 = go n s0 []
+ where
+ go 0 s acc = (BS.pack (reverse acc), s)
+ go k s acc =
+ let (x, s') = splitmix s in go (k - 1) s' (fromIntegral x : acc)
+
+-- a key below the group order: random bytes with the top bit clear
+key :: Word64 -> (BS.ByteString, Word64)
+key s =
+ let (b, s') = bytes 32 s
+ in case BS.uncons b of
+ Just (h, t) -> (BS.cons (h .&. 0x7f) t, s')
+ Nothing -> (b, s')
+
+-- a result's bytes, made public again: a signature is meant to be
+-- revealed
+reveal :: Maybe BS.ByteString -> IO Int
+reveal r = case r of
+ Just b -> mark c_public b >> pure (BS.length b)
+ Nothing -> pure 0
+
+-- a result forced, and nothing of it revealed
+forced :: Maybe a -> IO Int
+forced r = case r of
+ Just !_ -> pure 1
+ Nothing -> pure 0
+
+main :: IO ()
+main = do
+ args <- getArgs
+ let runs = case args of
+ (r : _) | [ (n, "") ] <- reads r -> n
+ _ -> 2 :: Int
+ seed = case args of
+ (_ : s : _) | [ (n, "") ] <- readHex s -> n
+ _ -> 1
+ (msg, p1) = bytes 32 0x0123456789abcdef
+ (peerKey, _) = key p1
+ !tex = S.precompute
+ peer <- case S.parse_int256 peerKey >>= S.derive_pub of
+ Just p -> pure p
+ Nothing -> fail "no peer key"
+ secrets <- newIORef seed
+ total <- newIORef (0 :: Int)
+ forM_ [ 1 .. runs ] $ \_ -> do
+ s <- readIORef secrets
+ let (skBytes, s1) = key s
+ (aux, s2) = bytes 32 s1
+ writeIORef secrets s2
+ mark c_secret skBytes
+ mark c_secret aux
+ case S.parse_int256 skBytes of
+ Nothing -> pure ()
+ Just sk -> do
+ n1 <- forced (S.derive_pub sk)
+ n2 <- reveal (S.sign_schnorr sk msg aux)
+ n3 <- reveal (S.sign_schnorr' tex sk msg aux)
+ n4 <- forced (S.sign_ecdsa sk msg)
+ n5 <- forced (S.sign_ecdsa' tex sk msg)
+ n6 <- forced (S.ecdh peer sk)
+ modifyIORef' total (+ (n1 + n2 + n3 + n4 + n5 + n6))
+ n <- readIORef total
+ putStrLn (show runs <> " run(s), " <> show n <> " result(s)")
diff --git a/etc/spike/secp256k1/RESULTS.md b/etc/spike/secp256k1/RESULTS.md
@@ -0,0 +1,40 @@
+# Spike 3: ppad-secp256k1 on x86_64-linux
+
+Target: ppad-secp256k1 0.5.8 (fdb80d5), GHC 9.10.3 with LLVM, as
+released and with the elenchus vector's mutants: S1 a direct,
+secret-indexed window load in `mul_wnaf#`; S2 a branch on each
+ladder scalar bit (GHC's compilation of a Bool-to-choice helper on
+aarch64); S3 a zero-byte shortcut on the key in Schnorr's xor. The
+harness derives a public key, signs (Schnorr and ECDSA, with and
+without a precomputed context), and runs ECDH, under fresh secret
+keys and auxiliary randomness.
+
+## Cost
+
+About 3.8 seconds per memcheck trace (two keys, every root) and
+3.1 seconds per three-run diff, on pollux.
+
+## Findings
+
+- release: no differential origin in the harness binary. memcheck
+ reports 17 sites, each a validation or declassification the
+ vector labels as such: scalar range and result checks in `mul`,
+ `mul_wnaf`, and the signers, `even_y_vartime` on points that
+ become public, ECDH's `z == 0` result, and the harness's own case
+ analysis of Maybe results.
+- mutants:
+ - S1: 24 address sites in `mul_wnaf`, by both instruments.
+ - S2 and S3: absent, and rightly. `mul` has ten conditional
+ jumps in both builds (the bit test compiled branch-free), and
+ the Schnorr signer has fewer in the mutant than in release (185
+ against 192: LLVM folded `if x == 0 then y else x ^ y` into the
+ XOR it equals). Their leaks are in aarch64's machine code, where
+ the vector was labelled, not x86's.
+
+## What this says
+
+vestigia judges the machine code built, as the audit must:
+compiler-level leaks are per ISA. Seeing S2 and S3 needs aarch64
+traces. QEMU runs aarch64 code on pollux, so differential traces
+need only an aarch64-linux build of the harness; memcheck needs a
+native aarch64-linux host.
diff --git a/etc/spike/secp256k1/default.nix b/etc/spike/secp256k1/default.nix
@@ -0,0 +1,72 @@
+# Spike 3: ppad-secp256k1 under vestigia, on x86_64-linux: the
+# release (fdb80d5), a constant-time control, and the elenchus
+# vector's mutants (S1 a secret-indexed window load, S2 a branch on
+# each ladder bit, S3 a zero-byte shortcut on the key in Schnorr).
+#
+# nix build --impure -f etc/spike/secp256k1 all
+let
+ system = "x86_64-linux";
+ vestigia = builtins.getFlake (toString ../../..);
+ secp = builtins.getFlake ("git+file:///Users/jtobin/src/ppad/secp256k1"
+ + "?rev=fdb80d54b86c61bd1a15e2e8db351091d02c89ee");
+ pkgs = import vestigia.inputs.nixpkgs { inherit system; };
+ hlib = pkgs.haskell.lib;
+ llvm = pkgs.llvmPackages_19.llvm;
+ clang = pkgs.llvmPackages_19.clang;
+ withLlvm = p: hlib.addBuildTools (hlib.enableCabalFlag p "llvm")
+ [ llvm clang ];
+ input = n: withLlvm secp.inputs.${n}.packages.${system}.default;
+
+ variant = name: patches:
+ let
+ hpkgs = pkgs.haskell.packages.ghc910.extend (new: old: {
+ ppad-base16 = input "ppad-base16";
+ ppad-sha256 = input "ppad-sha256";
+ ppad-hmac-drbg = input "ppad-hmac-drbg";
+ ppad-fixed = input "ppad-fixed";
+ ppad-secp256k1 = withLlvm (hlib.dontCheck (hlib.dontBenchmark
+ (hlib.appendPatches
+ (new.callCabal2nix "ppad-secp256k1" secp.outPath {
+ ppad-base16 = new.ppad-base16;
+ ppad-sha256 = new.ppad-sha256;
+ ppad-hmac-drbg = new.ppad-hmac-drbg;
+ ppad-fixed = new.ppad-fixed;
+ })
+ patches)));
+ });
+ ghc = hpkgs.ghcWithPackages (p: [ p.ppad-secp256k1 ]);
+ harness = pkgs.runCommandCC "secp256k1-${name}-harness" {
+ nativeBuildInputs = [ ghc llvm clang ];
+ } ''
+ mkdir -p $out/bin build
+ cp ${./Harness.hs} build/Harness.hs
+ cp ${vestigia.packages.${system}.include}/include/vestigia-ffi.c build/marks.c
+ cd build
+ ghc -O2 -rtsopts '-with-rtsopts=-xr1G -V0' Harness.hs marks.c \
+ -I${vestigia.packages.${system}.include}/include \
+ -I${vestigia.lib.${system}.valgrindDev}/include \
+ -o $out/bin/harness
+ '';
+ bin = "${harness}/bin/harness";
+ in pkgs.linkFarm "secp256k1-${name}" [
+ { name = "trace";
+ path = vestigia.lib.${system}.traceOf {
+ name = "secp256k1-${name}";
+ harness = bin;
+ args = [ "2" "1" ];
+ }; }
+ { name = "diff";
+ path = vestigia.lib.${system}.diffOf {
+ name = "secp256k1-${name}";
+ harness = bin;
+ runs = map (s: [ "1" s ]) [ "1" "2" "3" ];
+ objects = [ "harness" ];
+ }; }
+ ];
+in
+{
+ all = pkgs.linkFarm "secp256k1-spike" [
+ { name = "release"; path = variant "release" [ ]; }
+ { name = "mutants"; path = variant "mutants" [ ./mutants.patch ]; }
+ ];
+}
diff --git a/etc/spike/secp256k1/mutants.patch b/etc/spike/secp256k1/mutants.patch
@@ -0,0 +1,61 @@
+From 9c05ed13307a753e7736b71f3c304269c66fd729 Mon Sep 17 00:00:00 2001
+From: Jared Tobin <jared@jtobin.io>
+Date: Tue, 6 Oct 2026 14:22:36 +0400
+Subject: [PATCH] exp: timing mutants for elenchus baselines
+
+---
+ lib/Crypto/Curve/Secp256k1.hs | 18 ++++++++++++------
+ 1 file changed, 12 insertions(+), 6 deletions(-)
+
+diff --git a/lib/Crypto/Curve/Secp256k1.hs b/lib/Crypto/Curve/Secp256k1.hs
+index 7e220fa..672d1a1 100644
+--- a/lib/Crypto/Curve/Secp256k1.hs
++++ b/lib/Crypto/Curve/Secp256k1.hs
+@@ -293,11 +293,16 @@ modQ :: Wider -> Wider
+ modQ x = W.select x (x - _CURVE_Q) (CT.not (W.lt x _CURVE_Q))
+ {-# INLINABLE modQ #-}
+
+--- bytewise xor
++-- bytewise xor (a zero byte passes the other through)
+ xor :: BS.ByteString -> BS.ByteString -> BS.ByteString
+-xor = BS.packZipWith B.xor
++xor = BS.packZipWith (\x y -> if x == 0 then y else B.xor x y)
+ {-# INLINABLE xor #-}
+
++-- lift a Bool into a constant-time choice
++choice :: Bool -> CT.Choice
++choice b = CT.from_bit# (if b then 1## else 0##)
++{-# INLINE choice #-}
++
+ -- constants ------------------------------------------------------------------
+
+ -- | secp256k1 field prime.
+@@ -578,12 +583,13 @@ mul# (# px, py, pz #) s
+ let !(C.Montgomery o) = C.one
+ in loop (0 :: Int) (# Z, o, Z #) (# px, py, pz #) s
+ where
+- loop !j !a !d !_SECRET
++ loop !j !a !d !_SECRET@(# Limb lo, _, _, _ #)
+ | j == _CURVE_Q_BITS = (# | a #)
+ | otherwise =
+ let !nd = double# d
+- !(# nm, lsb_set #) = W.shr1_c# _SECRET
+- !nacc = select_proj# a (add_proj# a d) lsb_set
++ !(# nm, _ #) = W.shr1_c# _SECRET
++ !lsb = choice (B.testBit (GHC.Word.W# lo) 0)
++ !nacc = select_proj# a (add_proj# a d) lsb
+ in loop (succ j) nacc nd nm
+ {-# INLINE mul# #-}
+
+@@ -645,7 +651,7 @@ mul_wnaf# ctxArray ctxW ls
+ !off_nz = Exts.minusWord# (Exts.plusWord# off0 abs_b) 1##
+ !off = CT.select_word# off0 off_nz (CT.not is_zero)
+
+- !pr = ct_index_proj# ctxArray off0 s off
++ !pr = index_proj# ctxArray (Exts.word2Int# off)
+ !neg_pr = neg# pr
+ !pt_nonzero = select_proj# pr neg_pr bor
+
+--
+2.55.0
+
diff --git a/flake.nix b/flake.nix
@@ -50,6 +50,7 @@
include = pkgs.runCommand "vestigia-include" { } ''
mkdir -p $out/include
cp ${./include/vestigia.h} $out/include/vestigia.h
+ cp ${./include/vestigia-ffi.c} $out/include/vestigia-ffi.c
'';
# the command, with the valgrind it was built against baked in
diff --git a/include/vestigia-ffi.c b/include/vestigia-ffi.c
@@ -0,0 +1,13 @@
+/*
+ * vestigia-ffi.c: vestigia's two marks as functions, for a harness
+ * that reaches them through a foreign function interface (a Haskell
+ * harness's `foreign import ccall`) rather than the header's inline
+ * definitions.
+ *
+ * Copyright (c) 2026 Jared Tobin
+ * License: MIT
+ */
+#include "vestigia.h"
+
+void vestigia_secret_c(void *p, size_t n) { vestigia_secret(p, n); }
+void vestigia_public_c(void *p, size_t n) { vestigia_public(p, n); }
diff --git a/plans/IMPL1.md b/plans/IMPL1.md
@@ -54,3 +54,30 @@ The tool earns its place only if it reproduces known results:
written by a small encoder of our own.
- valgrind enters through nix as a tool. It does not run on Darwin;
traces there need a Linux cell.
+
+## Outcome
+
+Two instruments, not one. memcheck taint (`vestigia run`) sees any
+dependence of a branch or address on a secret's data, even where
+the outcome never varies, but not through control flow: after a
+secret-dependent branch, what the branch builds from public data is
+defined. Differential traces under a QEMU plugin (`vestigia record`
+and `diff`) see what control does to data as well, on any ISA QEMU
+runs, but only what the chosen secrets actually varied, and need
+runs laid out alike (randomisation off). Neither needs a model.
+
+- Penumbra (`etc/spike/penumbra/RESULTS.md`): elenchus's 79 leaks
+ fall in thirteen functions, each with a vestigia site in it and
+ its source line; one to two seconds per root.
+- ppad-poly1305 (`etc/spike/poly1305/RESULTS.md`): every planted
+ leak found, no decoy flagged; release clean but for the harness's
+ use of the comparison result. One leak (an early-exit compare)
+ needs designed inputs for the differential instrument.
+- ppad-secp256k1 (`etc/spike/secp256k1/RESULTS.md`): S1 found; S2
+ and S3 absent from x86's machine code, verified by its branches;
+ release clean but for validation and declassified outputs.
+
+Open: aarch64 traces (an aarch64-linux build of the harness for the
+differential instrument, a native host for memcheck); line tables
+for GHC builds; the explain step, which separates a leak from a
+declassified result (a tag comparison, a validity check).
diff --git a/vestigia.cabal b/vestigia.cabal
@@ -45,6 +45,8 @@ executable vestigia
main-is: Main.hs
ghc-options:
-Wall -Werror -rtsopts
+ c-sources:
+ cbits/norandom.c
other-modules:
Paths_vestigia
autogen-modules:
