โฌข DragonFlyBSD Kernel Audit
DF-1061 / verify.sh
โ† back to finding โ†“ download raw
#!/bin/sh
# DF-1061 โ€” pmap_inval LOOPRECOVER watchdog silent TLB-invalidation abandonment
# Static source verification (runtime trigger needs host-induced vCPU stall > 2s).
#
# Confirms (per the finding's static-verification fallback, finding markdown lines
# 124-132) that:
#   (1) CPUMASK_ASSZERO(info->done) is the force-clear in both "A" and "B" paths
#   (2) info->failed is written but never read (dead) โ€” no caller can detect abandonment
#   (3) the target clears its done bit only AFTER cpu_invlpg() (so a still-set bit means
#       the invalidation has NOT happened on that cpu)
#   (4) the sibling "C" path does NOT abandon โ€” it re-broadcasts the IPI
#
# Run from the repo root (sys/ must be present).

set -e
F=sys/platform/pc64/x86_64/pmap_inval.c

echo "=== (1) force-clear in 'A' (pmap_inval_smp) and 'B' (pmap_inval_smp_cmpset) ==="
grep -nE "CPUMASK_ASSZERO\(info->done\)|loopdebug\(\"[AB]\"|XXX recover" "$F"

echo
echo "=== (2) info->failed: writers only, no readers ==="
echo "writers (5 expected):"
grep -n "info->failed" "$F"
echo "readers (any non-assignment use, expect 0):"
grep -nE "info->failed[^[:space:]]*=|if.*info->failed|return.*info->failed| [!]?info->failed" "$F" | grep -v "info->failed[[:space:]]*=" || echo "  (none โ€” confirmed dead)"

echo
echo "=== (3) target clears done AFTER cpu_invlpg (pmap_inval_intr) ==="
sed -n '750,775p' "$F" | grep -nE "cpu_invlpg|info->done|npgs"

echo
echo "=== (4) sibling 'C' path re-broadcasts (does NOT abandon) ==="
sed -n '780,800p' "$F" | grep -nE "loopdebug\(\"C\"|ATOMIC_CPUMASK_NANDMASK|smp_invlpg|recover"

echo
echo "=== (5) LOOPRECOVER is unconditionally #define-d (not a kernel option) ==="
grep -nE "^#define LOOPRECOVER\b|LOOPRECOVER_TIMEOUT1|LOOPRECOVER_TIMEOUT2" "$F"

echo
echo "=== (6) Xinvltlb fires at interrupt level (mp_machdep.c) โ€” cannot be held off ==="
sed -n '1160,1175p' sys/platform/pc64/apic/mpapic.c 2>/dev/null || true
grep -nE "Xinvltlb|INTRTYPE" sys/platform/pc64/x86_64/mp_machdep.c 2>/dev/null | head -5 || true

echo
echo "DONE: all six static checks executed."