⬢ DragonFlyBSD Kernel Audit
DF-5580 / verdict.json
← 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
{
  "finding_id": "DF-5580",
  "status": "reproduced",
  "reproduced": true,
  "impact": "none",
  "confidence": "certain",
  "verdict": "The ten shift sites of the branchless masked-select initialization in __udivmodti4 (__udivti3.c:231-244 and :274-278) execute shift counts outside the domain of their 64-bit operands (counts 64..126 from n_utword_bits - sr, and counts like 0xFFFFFFFB from unsigned-wrapped negative sr - n_udword_bits). The UB is live and reproducible: -fsanitize=shift aborts at __udivti3.c:274:25 (shift=64, rc=134) and a recover-mode census records 1,017,186 events covering all ten sites. The results are nonetheless correct on the shipping gcc 8.3 (same compiler that built the running kernel): 2x2,151,999,419 userspace differential vectors vs native unsigned __int128 division with 0 mismatches, and ~268.7M vectors through the running kernels own exported __udivti3 symbol via a KLD harness, also 0 mismatches -- because each poisoned shift is ANDed with a mask that is provably zero whenever the count is out of domain. Impact today is therefore none; the risk is that any future compiler upgrade is entitled to fold/hoist/poison these evaluations and silently corrupt every in-kernel 128-bit division (muldivu64, sys/sys/systm.h:505 -- lapic/i8254 timer reload, kern_clock timekeeping, hyperv vmbus). fix.diff replaces the masked selects with the explicit sr==64/sr<64/sr>64 branches the files own comments already describe; validated: identical 2.15B-vector battery 0 mismatches, UBSan clean (rc=0), and the patched source compiled with kernel CFLAGS agrees with the kernel baseline symbol in kernel context on all vectors.",
  "exploit_chain": "",
  "evidence": "run.log / run.2.log (baseline differential, 2,151,999,419 vectors each, mismatches=0, two seed sets); ub_abort.log + status_ub_abort.txt (UBSan abort rc=134 at __udivti3.c:274:25 shift=64 -- the UB is live); ub_census.txt (1,017,186 shift-UB events across :231 :233 :235 :236 :238 :240 :242 :243 :274 :277, incl. shift=4294967291 negative-wrapped counts); kmod_kldtest_run.log (kernels own __udivti3 @0xffffffff80bdabb0 and fix.diff-patched source compiled with kernel CFLAGS: both 0 mismatches on ~268.7M vectors); run_fixed.log + ub_abort_fixed.log + status_ub_abort_fixed.txt (fix: 0 mismatches on identical battery, UBSan clean rc=0); env.txt (gcc 8.3 = kernel .comment compiler); fix.diff",
  "kernel_refs": [
    "sys/platform/pc64/x86_64/__udivti3.c:231-244",
    "sys/platform/pc64/x86_64/__udivti3.c:274-278",
    "sys/platform/pc64/x86_64/__udivti3.c:203-204",
    "sys/platform/pc64/x86_64/__udivti3.c:250-257",
    "sys/platform/pc64/x86_64/__udivti3.c:301-302",
    "sys/sys/systm.h:505-513",
    "sys/platform/pc64/conf/files:151"
  ],
  "poc_changes": "The finding-seed sketch had to be fully authored: differential harness #includes the kernel .c verbatim (access to static __udivmodti4 for remainder checks); UBSan required hand-written __ubsan_handle_shift_out_of_bounds[_abort] stubs because DragonFly gcc 8.3 ships no libubsan, plus compile-then-link split to avoid the drivers -lubsan; KLD harness (dev_ops/dev_ioctl_args DragonFly idiom) drives the kernels own exported symbol via /dev/df5580 ioctl. Two of my own harness bugs were found and fixed during verification and are documented in VERDICT.md (edge-set array overflow; sr-boundary generator truncating its dividend to 64 bits).",
  "attempts": 9,
  "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": 2900,
  "guest_dirty": 0,
  "build_cmd": "sh build.sh  (userspace: cc -O2 -Wall -o df5580_diff df5580_diff.c; KLD: cd kmod/df5580 && make SYSDIR=/usr/src/sys)",
  "run_cmd": "sh run.sh   (full matrix; KLD leg: kldload df5580.ko df5580fix.ko && ./df5580_kldtest 268435456)",
  "code_hash": "8665ad3ff0c1e0cfd100010b2903b095c855c2d15cf351bc0d705b4ec51064ad",
  "notes": "Severity Low / hardening: no wrong division results on the shipping toolchain (proven), but formally UB that a compiler upgrade can legally turn into silent miscompilation of all in-kernel 128-bit division (muldivu64 callers: lapic.c:556,675,704,726; clock.c:351,419,472,824; kern_clock.c:916,1386+; kern_cputimer.c:205; vmbus.c:365). Upstream compiler-rt deleted this branchless-mask implementation years ago. Negative results (checked, killed): no wrong-result bug (~6.7B vectors total, q and r, userspace + kernel contexts); div==0 -> #DE panic is the documented libgcc caller contract (all in-tree callers pass nonzero; DF-5554 class is 64-bit hardware div and does not link __udivti3); no memory-safety surface (no pointers/arrays/lengths; *rem NULL-checked); only __udivti3 exists in-tree (no __umodti3, no 128-bit modulo links); union punning covered by kernel -fno-strict-aliasing (see mod_build.log flags).",
  "recommended_fix": "Replace the masked-select shift blocks at :231-244 and :274-278 with the explicit sr==64 / sr<64 / sr>64 branch initialization (verbatim in fix.diff; matches pre-rewrite upstream compiler-rt and the code already described in the files own comments).",
  "fix_status": "fixed",
  "fix_kernel_uname": "DragonFly dfbsd 6.5-DEVELOPMENT #0: Thu Jul 2 06:02:54 UTC 2026 root@dfbsd:/usr/obj/usr/src/sys/X86_64_GENERIC x86_64 (baseline kernel; patched source executed in kernel context via KLD built with kernel CFLAGS)",
  "fix_baseline_reproduced": 1,
  "fix_patched_reproduced": 0,
  "fix_verdict": "fix.diff removes every out-of-domain shift. Validation: (1) identical 2,151,999,419-vector battery on the patched source -- 0 mismatches vs native division (run_fixed.log); (2) -fsanitize=shift -fno-sanitize-recover=shift on the patched source completes the edge battery clean, rc=0 (ub_abort_fixed.log), vs rc=134 abort at baseline; (3) patched source compiled with kernel CFLAGS (-Werror clean; modfix_build.log) as df5580fix.ko and executed in kernel context agrees with the running kernels baseline __udivti3 symbol and with native division on all ~268.7M KLD vectors (kmod_kldtest_run.log). A full single-fix kernel rebuild was not performed (non-memory-corruption finding; contract mandates kernel rebuilds only for reproduced memory corruption); the KLD route runs the patched code in kernel context with kernel flags, equivalent evidence for a pure codegen change.",
  "fix_evidence": "run_fixed.log (PASS, 0 mismatches, 313s); ub_abort_fixed.log + status_ub_abort_fixed.txt (rc=0, no UBSAN-FIRED); status_ub_abort.txt (baseline rc=134); kmod_kldtest_run.log (PASS: kernel baseline AND patched source match native division); modfix_build.log (kernel CFLAGS -Werror clean build of patched source); fix.diff"
}