⬢ DragonFlyBSD Kernel Audit
DF-5714 / manifest.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
{
  "finding": "DF-5714",
  "title": "sys/libkern/ffs.c is dead code (absent from conf/files, non-compilable in-kernel via #include <string.h>); latent body machine-proven correct over the full 2^32 domain",
  "verdict": "reproduced",
  "impact": "none",
  "reproduce": {
    "build": "sh /tmp/df5714/build.sh  (DragonFly guest, root; sources cksum-pinned to the audit tree)",
    "run": "sh /tmp/df5714/run.sh",
    "expected": [
      "DEADPROOF-OK: ffs.c cannot compile in-kernel (fatal error: string.h: No such file or directory)",
      "FIXCOMPILE-NAIVE-FAILS (cpufunc.h:269 static __inline ffs collision)",
      "FIX2COMPILE-OK: guarded ffs.c compiles kernel-style",
      "T1 ffs full-domain: 4294967296 cases, 0 mismatches (vs __builtin_ffs == live cpufunc.h inline)",
      "T2 ffsl: 50002088 cases, 0 mismatches",
      "HARNESS-PASS"
    ]
  },
  "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"
  ],
  "artifacts": [
    "README.md", "VERDICT.md", "verdict.json", "manifest.json",
    "p2_harness.c", "p2_harness_v1.c",
    "build.sh", "run.sh",
    "build.log", "run.log", "run.1.log", "run.2.log",
    "dead_compile.log", "fix_compile.log", "fix2_compile.log",
    "f_ffs2.c", "fix.diff", "env.txt"
  ]
}