code wiki / (root) / nx_ivvguard_gate.nx
`nx_ivvguard_gate.nx` source

↩ module page · 233 lines · 14449 B
1// nx_ivvguard_gate.nx -- proves the IV+V beat safety predicates BEFORE any forking or deleting code is
2// written (2026-08-07). Every case is a fabricated string; the gate has NO side effects at all.
3// The NEGATIVE cases are the point: each one is a specific way a plausible-looking implementation would
4// have been unsafe, so a passing run is evidence about the failure modes, not just the happy path.
5// expect_exit: 0   license_tier: ORIGINAL   No hw writes (Rule 26).
6import "nx_ivvguard.nx"
7import "nx_gate_verdict.nx"
8import "nx_syscalls.nx"
9
10func gw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
11func row(name: *u8, ok: i64, ctr: *i64) -> i64 {
  ctr[1] = ctr[1] + 1
  if ok==1 { ctr[0]=ctr[0]+1; gw("  [PASS] " as *u8) } else { gw("  [FAIL] " as *u8) }
  gw(name); gw("\\n" as *u8); return ok
15}
16
17func main() -> i64 {
  gw("=== nx_ivvguard_gate: exec allowlist + wipe confinement, proven before any exec or unlink ===\\n" as *u8)
  let ctr: *i64 = sys_mmap(16) as *i64
  ctr[0]=0; ctr[1]=0
21
  // ---- T-A EXEC ALLOWLIST: accepts exactly the sanctioned shapes ----
  var a1: i64 = 0
  if ivv_cmd_allowed("./nx_coa_gate.elf" as *u8) == 1 { if ivv_cmd_allowed("./_offc_probe.elf" as *u8) == 1 { a1 = 1 } }
  row("T-A1 allowlist ACCEPTS ./nx_*.elf and ./_*.elf" as *u8, a1, ctr)
26
  // a SUFFIX-only implementation would admit this absolute path -- the classic mistake
  var a2: i64 = 0; if ivv_cmd_allowed("/usr/bin/evil.elf" as *u8) == 0 { a2 = 1 }
  row("T-A2 REFUSES an absolute path ending .elf (suffix-only test would EXECUTE it)" as *u8, a2, ctr)
30
  // a PREFIX-only implementation would admit this
  var a3: i64 = 0; if ivv_cmd_allowed("./nx_notanelf" as *u8) == 0 { a3 = 1 }
  row("T-A3 REFUSES ./nx_ without .elf (prefix-only test would EXECUTE it)" as *u8, a3, ctr)
34
  // an UNANCHORED contains-test would admit this
  var a4: i64 = 0; if ivv_cmd_allowed("/tmp/x/./nx_evil.elf" as *u8) == 0 { a4 = 1 }
  row("T-A4 REFUSES a path that merely CONTAINS ./nx_ (contains-test would EXECUTE it)" as *u8, a4, ctr)
38
  // ---- T-B WIPE CONFINEMENT ----
  var b1: i64 = 0; if ivv_wipe_allowed("/tmp/ivv_scratch" as *u8) == 1 { b1 = 1 }
  row("T-B1 confinement ACCEPTS a real /tmp/ path" as *u8, b1, ctr)
42
  var b2: i64 = 0; if ivv_wipe_allowed("/etc/passwd" as *u8) == 0 { b2 = 1 }
  row("T-B2 REFUSES outside /tmp -- nothing is deleted" as *u8, b2, ctr)
45
  var b3: i64 = 0; if ivv_wipe_allowed("/tmp" as *u8) == 0 { b3 = 1 }
  row("T-B3 REFUSES bare /tmp (no trailing slash = not INSIDE the directory)" as *u8, b3, ctr)
48
  var b4: i64 = 0; if ivv_wipe_allowed("/var/tmp/x" as *u8) == 0 { b4 = 1 }
  row("T-B4 REFUSES a path that merely CONTAINS /tmp/ later in the string" as *u8, b4, ctr)
51
  // STRONGER THAN THE SHELL: the original glob admits a traversal segment and escapes.
  var b5: i64 = 0; if ivv_wipe_allowed("/tmp/../etc/shadow" as *u8) == 0 { b5 = 1 }
  row("T-B5 REFUSES traversal out of /tmp -- the shell glob does NOT (deliberate strengthening)" as *u8, b5, ctr)
55
  // ---- T-D / T-E THE VERDICT IS A CONJUNCTION ----
  let out: *u8 = sys_mmap(256)
  var o: i64 = 0
  let s1: *u8 = "gate ran fine but printed no verdict anchor\\n" as *u8
  while s1[o] != (0 as u8) { out[o] = s1[o]; o = o + 1 }
  var d1: i64 = 0; if ivv_is_green(0, out, o, "verdict=GREEN" as *u8) == 0 { d1 = 1 }
  row("T-D rc=0 but marker ABSENT -> DRIFT (this is the fake-green class the beat exists to catch)" as *u8, d1, ctr)
63
  let out2: *u8 = sys_mmap(256)
  var o2: i64 = 0
  let s2: *u8 = "NX-FOO passed 3/3 verdict=GREEN (all good)\\n" as *u8
  while s2[o2] != (0 as u8) { out2[o2] = s2[o2]; o2 = o2 + 1 }
  var e1: i64 = 0; if ivv_is_green(1, out2, o2, "verdict=GREEN" as *u8) == 0 { e1 = 1 }
  row("T-E marker PRESENT but rc!=0 -> DRIFT (the mirror image; a printed claim is not an exit code)" as *u8, e1, ctr)
70
  var g1: i64 = 0; if ivv_is_green(0, out2, o2, "verdict=GREEN" as *u8) == 1 { g1 = 1 }
  row("T-G rc=0 AND marker present -> GREEN (the conjunction is not vacuous)" as *u8, g1, ctr)
73
  // ---- T-F THE TOOTH FLOOR: AN IMPROVEMENT MUST PASS, A REGRESSION MUST FAIL ----
  // Built from the live failure: row ivv-lawwarden declares "passed 15/15 verdict=GREEN" while the gate
  // now runs 26 teeth, so an equality check reports drift FOREVER even once the gate is healthy.
  let fo: *u8 = sys_mmap(512)
  var fl: i64 = 0
  let fs: *u8 = "nx_law_warden gate\n  T1 ok\npassed 26/26 verdict=GREEN\n" as *u8
  while fs[fl] != (0 as u8) { fo[fl] = fs[fl]; fl = fl + 1 }
  let fr: *i64 = sys_mmap(64) as *i64
82
  var f1: i64 = 0
  if ivv_is_green2(0, fo, fl, "passed 15/15 verdict=GREEN" as *u8, fr) == 1 { f1 = 1 }
  row("T-F1 a gate that GREW 15->26 teeth is GREEN (the equality check called this drift forever)" as *u8, f1, ctr)
86
  var f1b: i64 = 0
  if fr[1] == 26 { if fr[2] == 15 { f1b = 1 } }
  row("T-F1b and it REPORTS observed=26 against declared floor=15 (the numbers are read, not ignored)" as *u8, f1b, ctr)
90
  let go: *u8 = sys_mmap(512)
  var gl: i64 = 0
  let gs: *u8 = "passed 3/3 verdict=GREEN\n" as *u8
  while gs[gl] != (0 as u8) { go[gl] = gs[gl]; gl = gl + 1 }
  var f2: i64 = 0
  if ivv_is_green2(0, go, gl, "passed 15/15 verdict=GREEN" as *u8, fr) == 0 { f2 = 1 }
  row("T-F2 a gate that SHRANK 15->3 teeth is DRIFT -- tooth loss is exactly what an anchor-only check goes blind to" as *u8, f2, ctr)
98
  let ho: *u8 = sys_mmap(512)
  var hl: i64 = 0
  let hs: *u8 = "  T15 segamp: FAIL\npassed 25/26 verdict=RED\n" as *u8
  while hs[hl] != (0 as u8) { ho[hl] = hs[hl]; hl = hl + 1 }
  var f3: i64 = 0
  if ivv_is_green2(1, ho, hl, "passed 15/15 verdict=GREEN" as *u8, fr) == 0 { f3 = 1 }
  row("T-F3 the REAL live failure 25/26 verdict=RED is still DRIFT -- the floor loosens the count, never the verdict" as *u8, f3, ctr)
106
  var f4: i64 = 0
  if ivv_is_green2(0, ho, hl, "passed 15/15 verdict=GREEN" as *u8, fr) == 0 { f4 = 1 }
  row("T-F4 25 of 26 passing is NOT green even at rc=0 -- passed must equal total, floor or no floor" as *u8, f4, ctr)
110
  // ---- T-F4b THE DOUBLE-PRINT SHAPE. THIS GATE WAS 34/34 BEFORE AND AFTER A REAL BUG FIX. ----
  // The fixture is the VERBATIM output of nx_asset_merkle_gate, captured by running it, not invented:
  // the shared base-class verdict refactor makes gates print the tally TWICE -- once BARE on a summary
  // line, then again with the verdict suffix. ivv_match_counted took the FIRST "passed ", parsed its
  // digits, failed the (correct) suffix-immediately-after rule against the newline, and reported the
  // marker ABSENT while it sat one line below. 12 of 95 sweep rows were falsely UNPROVEN, ten of them
  // consecutive ivv-asset_* gates.
  // ★★★★★★A GATE THAT PASSES IDENTICALLY BEFORE AND AFTER A REAL BUG FIX DID NOT COVER THAT BUG --
  //   AND ITS GREEN WAS THE REASON NOBODY LOOKED HERE FIRST.
  // ★★★★★BUILD THE FIXTURE FROM CAPTURED BYTES, NOT FROM YOUR MODEL OF THE PRODUCER: the double
  //   print is not something anyone would have thought to fabricate.
  let do2: *u8 = sys_mmap(512)
  var dl: i64 = 0
  let ds: *u8 = "ASSET-MERKLE-GATE passed 4/4\nNX-ASSET-MERKLE-GATE passed 4/4 verdict=GREEN (teeth unchanged)\n" as *u8
  while ds[dl] != (0 as u8) { do2[dl] = ds[dl]; dl = dl + 1 }
  var f4b: i64 = 0
  if ivv_is_green2(0, do2, dl, "passed 4/4 verdict=GREEN" as *u8, fr) == 1 { f4b = 1 }
  row("T-F4b a BARE tally printed before the real marker must not hide it (the live asset_* double-print)" as *u8, f4b, ctr)
129
  // NON-VACUITY FOR T-F4b: the same buffer with a marker that genuinely is not there must still FAIL,
  // so T-F4b cannot be satisfied by a matcher that simply says yes to everything.
  var f4c: i64 = 0
  if ivv_is_green2(0, do2, dl, "passed 9/9 verdict=GREEN" as *u8, fr) == 0 { f4c = 1 }
  row("T-F4c and the SAME buffer still REFUSES a count that is absent from it (T-F4b is not vacuous)" as *u8, f4c, ctr)
135
  // The count-free rows must behave EXACTLY as before, or this change silently regresses them.
  let no: *u8 = sys_mmap(512)
  var nl2: i64 = 0
  let ns: *u8 = "argecho: planted-lie\n" as *u8
  while ns[nl2] != (0 as u8) { no[nl2] = ns[nl2]; nl2 = nl2 + 1 }
  var f5: i64 = 0
  if ivv_is_green2(0, no, nl2, "THIS-MARKER-NEVER-APPEARS-BY-DESIGN" as *u8, fr) == 0 { f5 = 1 }
  row("T-F5 the live negative control still FAILS under v2 -- a count-free marker falls back to containment unchanged" as *u8, f5, ctr)
144
  var f6: i64 = 0
  if fr[2] == 0 - 1 { f6 = 1 }
  row("T-F6 and a count-free marker reports NO floor (-1) rather than a fabricated 0" as *u8, f6, ctr)
148
  // The suffix must sit immediately after the count, else an unrelated line could satisfy the marker.
  let xo: *u8 = sys_mmap(512)
  var xl: i64 = 0
  let xs: *u8 = "passed 26/26 verdict=RED\nsomewhere later verdict=GREEN\n" as *u8
  while xs[xl] != (0 as u8) { xo[xl] = xs[xl]; xl = xl + 1 }
  var f7: i64 = 0
  if ivv_is_green2(0, xo, xl, "passed 15/15 verdict=GREEN" as *u8, fr) == 0 { f7 = 1 }
  row("T-F7 a verdict=GREEN appearing ELSEWHERE cannot satisfy the marker -- the suffix is anchored to the count" as *u8, f7, ctr)
157
  var f8: i64 = 0
  let sp: *i64 = sys_mmap(64) as *i64
  if ivv_find_count("GALXCOMPACTGATE 9/9 GREEN" as *u8, sp) == 1 { if sp[0] == 16 { f8 = 1 } }
  row("T-F8 the count token is located in the OTHER live marker shape too (no verdict= required)" as *u8, f8, ctr)
162
  var f9: i64 = 0
  if ivv_floor_ok(26, 15) == 1 { if ivv_floor_ok(14, 15) == 0 { if ivv_floor_ok(15, 15) == 1 { f9 = 1 } } }
  row("T-F9 floor relation is >= not == : grow PASS, equal PASS, shrink FAIL (non-vacuous in both directions)" as *u8, f9, ctr)
166
  // ---- T-S THE STALE-BUFFER DEFECT, CAUGHT IN PRODUCTION AND NOW NAILED DOWN ----
  let sres: *i64 = sys_mmap(64) as *i64
  sres[0] = 9
  sres[1] = 9
  sres[2] = 9
  let so: *u8 = sys_mmap(512)
  var sn: i64 = 0
  let ss: *u8 = "some gate that failed hard\n" as *u8
  while ss[sn] != (0 as u8) { so[sn] = ss[sn]; sn = sn + 1 }
  ivv_is_green2(1, so, sn, "passed 15/15 verdict=GREEN" as *u8, sres)
  var s0: i64 = 0
  if sres[1] == 0 - 1 { s0 = 1 }
  row("T-S0 a FAILING row does not inherit the previous row's tooth counts (live sweep reported 9/9 three times)" as *u8, s0, ctr)
180
  // ---- T-R0 THE DEFECT ITSELF, PROVEN WITHOUT MUTATING ANY SOURCE ----
  // The old rule was ivg_ends(WHOLE_FIELD, ".elf"). Rather than reintroduce it to watch it fail --
  // this tree has already been burned once by a mutant that ESCAPED the tool that planted it -- the
  // tooth simply evaluates that exact expression on the exact live row and asserts it comes back 0.
  // (STAR)A BITE PROOF DOES NOT REQUIRE EDITING THE CODE UNDER TEST; IF THE OLD RULE CAN BE WRITTEN AS
  // AN EXPRESSION, IT CAN BE FALSIFIED AS ONE, AND NOTHING IS LEFT BEHIND TO ESCAPE.
  var r0: i64 = 0
  if ivg_ends("./nx_actlog.elf selftest /tmp/ccgate/ivv_al.jrnl" as *u8, ".elf" as *u8) == 0 { r0 = 1 }
  row("T-R0 BITE: the OLD whole-field suffix rule REFUSES live row ivv-actlog -- the 12/12 gate was green on a broken predicate" as *u8, r0, ctr)
190
  // ---- T-R THE FOUR REAL ROWS, READ OFF THE LIVE ivvreg- PLANE 2026-08-07 ----
  // These exist because the fabricated fixtures above ALL PASSED while the predicate was WRONG. Every
  // string below is a verbatim field from the live plane, not an invention. T-R2 is the one that bit:
  // its command carries arguments and ends .jrnl, so the original whole-field suffix test refused it.
  // (STAR)THE CHEAPEST TOOTH IN ANY GATE IS ONE REAL ROW; IT OUTRANKS TEN CLEVER FABRICATIONS BECAUSE
  // IT IS THE ONLY ONE THAT CANNOT SHARE YOUR MISCONCEPTION.
  var r1: i64 = 0; if ivv_cmd_allowed("./_ss_compact_cap_gate.elf" as *u8) == 1 { r1 = 1 }
  row("T-R1 live row ivv-sscap ACCEPTED (bare exe, underscore prefix)" as *u8, r1, ctr)
199
  var r2: i64 = 0; if ivv_cmd_allowed("./nx_actlog.elf selftest /tmp/ccgate/ivv_al.jrnl" as *u8) == 1 { r2 = 1 }
  row("T-R2 live row ivv-actlog ACCEPTED -- ARGUMENTS, and the field ENDS .jrnl (whole-field suffix test REFUSED this valid row)" as *u8, r2, ctr)
202
  var r3: i64 = 0; if ivv_cmd_allowed("./nx_law_warden.elf selftest" as *u8) == 1 { r3 = 1 }
  row("T-R3 live row ivv-lawwarden ACCEPTED (one argument)" as *u8, r3, ctr)
205
  var r4: i64 = 0; if ivv_cmd_allowed("./nx_tool_argecho.elf planted-lie" as *u8) == 1 { r4 = 1 }
  row("T-R4 live row ivv-negcontrol ACCEPTED -- the planted lie must RUN in order to FAIL" as *u8, r4, ctr)
208
  // The argument tail is inert argv, never re-parsed, so a hostile-looking argument changes nothing
  // about WHICH binary runs. What must NOT happen is the reverse: a sanctioned-looking ARGUMENT
  // laundering an unsanctioned EXE.
  var r5: i64 = 0; if ivv_cmd_allowed("/bin/sh ./nx_ok.elf" as *u8) == 0 { r5 = 1 }
  row("T-R5 REFUSES an unsanctioned exe carrying a sanctioned-looking ARGUMENT (token 0 is the only token that decides)" as *u8, r5, ctr)
214
  var r6: i64 = 0; if ivv_cmd_allowed("./nx_notanelf selftest" as *u8) == 0 { r6 = 1 }
  row("T-R6 REFUSES a sanctioned prefix whose FIRST TOKEN lacks .elf even though a later token has it" as *u8, r6, ctr)
217
  // ---- T-S THE NO-WIPE SENTINEL ----
  // Two of the four live rows carry a bare dash in the wipe column.
  var s3: i64 = 0; if ivv_wipe_none("-" as *u8) == 1 { s3 = 1 }
  row("T-S1 the live dash sentinel is recognised as NO-WIPE" as *u8, s3, ctr)
222
  var s4: i64 = 0; if ivv_wipe_allowed("-" as *u8) == 0 { s4 = 1 }
  row("T-S2 and the dash is STILL refused as a path -- skipping a wipe and permitting one are different answers" as *u8, s4, ctr)
225
  var s5: i64 = 0; if ivv_wipe_none("/tmp/ccgate/_cctest" as *u8) == 0 { s5 = 1 }
  row("T-S3 a real path is NOT mistaken for the sentinel (the sentinel test is not vacuous)" as *u8, s5, ctr)
228
  var s6: i64 = 0; if ivv_wipe_none("-x" as *u8) == 0 { s6 = 1 }
  row("T-S4 the sentinel is EXACT -- a dash-prefixed path is not a sentinel" as *u8, s6, ctr)
231
  let rc: i64 = gv_verdict("IVVGUARD" as *u8, ctr, "exec allowlist + wipe confinement + non-vacuous verdict, proven on the FOUR LIVE ivvreg- rows as well as fabricated negatives" as *u8)
  sys_exit(rc); return rc
234}
nx_ivvguard_gate.nx source

`nx_ivvguard_gate.nx` source
