DF-5714 / verdict.json
{ "finding_id": "DF-5714", "status": "reproduced", "verdict": "sys/libkern/ffs.c is dead code: absent from sys/conf/files (libkern block 2195-2237), superseded on the only supported arch by the cpufunc.h:266-273 static __inline ffs (__builtin_ffs, HAVE_INLINE_FFS), and empirically non-compilable in-kernel because ffs.c:33 #include <string.h> cannot resolve under -nostdinc (kern.pre.mk:61) \u2014 fatal error recorded in dead_compile.log. The latent body was proven arithmetically correct on the full input space: 0 mismatches vs __builtin_ffs over all 4,294,967,296 masks (T1), clearing the mask==0 return, negative/INT_MIN inputs, and the implementation-defined signed right shift at ffs.c:46; ffsl.c twin 0/50,002,088 (T2). Consumer census (102 live call sites): all use the inline, no 64-bit truncation misuse, no memory operands (guard-page class vacuous). Impact none (nothing links the file); Info hygiene finding, same class as DF-5700 (bcmp.c).", "reproduced": true, "impact": "none", "confidence": "certain", "exploit_chain": "", "evidence": "build.log lines DEADPROOF-OK: ffs.c cannot compile in-kernel + dead_compile.log (fatal error: string.h); run.log T1 ffs full-domain: 4294967296 cases, 0 mismatches and T2 ffsl: 50002088 cases, 0 mismatches; FIXCOMPILE-NAIVE-FAILS (fix_compile.log, cpufunc.h inline collision) and FIX2COMPILE-OK (fix2_compile.log) validating fix.diff; env.txt pins guest cksums == audit tree (ffs.c 3349697062 1930).", "kernel_refs": [ "sys/libkern/ffs.c:33", "sys/libkern/ffs.c:43-47", "sys/cpu/x86_64/include/cpufunc.h:266-273", "sys/conf/files:2195-2237", "sys/conf/kern.pre.mk:61" ], "poc_changes": "Seed had no PoC (pass-1 filed nothing). Rig authored per the DF-5712/neg-evidence-strtoul pattern. Iterations kept in-pack: (1) ffsl.c needed its kernel-only #include <sys/libkern.h> stripped like strcmp.c (userland stub #errors); (2) guest sh lacks process substitution \u2014 replaced diff <() with cmp on temp files; (3) run.1.log: guard-page fault cases reused G2s page contents, fixed by re-arming the page to all-K; (4) run.2.log: libc control calls were DCEd ((void)strcmp with unused result), fixed by consuming the result; final run.log HARNESS-PASS.", "attempts": 5, "guest_uname": "DragonFly dfbsd 6.5-DEVELOPMENT DragonFly 6.5-DEVELOPMENT #0: Thu Jul 2 06:02:54 UTC 2026 root@dfbsd:/usr/obj/usr/src/sys/X86_64_GENERIC x86_64", "runtime_sec": 26, "guest_dirty": 0, "build_cmd": "sh /tmp/df5714/build.sh (guest root; verbatim -D-renamed compiles of ffs.c/ffsl.c/strcmp.c + deadproof + fix validation)", "run_cmd": "sh /tmp/df5714/run.sh (guest root; ./p2_harness ~26 s: T1 full 2^32 sweep, T2, T3, T4 guard-page, T5)", "code_hash": "9bcea641f96ecaf97f8c6a30bbfec92b9f5bcb37911cd55b66b6e44e90c3913b", "notes": "Decisive run 26 s; builds + all runs total ~4 min on the guest. Guest left clean (only /tmp/df5714 scratch; no kernel state, modules, or sysctls touched; no panic \u2014 no reset needed). ffsll does not exist anywhere in the kernel (zero definitions/callers). The same harness carries the strcmp.c negative evidence (T3: 201,114,116 cases, 0 sign and 0 exact mismatches vs guest libc; T4: guard-page parity kernel-vs-libc in all five edge cases) \u2014 mirrored in findings/poc/neg-evidence-strcmp-pass2/.", "recommended_fix": "Adopt fix.diff (include swap to <sys/libkern.h> + #if !defined(HAVE_INLINE_FFS) gate), or simply delete sys/libkern/ffs.c (and the equally dead ffsl.c) \u2014 they are unreferenced by conf/files and cannot compile as committed.", "fix_status": "fixed", "fix_baseline_reproduced": 1, "fix_patched_reproduced": 1, "fix_verdict": "Validation is at the compile level, which is exactly the level where the defect manifests (the file is linked nowhere, so there is no runtime behavior to A/B and no kernel rebuild to do). Baseline reproduced: unpatched ffs.c fails kernel-style compile (DEADPROOF-OK, dead_compile.log: fatal error: string.h: No such file or directory). Naive include-swap fix reproduced as INSUFFICIENT (fix_compile.log: cpufunc.h:269 static __inline ffs collides with the out-of-line definition). Final fix.diff validated: patched file compiles kernel-style with the body correctly gated away on x86_64 (FIX2COMPILE-OK, fix2_compile.log; guest-built f_ffs2.c byte-identical to the diff result, verified by cmp).", "fix_evidence": "build.log sections == dead-file proof / == fix.diff validation; dead_compile.log; fix_compile.log; fix2_compile.log; f_ffs2.c; fix.diff" } |