code wiki / _hdl_build / nx_sup_kernel_witness.nx
`nx_sup_kernel_witness.nx` source

↩ module page · 311 lines · 13436 B
1// nx_sup_kernel_witness.nx -- SECOND-METHOD-CLASS WITNESS for the SUPERVISOR domain (2026-08-03).
2//
3// WHY: nx_sota_status holds 40 domains at MECH-OK -- 'executed evidence GREEN; awaiting a 2nd
4// independent method class' -- and supervisor is the lowest-coverage of them (347). The recipe is
5// proven twice (videocodec/ffmpeg-psnr, coding/library-refetch): find an EXTERNAL artifact that can
6// DISAGREE with us, run both, sign the row. Here the external authority is the LINUX KERNEL'S OWN
7// BOOK-KEEPING -- the /proc process table and the /proc/net/tcp{,6} LISTEN socket table -- an
8// accounting we did not write and cannot wish into agreement.
9//
10// THE CLAIM UNDER TEST: mgmt_snap.json, the snapshot the supervisor itself writes each poll
11// ('SVC <name> <port> UP <procs> ...'). For every service the supervisor claims UP:
12//   axis 1 (process table): at least one live pid whose cmdline names the service binary
13//   axis 2 (socket table):  when port>0, a LISTEN socket on exactly that port
14// PRESENCE, not process-count equality, is asserted DELIBERATELY: sites.elf preforks workers, so
15// the snapshot's procs=1 and the kernel's 5 pids are DIFFERENT UNITS -- comparing counts would
16// manufacture a false disagreement (do the arithmetic in the unit the criterion is written in).
17//
18// DISCRIMINATION IS PROVEN IN-RUN, never assumed: a fabricated service name and a fabricated port
19// are checked the same way and MUST come back absent; if either 'confirms', the run is INVALID --
20// a witness that cannot refuse cannot confirm.
21//
22// exit 0 = GREEN (every UP claim kernel-confirmed on both axes, negative controls refused)
23//      1 = RED (the kernel DISAGREES with a supervisor claim -- a REAL finding, report it)
24//      2 = snapshot unreadable/empty (cannot witness a claim nobody made)
25//      3 = NEGCTL-INVALID (the instrument cannot refuse -> no verdict, never a pass)
26// license_tier: ORIGINAL   No hw writes (Rule 26).   expect_exit: 0
27import "nx_syscalls.nx"
28const SW_MAGIC_4096: i64 = 4096
29const SW_MAGIC_8192: i64 = 8192
30const SW_MAGIC_32768: i64 = 32768
31
32const SW_SNAPCAP: i64 = 65536
33const SW_TCPCAP: i64 = 1048576
34const SW_CMDCAP: i64 = 4096
35const SW_PIDSCAN: i64 = 131072
36const SW_MAXSVC: i64 = 64
37const SW_NEGPORT: i64 = 39999
38
39static sw_arena: *u8
40static sw_ao: i64
41static sw_name: *i64
42static sw_port: *i64
43static sw_hits: *i64
44static sw_stemhits: *i64
45static sw_nsvc: i64
46static sw_lports: *i64
47static sw_nlp: i64
48static sw_neghits: i64
49
50func sw_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
51func sw_num(v: i64) -> i64 {
  let t: *u8 = sys_mmap(32)
  let o: *u8 = sys_mmap(32)
  var m: i64 = v
  var k: i64 = 0
  if m == 0 { t[0] = 48 as u8; k = 1 }
  while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
  var i: i64 = 0
  while i < k { o[i] = t[k-1-i]; i = i + 1 }
  sys_write(1, o, k)
  return 0
62}
63func sw_len(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n }
64func sw_read(path: *u8, buf: *u8, cap: i64) -> i64 {
  let fd: i64 = sys_openat_rd(path)
  if fd < 0 { return 0 - 1 }
  var tot: i64 = 0
  var go: i64 = 1
  while go == 1 {
      let n: i64 = sys_read(fd, ((buf as i64) + tot) as *u8, cap - tot)
      if n <= 0 { go = 0 } else { tot = tot + n; if tot >= cap { go = 0 } }
  }
  sys_close(fd)
  return tot
75}
76func sw_find(hay: *u8, hn: i64, ned: *u8, nl: i64) -> i64 {
  if nl <= 0 { return 0 - 1 }
  var i: i64 = 0
  while i + nl <= hn {
      var k: i64 = 0
      var m: i64 = 1
      while k < nl { if hay[i+k] != ned[k] { m = 0; k = nl } else { k = k + 1 } }
      if m == 1 { return i }
      i = i + 1
  }
  return 0 - 1
87}
88
89// collect LISTEN (st==0A) local ports from one /proc/net table into sw_lports
90func sw_tcp_scan(path: *u8) -> i64 {
  let b: *u8 = sys_mmap(SW_TCPCAP)
  let n: i64 = sw_read(path, b, SW_TCPCAP - 1)
  if n <= 0 { return 0 }
  var i: i64 = 0
  while i < n {
      var le: i64 = i
      while le < n { if b[le] == (10 as u8) { break } le = le + 1 }
      var p: i64 = i
      var t: i64 = 0
      var lps: i64 = 0 - 1
      var stok: i64 = 0 - 1
      while p < le {
          while p < le { if b[p] != (32 as u8) { break } p = p + 1 }
          if p >= le { break }
          let ts: i64 = p
          while p < le { if b[p] == (32 as u8) { break } p = p + 1 }
          if t == 1 { lps = ts }
          if t == 3 { stok = ts }
          t = t + 1
      }
      if lps >= 0 { if stok >= 0 { if stok + 1 < le {
          if b[stok] == (48 as u8) { if b[stok+1] == (65 as u8) {
              var cp: i64 = lps
              while cp < le { if b[cp] == (58 as u8) { break } cp = cp + 1 }
              if cp < le {
                  var pv: i64 = 0
                  var h: i64 = cp + 1
                  var going: i64 = 1
                  while going == 1 {
                      if h >= le { going = 0 } else {
                          let c: i64 = b[h] as i64
                          var d: i64 = 0 - 1
                          if c >= 48 { if c <= 57 { d = c - 48 } }
                          if c >= 65 { if c <= 70 { d = c - 55 } }
                          if d >= 0 { pv = pv*16 + d; h = h + 1 } else { going = 0 }
                      }
                  }
                  if pv > 0 { if sw_nlp < SW_MAGIC_4096 { sw_lports[sw_nlp] = pv; sw_nlp = sw_nlp + 1 } }
              }
          } }
      } } }
      i = le + 1
  }
  return 0
135}
136
137func main(argc: i64, argv: *i64) -> i64 {
  sw_p("=== nx_sup_kernel_witness -- the supervisor's inventory vs the kernel's own accounting ===\n" as *u8)
  let sb: *u8 = sys_mmap(SW_SNAPCAP)
  let sn: i64 = sw_read("mgmt_snap.json\x00" as *u8, sb, SW_SNAPCAP - 1)
  if sn <= 0 {
      sw_p("SUP-KERNEL-WITNESS ABSENT: cannot read mgmt_snap.json (the supervisor's own claim snapshot)\n" as *u8)
      sys_exit(2); return 2
  }
  sw_arena = sys_mmap(SW_MAGIC_8192)
  sw_ao = 0
  sw_name = sys_mmap(8 * SW_MAXSVC) as *i64
  sw_port = sys_mmap(8 * SW_MAXSVC) as *i64
  sw_hits = sys_mmap(8 * SW_MAXSVC) as *i64
  sw_stemhits = sys_mmap(8 * SW_MAXSVC) as *i64
  sw_nsvc = 0
  var i: i64 = 0
  while i < sn {
      var le: i64 = i
      while le < sn { if sb[le] == (10 as u8) { break } le = le + 1 }
      if le - i > 4 { if sb[i] == (83 as u8) { if sb[i+1] == (86 as u8) { if sb[i+2] == (67 as u8) { if sb[i+3] == (32 as u8) {
          var p: i64 = i + 4
          let ns: i64 = p
          while p < le { if sb[p] == (32 as u8) { break } p = p + 1 }
          let ne: i64 = p
          while p < le { if sb[p] != (32 as u8) { break } p = p + 1 }
          var pv: i64 = 0
          while p < le {
              let c: i64 = sb[p] as i64
              if c >= 48 { if c <= 57 { pv = pv*10 + (c - 48); p = p + 1 } else { break } } else { break }
          }
          while p < le { if sb[p] != (32 as u8) { break } p = p + 1 }
          var isup: i64 = 0
          if p + 2 <= le { if sb[p] == (85 as u8) { if sb[p+1] == (80 as u8) { isup = 1 } } }
          if isup == 1 { if sw_nsvc < SW_MAXSVC { if ne > ns {
              sw_name[sw_nsvc] = sw_ao
              var q: i64 = ns
              while q < ne { sw_arena[sw_ao] = sb[q]; sw_ao = sw_ao + 1; q = q + 1 }
              sw_arena[sw_ao] = 0 as u8
              sw_ao = sw_ao + 1
              sw_port[sw_nsvc] = pv
              sw_hits[sw_nsvc] = 0
              sw_stemhits[sw_nsvc] = 0
              sw_nsvc = sw_nsvc + 1
          } } }
      } } } } }
      i = le + 1
  }
  if sw_nsvc == 0 {
      sw_p("SUP-KERNEL-WITNESS ABSENT: snapshot readable but holds zero SVC-UP rows\n" as *u8)
      sys_exit(2); return 2
  }
  // kernel axis 2 first: the LISTEN table (both address families)
  sw_lports = sys_mmap(8 * SW_MAGIC_4096) as *i64
  sw_nlp = 0
  sw_tcp_scan("/proc/net/tcp\x00" as *u8)
  sw_tcp_scan("/proc/net/tcp6\x00" as *u8)
  // kernel axis 1: ONE pass over the process table, every claimed name + the fabricated one
  let pmb: *u8 = sys_mmap(64)
  var pidmax: i64 = SW_MAGIC_32768
  let pmn: i64 = sw_read("/proc/sys/kernel/pid_max\x00" as *u8, pmb, 63)
  if pmn > 0 {
      var pv2: i64 = 0
      var z: i64 = 0
      while z < pmn { let c: i64 = pmb[z] as i64; if c >= 48 { if c <= 57 { pv2 = pv2*10 + (c - 48) } } z = z + 1 }
      if pv2 > 0 { pidmax = pv2 }
  }
  var scanto: i64 = pidmax
  if scanto > SW_PIDSCAN { scanto = SW_PIDSCAN }
  let path: *u8 = sys_mmap(64)
  let cmd: *u8 = sys_mmap(SW_CMDCAP)
  let tt: *u8 = sys_mmap(32)
  let neg: *u8 = "nx_zz_negctl_witness.elf" as *u8
  sw_neghits = 0
  var pid: i64 = 2
  while pid <= scanto {
      var o: i64 = 0
      let pre: *u8 = "/proc/"
      var k: i64 = 0
      while pre[k] != (0 as u8) { path[o] = pre[k]; o = o + 1; k = k + 1 }
      var m: i64 = pid
      var kk: i64 = 0
      while m > 0 { tt[kk] = (48 + (m % 10)) as u8; m = m / 10; kk = kk + 1 }
      var z2: i64 = kk - 1
      while z2 >= 0 { path[o] = tt[z2]; o = o + 1; z2 = z2 - 1 }
      let suf: *u8 = "/cmdline"
      k = 0
      while suf[k] != (0 as u8) { path[o] = suf[k]; o = o + 1; k = k + 1 }
      path[o] = 0 as u8
      let cn: i64 = sw_read(path, cmd, SW_CMDCAP - 1)
      if cn > 0 {
          var y: i64 = 0
          while y < cn { if cmd[y] == (0 as u8) { cmd[y] = 32 as u8 } y = y + 1 }
          var s2: i64 = 0
          while s2 < sw_nsvc {
              let nm: *u8 = ((sw_arena as i64) + sw_name[s2]) as *u8
              let nl: i64 = sw_len(nm)
              if sw_find(cmd, cn, nm, nl) >= 0 { sw_hits[s2] = sw_hits[s2] + 1 } else {
                  if nl > 4 {
                      let at: i64 = sw_find(cmd, cn, nm, nl - 4)
                      if at >= 0 {
                          var bok: i64 = 1
                          let nxp: i64 = at + (nl - 4)
                          if nxp < cn {
                              let c2: i64 = cmd[nxp] as i64
                              if c2 >= 97 { if c2 <= 122 { bok = 0 } }
                              if c2 >= 48 { if c2 <= 57 { bok = 0 } }
                              if c2 == 95 { bok = 0 }
                              if c2 == 46 { bok = 0 }
                          }
                          if bok == 1 { sw_stemhits[s2] = sw_stemhits[s2] + 1 }
                      }
                  }
              }
              s2 = s2 + 1
          }
          if sw_find(cmd, cn, neg, sw_len(neg)) >= 0 { sw_neghits = sw_neghits + 1 }
      }
      pid = pid + 1
  }
  // verdict
  sw_p("  pid_max=" as *u8); sw_num(pidmax)
  sw_p(" scanned_to=" as *u8); sw_num(scanto)
  sw_p(" listen_socket_rows=" as *u8); sw_num(sw_nlp)
  sw_p("\n" as *u8)
  var red: i64 = 0
  var pconf: i64 = 0
  var lclaim: i64 = 0
  var lconf: i64 = 0
  var s3: i64 = 0
  while s3 < sw_nsvc {
      let nm2: *u8 = ((sw_arena as i64) + sw_name[s3]) as *u8
      sw_p("  WITNESS " as *u8); sw_p(nm2)
      sw_p(" port=" as *u8); sw_num(sw_port[s3])
      sw_p(" proc_hits=" as *u8); sw_num(sw_hits[s3])
      sw_p("+" as *u8); sw_num(sw_stemhits[s3]); sw_p("stem" as *u8)
      var present: i64 = 0
      if sw_hits[s3] > 0 { present = 1 }
      if sw_stemhits[s3] > 0 { present = 1 }
      if present == 1 { pconf = pconf + 1; sw_p(" proc=CONFIRMED" as *u8) } else { red = 1; sw_p(" proc=MISSING <- KERNEL DISAGREES" as *u8) }
      if sw_port[s3] > 0 {
          lclaim = lclaim + 1
          var lst: i64 = 0
          var w2: i64 = 0
          while w2 < sw_nlp { if sw_lports[w2] == sw_port[s3] { lst = 1 } w2 = w2 + 1 }
          if lst == 1 { lconf = lconf + 1; sw_p(" listen=CONFIRMED" as *u8) } else { red = 1; sw_p(" listen=MISSING <- KERNEL DISAGREES" as *u8) }
      } else { sw_p(" listen=SKIP-no-port" as *u8) }
      sw_p("\n" as *u8)
      s3 = s3 + 1
  }
  var negport: i64 = 0
  var w3: i64 = 0
  while w3 < sw_nlp { if sw_lports[w3] == SW_NEGPORT { negport = 1 } w3 = w3 + 1 }
  sw_p("  negctl fabricated-name-hits=" as *u8); sw_num(sw_neghits)
  sw_p(" fabricated-port-39999-listening=" as *u8); sw_num(negport)
  sw_p("\n" as *u8)
  if sw_neghits > 0 {
      sw_p("SUP-KERNEL-WITNESS verdict=NEGCTL-INVALID (a fabricated name was 'found' -- the instrument cannot refuse, so it cannot confirm)\n" as *u8)
      sys_exit(3); return 3
  }
  if negport == 1 {
      sw_p("SUP-KERNEL-WITNESS verdict=NEGCTL-INVALID (the fabricated port is listening -- pick a different negctl port and re-run; no verdict issued)\n" as *u8)
      sys_exit(3); return 3
  }
  sw_p("SUP-KERNEL-WITNESS claimed_up=" as *u8); sw_num(sw_nsvc)
  sw_p(" proc_confirmed=" as *u8); sw_num(pconf)
  sw_p(" listen_claimed=" as *u8); sw_num(lclaim)
  sw_p(" listen_confirmed=" as *u8); sw_num(lconf)
  if red == 0 {
      sw_p(" verdict=GREEN (the kernel's process table and socket table independently corroborate every UP claim; negative controls refused)\n" as *u8)
      sys_exit(0); return 0
  }
  sw_p(" verdict=RED (the kernel DISAGREES with at least one supervisor claim -- that disagreement is the finding; report it, do not soften it)\n" as *u8)
  sys_exit(1)
  return 1
311}
nx_sup_kernel_witness.nx source

`nx_sup_kernel_witness.nx` source
