lib.nix (8212B)
1 # vestigia for one system: the command (with the valgrind, QEMU, 2 # plugin, and addr2line it runs baked in where they exist), the QEMU 3 # plugin, the harness-side headers, and the functions that run a 4 # harness under either instrument as a derivation. 5 # 6 # The flake applies it per system; a consumer pinning vestigia (as 7 # synthesis does) imports it with its own package set, so a trace is 8 # built by the same definitions wherever it is built. 9 { pkgs, src ? ../. }: 10 11 let 12 lib = pkgs.lib; 13 14 hpkgs = pkgs.haskell.packages.ghc910.extend (new: old: { 15 vestigia = new.callCabal2nix "vestigia" src { }; 16 }); 17 18 # memcheck runs on Linux only; elsewhere the command can still 19 # read a run's XML. It reports an integer division's undefined 20 # operands (memcheck-operand.patch) 21 linux = pkgs.stdenv.hostPlatform.isLinux; 22 valgrind = pkgs.valgrind.overrideAttrs (o: { 23 patches = (o.patches or [ ]) ++ [ ./memcheck-operand.patch ]; 24 }); 25 26 # the QEMU plugin recording a run's leakage trace per 27 # instruction, and the QEMU that runs a harness under it, for 28 # either ISA, whatever the host's: user mode alone, its guest's 29 # getrandom drawn from the generator -seed fixes 30 # (qemu-getrandom.patch), and an Arm CPU without the cryptographic 31 # extension to be had (crypto=off, qemu-crypto.patch) 32 qemu = (pkgs.qemu.override { 33 userOnly = true; 34 hostCpuTargets = [ "x86_64-linux-user" "aarch64-linux-user" ]; 35 }).overrideAttrs (o: { 36 patches = (o.patches or [ ]) ++ [ 37 ./qemu-getrandom.patch 38 ./qemu-crypto.patch 39 ]; 40 }); 41 plugin = pkgs.runCommandCC "vestigia-qemu-plugin" { 42 nativeBuildInputs = [ pkgs.pkg-config ]; 43 buildInputs = [ pkgs.glib ]; 44 } '' 45 mkdir -p $out/lib 46 cc -O2 -shared -fPIC -Wall -Werror \ 47 $(pkg-config --cflags glib-2.0) -I${qemu}/include \ 48 -o $out/lib/libvestigia-qemu.so ${src}/plugin/vestigia-qemu.c 49 ''; 50 # the harness-side header; a harness build also needs 51 # valgrind's own (valgrindDev) 52 include = pkgs.runCommand "vestigia-include" { } '' 53 mkdir -p $out/include 54 cp ${src}/include/vestigia.h $out/include/vestigia.h 55 cp ${src}/include/vestigia.c $out/include/vestigia.c 56 ''; 57 58 # the command, with the valgrind it was built against baked in, 59 # and LLVM's addr2line, which reads either ISA's objects and names 60 # inlined frames by their own functions (Vestigia.Symbol) 61 vestigia = pkgs.runCommand "vestigia" { 62 nativeBuildInputs = [ pkgs.makeWrapper ]; 63 } '' 64 mkdir -p $out/bin 65 makeWrapper ${hpkgs.vestigia}/bin/vestigia $out/bin/vestigia \ 66 ${lib.optionalString linux (lib.concatStringsSep " " [ 67 "--set-default VESTIGIA_VALGRIND ${valgrind}/bin/valgrind" 68 "--set-default VESTIGIA_QEMU_X86_64 ${qemu}/bin/qemu-x86_64" 69 "--set-default VESTIGIA_QEMU_AARCH64 ${qemu}/bin/qemu-aarch64" 70 "--set-default VESTIGIA_PLUGIN" 71 "${plugin}/lib/libvestigia-qemu.so" 72 "--set-default VESTIGIA_ADDR2LINE" 73 "${pkgs.llvm}/bin/llvm-addr2line" 74 "--set-default VESTIGIA_OBJDUMP" 75 "${pkgs.llvm}/bin/llvm-objdump" 76 ])} 77 ln -s ${include}/include $out/include 78 ''; 79 80 # runs of one harness under memcheck, as a derivation: each run 81 # kept (run-K: memcheck's XML, the objects its harness reported, 82 # its exit status, its own report), what each printed, and the 83 # report over all of them. `runs` is a list of argument lists, the 84 # secrets of the trace; memcheck sees only the path a run takes, so 85 # each run adds the sites on its own. `objects` keeps sites in 86 # objects whose path contains one of them. A harness that fails 87 # still leaves a report of what ran; a run vestigia could not read 88 # fails the build. 89 traceOf = { name, harness, runs, objects ? [ ] }: 90 pkgs.runCommand "vestigia-trace-${name}" { } '' 91 mkdir -p $out 92 start=$(date +%s%N) 93 ${lib.concatImapStrings (k: args: '' 94 set +e 95 ${vestigia}/bin/vestigia run --dir $out/run-${toString k} \ 96 --out $out/run-${toString k}/trace.json \ 97 -- ${harness} ${lib.escapeShellArgs args} \ 98 > $out/stdout-${toString k} 2> $out/stderr-${toString k} 99 echo $? > $out/status-${toString k} 100 set -e 101 '') runs} 102 ${vestigia}/bin/vestigia read --out $out/trace.json \ 103 ${lib.concatMapStrings (o: "--object ${lib.escapeShellArg o} ") 104 objects}${lib.concatImapStrings (k: _: 105 "$out/run-${toString k} ") runs} 2> $out/summary || { 106 cat $out/summary >&2 107 exit 1 108 } 109 echo $(( ($(date +%s%N) - start) / 1000000 )) > $out/milliseconds 110 ''; 111 112 # runs of one harness that differ only in a secret, each 113 # recorded under QEMU, and where they diverge: the dumps, and 114 # the report. `runs` is a list of argument lists; `objects` 115 # keeps origins in objects whose path contains one of them. The 116 # first run is repeated as a control, so that what differs 117 # without the secret is set aside rather than taken for it. 118 # `designed` runs, aimed at particular paths, are compared beside 119 # them for control and coverage but not for addresses (vestigia 120 # diff --designed). Under a `contract` (arm-dit or intel-doitm, the 121 # harness's ISA's), every run also fingerprints the operands of the 122 # instructions outside it in `objects`, listed once (vestigia watch, 123 # kept as `watch`) for every run to read (record --watch). On a 124 # `cpu`, every run is recorded with QEMU emulating that model (its 125 # -cpu, properties and all), so that a harness choosing its code by 126 # the CPU's features runs the code that model leads it to. 127 # A run's own failure leaves its status; a dump vestigia cannot read 128 # fails the build. 129 diffOf = { name, harness, runs, objects ? [ ], designed ? [ ] 130 , contract ? null, cpu ? null }: 131 let 132 model = lib.optionalString (cpu != null) 133 "--cpu ${lib.escapeShellArg cpu} "; 134 watch = lib.optionalString (contract != null) 135 "--contract ${lib.escapeShellArg contract} --watch $out/watch "; 136 in 137 pkgs.runCommand "vestigia-diff-${name}" { } '' 138 mkdir -p $out 139 start=$(date +%s%N) 140 ${lib.optionalString (contract != null) '' 141 ${vestigia}/bin/vestigia watch --out $out/watch ${model}\ 142 --contract ${lib.escapeShellArg contract} \ 143 ${lib.concatMapStrings (o: "--object ${lib.escapeShellArg o} ") 144 objects}-- ${harness} \ 145 ${lib.escapeShellArgs (builtins.head runs)} 146 ''} 147 ${lib.concatImapStrings (k: args: '' 148 set +e 149 ${vestigia}/bin/vestigia record --dump $out/dump-${toString k} \ 150 ${model}${watch}-- ${harness} ${lib.escapeShellArgs args} \ 151 > $out/stdout-${toString k} 2> $out/stderr-${toString k} 152 echo $? > $out/status-${toString k} 153 set -e 154 '') runs}${lib.concatImapStrings (k: args: '' 155 set +e 156 ${vestigia}/bin/vestigia record \ 157 --dump $out/designed-${toString k} \ 158 ${model}${watch}-- ${harness} ${lib.escapeShellArgs args} \ 159 > $out/stdout-designed-${toString k} \ 160 2> $out/stderr-designed-${toString k} 161 echo $? > $out/status-designed-${toString k} 162 set -e 163 '') designed} 164 set +e 165 ${vestigia}/bin/vestigia record --dump $out/control-1 \ 166 ${model}${watch}-- ${harness} \ 167 ${lib.escapeShellArgs (builtins.head runs)} \ 168 > $out/stdout-control-1 2> $out/stderr-control-1 169 echo $? > $out/status-control-1 170 set -e 171 ${vestigia}/bin/vestigia diff --out $out/diff.json \ 172 ${lib.concatMapStrings (o: "--object ${lib.escapeShellArg o} ") 173 objects}${lib.concatImapStrings (k: _: 174 "--designed $out/designed-${toString k} ") designed} \ 175 --control $out/control-1 \ 176 ${lib.concatImapStrings (k: _: "$out/dump-${toString k} ") 177 runs}2> $out/summary 178 echo $(( ($(date +%s%N) - start) / 1000000 )) > $out/milliseconds 179 ''; 180 # the version the cabal file declares, which the command reports 181 version = builtins.head (builtins.match ".*\nversion: *([0-9.]+).*" 182 (builtins.readFile (src + "/vestigia.cabal"))); 183 in 184 { 185 inherit hpkgs vestigia plugin include traceOf diffOf version; 186 valgrindDev = valgrind.dev; 187 }