⬢ DragonFlyBSD Kernel Audit
DF-5090 / proof.sh
← back to finding ↓ download raw 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
#!/bin/sh
# DF-5090 static-verification proof: sys/dev/netif/mii_layer/ruephy.c is DEAD CODE.
#
# Claim: the ruephy(4) MII driver can never attach on any DragonFly system built
# from this tree, because its probe() only accepts children of a NIC driver
# named "rue", and no driver/devclass/module/config-entry named "rue" exists
# anywhere in sys/.  Therefore the latent DF-4930/DF-5001 empty-media panic
# branch, the DF-1973/DF-5009 service KASSERT, and the unguarded ifm_cur
# deref in ruephy_status() are all unreachable.
#
# Run from the repo root:  sh findings/poc/DF-5090/proof.sh
# Exits 0 with PROOF OK if every invariant holds.
set -e
cd "$(dirname "$0")/../../.."   # repo root

fail() { echo "PROOF FAILED: $1" >&2; exit 1; }

echo "== A. no driver_t / DRIVER_MODULE / devclass registers the name 'rue' =="
# any driver_t struct whose registered name is exactly "rue", any DRIVER_MODULE(rue,...)
A1=$(grep -rn 'DRIVER_MODULE(rue,' sys/ | wc -l)
A2=$(grep -rn '"rue"' sys/ --include=*.c --include=*.h)
echo "$A2"
[ "$A1" -eq 0 ] || fail "DRIVER_MODULE(rue,...) exists"
# the ONLY '"rue"' string literals in the whole tree are the two ruephy.c
# probe gates themselves (mii_layer copy line 96, u4b orphan line 101):
echo "$A2" | grep -q 'sys/dev/netif/mii_layer/ruephy.c:96:' || fail "mii gate line moved"
echo "$A2" | grep -q 'sys/bus/u4b/net/ruephy.c:101:' || fail "u4b gate line moved"
[ "$(echo "$A2" | wc -l)" -eq 2 ] || fail "extra 'rue' literals appeared in tree"

echo "== B. no 'device rue' in any kernel config / platform =="
B=$(grep -rn 'device[[:space:]]*rue$' sys/config/ sys/platform/ 2>/dev/null | wc -l)
[ "$B" -eq 0 ] || fail "a config enables device rue"

echo "== C. no if_rue / rue module source exists anywhere =="
C=$(find sys -iname 'if_rue*' -o -iname 'rue.c' | wc -l)
[ "$C" -eq 0 ] || fail "rue NIC driver source exists"

echo "== D. the u4b copy of ruephy.c is an orphan (never compiled) =="
D=$(grep -rn 'u4b/net/ruephy' sys/conf/ sys/bus/u4b/Makefile sys/bus/u4b/*/Makefile 2>/dev/null | wc -l)
[ "$D" -eq 0 ] || fail "u4b orphan is referenced by a build file"

echo "== E. the mii_layer copy IS compiled into miibus =="
grep -q 'dev/netif/mii_layer/ruephy.c[[:space:]]*optional miibus' sys/conf/files \
    || fail "mii_layer ruephy no longer in conf/files (re-check reachability!)"

echo "== F. latent family patterns present in the audited file =="
sed -n '141,145p' sys/dev/netif/mii_layer/ruephy.c
sed -n '161,162p' sys/dev/netif/mii_layer/ruephy.c
sed -n '282p'      sys/dev/netif/mii_layer/ruephy.c

echo "== G. KASSERT gating: DragonFly stock configs DO enable INVARIANTS =="
sed -n '116,118p' sys/sys/systm.h
for CFG in sys/config/X86_64_GENERIC sys/config/LINT64 sys/config/VKERNEL64; do
    printf '%s: INVARIANTS count=%s\n' "$CFG" "$(grep -c INVARIANTS $CFG || true)"
done   # X86_64_GENERIC:56 enables INVARIANTS => KASSERT at ruephy.c:161 is LIVE
       # on stock kernels; it is defused only by unreachability (probe gate :96)

echo
echo "PROOF OK: probe gate (ruephy.c:96) can never pass => attach/service/status/reset"
echo "are unreachable on every kernel buildable from this tree."