probe.nix (6325B)
1 # The probe check: etc/probe/harness.c under both instruments, each 2 # site and origin it should show found where it should be, and 3 # nothing else in the harness. On an x86_64 host, the same harness 4 # built for aarch64 is traced differentially too, under QEMU; memcheck 5 # needs a native host. Each differential trace is repeated under its 6 # ISA's data-independent-timing contract, which finds the floating- 7 # point division outside it and changes no origin. 8 { pkgs, vestigia }: 9 10 let 11 lib = pkgs.lib; 12 13 # the harness, built by a package set's C compiler and linked at a 14 # fixed address, where an instruction's address in the file is not 15 # its offset there 16 probeOf = ps: ps.runCommandCC "vestigia-probe" { 17 hardeningDisable = [ "fortify" ]; 18 } '' 19 mkdir -p $out/bin 20 $CC -O0 -g -fno-pie -no-pie -I${vestigia.include}/include \ 21 -I${vestigia.valgrindDev}/include \ 22 -o $out/bin/probe ${../etc/probe/harness.c} \ 23 ${vestigia.include}/include/vestigia.c 24 $READELF -h $out/bin/probe | grep -q 'Type: *EXEC' 25 ''; 26 27 probe = probeOf pkgs; 28 cross = probeOf pkgs.pkgsCross.aarch64-multiplatform; 29 x86_64 = pkgs.stdenv.hostPlatform.isx86_64; 30 31 threads = pkgs.runCommandCC "vestigia-probe-threads" { } '' 32 mkdir -p $out/bin 33 cc -O0 -pthread -o $out/bin/threads ${../etc/probe/threads.c} 34 ''; 35 36 secrets = [ "00000005" "0000003a" "000000c3" ]; 37 objects = [ "/bin/probe" ]; 38 39 trace = vestigia.traceOf { 40 name = "probe"; 41 harness = "${probe}/bin/probe"; 42 runs = map (s: [ s ]) secrets; 43 inherit objects; 44 }; 45 46 diffOf = name: harness: contract: vestigia.diffOf { 47 inherit name objects contract; 48 harness = "${harness}/bin/probe"; 49 runs = map (s: [ s ]) secrets; 50 }; 51 native = if x86_64 then "intel-doitm" else "arm-dit"; 52 diff = diffOf "probe" probe null; 53 diffCross = diffOf "probe-aarch64" cross null; 54 diffContract = diffOf "probe-contract" probe native; 55 diffCrossContract = diffOf "probe-aarch64-contract" cross "arm-dit"; 56 57 # each report's (class, function) pairs in the harness, sorted 58 expected = { 59 trace = [ [ "address" "lookup" ] [ "address" "rare" ] 60 [ "control" "branchy" ] [ "control" "calls" ] 61 [ "control" "rare" ] [ "operand" "divide" ] 62 [ "operand" "divide_memory" ] ]; 63 diff = [ [ "address" "lookup" ] [ "control" "branchy" ] 64 [ "control" "calls" ] [ "control" "rare" ] 65 [ "operand" "divide" ] [ "operand" "divide_memory" ] ]; 66 }; 67 in 68 pkgs.runCommand "vestigia-probe-check" { 69 nativeBuildInputs = [ pkgs.jq ]; 70 } '' 71 check() { 72 got=$(jq -c "$2" "$1") 73 if [ "$got" != "$3" ]; then 74 echo "probe: $1: expected $3, got $got" >&2 75 exit 1 76 fi 77 } 78 check ${trace}/trace.json \ 79 '[.sites[] | [.class, .function]] | unique' \ 80 '${builtins.toJSON expected.trace}' 81 check ${diff}/diff.json \ 82 '[.origins[] | [.class, .frames[0].function]] | unique' \ 83 '${builtins.toJSON expected.diff}' 84 85 # every secret is traced under taint, and the table index on the 86 # third secret's path is that run's alone 87 check ${trace}/trace.json '[.runs[] | .exit]' '[0,0,0]' 88 check ${trace}/trace.json \ 89 '[.sites[] | select(.function == "rare" and .class == "address") 90 | .runs]' \ 91 '[["run-3"]]' 92 93 # both instruments name each instruction they both saw by one 94 # address: a division memcheck reports where it divides, not at the 95 # memory access before it 96 check ${trace}/trace.json \ 97 '[.sites[] | select(.class == "operand") | .offset] | sort' \ 98 "$(jq -c '[.origins[] | select(.class == "operand") | .offset] 99 | sort' ${diff}/diff.json)" 100 ${lib.optionalString x86_64 '' 101 check ${diffCross}/diff.json \ 102 '[.origins[] | [.class, .frames[0].function]] | unique' \ 103 '${builtins.toJSON expected.diff}' 104 ''} 105 106 # under a contract, the floating-point division is outside it, and 107 # the origins are those found without one 108 for d in ${diffContract} ${lib.optionalString x86_64 109 "${diffCrossContract}"}; do 110 check $d/diff.json '[.outside[] | .frames[0].function] | unique' \ 111 '["fpdivide"]' 112 check $d/diff.json \ 113 '[.origins[] | [.class, .frames[0].function]] | unique' \ 114 '${builtins.toJSON expected.diff}' 115 check $d/diff.json '.summary.watched > 0' 'true' 116 check $d/diff.json '[.outside[] | .instruction | type] | unique' \ 117 '["string"]' 118 done 119 check ${diffContract}/diff.json '[.contract.name, .isa]' \ 120 '${builtins.toJSON [ native (if x86_64 then "x86_64" else "aarch64") ]}' 121 check ${diff}/diff.json '.contract' 'null' 122 ${lib.optionalString x86_64 '' 123 check ${diffCrossContract}/diff.json '[.contract.name, .isa]' \ 124 '["arm-dit","aarch64"]' 125 ''} 126 127 # each origin's stack runs from its own function to the call in 128 # main that reached it 129 for d in ${diff} ${lib.optionalString x86_64 "${diffCross}"}; do 130 check $d/diff.json \ 131 '[.origins[] | [.stacks[0][0].function, .stacks[0][1].function] 132 | .[1]] | unique' \ 133 '["main"]' 134 done 135 136 # each run as it was made: the declared, then the control 137 check ${diff}/diff.json \ 138 '[.runs[] | [.kind, .arguments[1], .status]]' \ 139 '${builtins.toJSON (map (s: [ "declared" s 0 ]) secrets 140 ++ [ [ "control" (builtins.head secrets) 0 ] ])}' 141 142 v=${vestigia.vestigia}/bin/vestigia 143 144 # a control must repeat the run it controls, and every run must lay 145 # out as the first: its arguments of one number and length 146 $v record --dump a -- ${probe}/bin/probe 00000005 147 $v record --dump b -- ${probe}/bin/probe 0000003a 148 $v record --dump c -- ${probe}/bin/probe 000000003a 149 if $v diff --control b a a 2> refusal; then 150 echo "probe: a control repeating another secret was taken" >&2 151 exit 1 152 fi 153 grep -q 'does not repeat' refusal 154 if $v diff a c 2> refusal; then 155 echo "probe: a run with a longer argument was compared" >&2 156 exit 1 157 fi 158 grep -q 'number or length' refusal 159 160 # a guest that starts a second thread is stopped, and its dump 161 # refused 162 if $v record --dump threads -- ${threads}/bin/threads; then 163 echo "probe: a guest's second thread was recorded" >&2 164 exit 1 165 fi 166 if $v diff threads threads 2> refusal; then 167 echo "probe: a stopped guest's dump was compared" >&2 168 exit 1 169 fi 170 grep -q 'second thread' refusal 171 touch $out 172 ''