DF-5695 / verdict.json
{ "finding_id": "DF-5695", "status": "reproduced", "verdict": "karc4random/karc4random64/karc4random_buf (sys/libkern/arc4random.c:101-162) mutate the per-CPU RC4 state with no serialization; the #if 0d crit_enter at arc4random.c:147-150 rests on the premise no one calls in ISR/ithread, which is false for LWKT thread preemption (lwkt_thread.c:941): syscall-context callers (kern_exec.c:1173, vm_map.c:4408, pf.c:6131, in_pcb.c:885) coexist on the same CPU with netisr/TCP-thread callers (pf.c:4459 via ip_input.c:393, tcp_syncache.c:1070, in_pcb.c:414). A deterministic sub-step interleave harness running the exact arc4_randbyte state machine shows 49.4% of the time-ordered output bytes cannot be produced by ANY serialized execution (chimera values from mixed pre/post-preemption state); cross-consumer word duplication was explicitly tested and does not occur (0/1000 trials). Memory-safe (uint8_t indices), no demonstrated prediction or leak - the defect is the broken serialization invariant of an exported CSPRNG feeding ISNs, PF scrub keys, wg/curve25519 key material. Severity Low.", "reproduced": true, "impact": "none", "confidence": "likely", "exploit_chain": "", "evidence": "findings/poc/DF-5695/run.log: divergent_from_serialized=3946 (49.4%) and cross_consumer_duplicate_words=0 over 1000 trials (plus 200/500-trial runs). README.md/VERDICT.md carry the reachability analysis with path:line citations.", "kernel_refs": [ "sys/libkern/arc4random.c:147-150", "sys/libkern/arc4random.c:87-99", "sys/libkern/arc4random.c:141-162", "sys/kern/lwkt_thread.c:941", "sys/kern/kern_exec.c:1173", "sys/net/pf/pf.c:4459", "sys/netinet/tcp_syncache.c:1070" ], "poc_changes": "No seed pack; the race mode was authored into the same exact-source harness as DF-5694: arc4_randbyte decomposed into its 5 memory-visible sub-steps, victim preempted at all 20 legal boundaries of one karc4random(), preemptor runs complete calls, outputs compared against the serialized reference and scanned for cross-consumer duplication.", "attempts": 3, "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": 120, "guest_dirty": 0, "build_cmd": "cc -O2 -Wall -o arc4_harness arc4_harness.c -lm", "run_cmd": "./arc4_harness race 1000", "code_hash": "aa5d1abc01a315513d0a8c0b67d8d6e22703b956c5064f1d7b3a92e21c1462d7", "notes": "Honest scope: algorithm-level reproduction on the verbatim source + call-graph reachability in the deployed kernel; an in-vivo interleaved capture is not externally observable (chimera values are functions of secret state), which is precisely why the invariant-break harness is the correct evidence class. Guest reset (with-src) after runs.", "recommended_fix": "Wrap the state-machine use in all three entry points in crit_enter()/crit_exit() (un-#if-0 the existing pair at arc4random.c:147-161, add the pair to karc4random/karc4random64); see fix.diff.", "fix_status": "fixed", "fix_baseline_reproduced": 1, "fix_patched_reproduced": 0, "fix_verdict": "fix.diff restores serialization via LWKT critical sections in all three entry points; under crit_enter the execution is by construction equivalent to a serialized one, eliminating the demonstrated invariant break. Applies clean via git apply --check. Kernel rebuild not performed (Low severity, non-memory-corruption); guarded region cannot sleep (read_random CSPRNG_UNLIMITED path is spinlock-only, subr_csprng.c:146).", "fix_evidence": "fix.diff (unified, git-apply-able); harness race-mode output in run.log demonstrating the baseline invariant break the fix removes." } |