⬢ DragonFlyBSD Kernel Audit
DF-5090 / proof.log
← back to finding ↓ download raw
== A. no driver_t / DRIVER_MODULE / devclass registers the name 'rue' ==
sys/bus/u4b/net/ruephy.c:101:	    "rue") == 0)
sys/dev/netif/mii_layer/ruephy.c:96:	if (strcmp(device_get_name(parent), "rue") != 0)
== B. no 'device rue' in any kernel config / platform ==
== C. no if_rue / rue module source exists anywhere ==
== D. the u4b copy of ruephy.c is an orphan (never compiled) ==
== E. the mii_layer copy IS compiled into miibus ==
== F. latent family patterns present in the audited file ==
	if ((sc->mii_capabilities & BMSR_MEDIAMASK) == 0)
		kprintf("no media present");
	else
		mii_phy_add_media(sc);
	kprintf("\n");
	KASSERT(IFM_INST(ife->ifm_media) == sc->mii_inst,
		("ruephy_service: can't isolate RealTek RTL8150 PHY"));
		mii->mii_media_active = mii->mii_media.ifm_cur->ifm_media;
== G. KASSERT gating: DragonFly stock configs DO enable INVARIANTS ==
#else
#define	KASSERT(exp,msg)		do { } while (0)
#define	KKASSERT(exp)			do { } while (0)
sys/config/X86_64_GENERIC: INVARIANTS count=1
sys/config/LINT64: INVARIANTS count=3
sys/config/VKERNEL64: INVARIANTS count=1

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