nx_gpt_relocate_gate.nx source

1// nx_gpt_relocate_gate.nx -- the REFEREE for smallos SO0 (nk0_gpt_relocate in nx_efi_fat32_image, 2026-09-02). 2// Authors a real image with the emitter, grows a copy to a larger "device", relocates the backup GPT to the 3// device's true end, and re-reads the DEVICE to prove: backup header at the last LBA, primary AlternateLBA and 4// LastUsableLBA moved, protective MBR widened, both partition entries byte-unchanged, the old mid-disk backup 5// retired, a second run idempotent, and every refusal (smaller device, not GPT, a foreign disk GUID) named and 6// write-free. The gate carries its own CRC32 ONLY to forge a valid-but-foreign header for the neg-control. 7// nx_gpt_relocate_gate [subject-elf] default _build/nx_efi_fat32_image.sov.elf (cwd nxc2) 8// Fixtures are assembled at runtime under /tmp/nx_gpt_relocate_gate/. license_tier: ORIGINAL. No hw writes: 9// every "device" here is a regular file. 10import "nx_syscalls.nx" 11import "nx_gate_verdict.nx" 12import "nx_gatekit_lib.nx" 13 14const RG_CAP: i64 = 65536 15const RG_SEC: i64 = 512 16const RG_IMG_BYTES: i64 = 69257728 // the emitter's authored size (its IMG_BYTES) 17const RG_OLD_LAST: i64 = 135268 // the emitter's LAST_LBA 18const RG_GROW_BYTES: i64 = 100663296 // 96 MiB "device": larger than the image, sector-aligned 19const RG_SMALL_BYTES: i64 = 1048576 // a "device" smaller than the image 20const RG_HDR_SZ: i64 = 92 21const RG_ARR_SEC: i64 = 32 22const RG_ENTSZ: i64 = 128 23const RG_FAKE_EFI_BYTES: i64 = 1024 24const RG_ROOT: *u8 = "/tmp/nx_gpt_relocate_gate" 25const RG_EFI: *u8 = "/tmp/nx_gpt_relocate_gate/fake.efi" 26const RG_BASE: *u8 = "/tmp/nx_gpt_relocate_gate/base.img" 27const RG_GROW: *u8 = "/tmp/nx_gpt_relocate_gate/grow.img" 28const RG_SMALL: *u8 = "/tmp/nx_gpt_relocate_gate/small.img" 29const RG_NOTGPT: *u8 = "/tmp/nx_gpt_relocate_gate/notgpt.img" 30const RG_FOREIGN: *u8 = "/tmp/nx_gpt_relocate_gate/foreign.img" 31 32func rg_r32(b: *u8, off: i64) -> i64 { return (b[off] as i64) | ((b[off+1] as i64) << 8) | ((b[off+2] as i64) << 16) | ((b[off+3] as i64) << 24) } 33func rg_r64(b: *u8, off: i64) -> i64 { return rg_r32(b, off) | (rg_r32(b, off + 4) << 32) } 34func rg_w32(b: *u8, off: i64, v: i64) -> i64 { b[off]=(v&0xff) as u8; b[off+1]=((v>>8)&0xff) as u8; b[off+2]=((v>>16)&0xff) as u8; b[off+3]=((v>>24)&0xff) as u8; return 0 } 35// IEEE CRC32, fixture-signing only (the subject carries its own; this copy exists so the gate can forge a 36// VALID header that is not ours -- an adversary's tool, never the ruler) 37func rg_crc32(b: *u8, off: i64, n: i64) -> i64 { 38 var crc: i64 = 0xFFFFFFFF 39 var i: i64 = 0 40 while i < n { 41 crc = crc ^ ((b[off + i] as i64) & 0xff) 42 var bit: i64 = 0 43 while bit < 8 { 44 let lsb: i64 = crc & 1 45 let mask: i64 = 0 - lsb 46 crc = ((crc >> 1) & 0x7FFFFFFFFFFFFFFF) ^ (mask & 0xEDB88320) 47 crc = crc & 0xFFFFFFFF 48 bit = bit + 1 49 } 50 i = i + 1 51 } 52 return (crc ^ 0xFFFFFFFF) & 0xFFFFFFFF 53} 54func rg_sig_at(b: *u8, off: i64) -> i64 { 55 let sig: *u8 = "EFI PART" as *u8 56 var i: i64 = 0 57 while i < 8 { if (b[off + i] as i64) != (sig[i] as i64) { return 0 } i = i + 1 } 58 return 1 59} 60// write n bytes of buf to path (truncating), then optionally extend the file to `total` bytes (sparse tail) 61func rg_write_file(path: *u8, buf: *u8, n: i64, total: i64) -> i64 { 62 let fd: i64 = sys_openat_wr(path, 0x1a4) 63 if fd < 0 { return 0 - 1 } 64 var put: i64 = 0 65 while put < n { let w: i64 = sys_write(fd, (buf + put) as *u8, n - put); if w <= 0 { sys_close(fd); return 0 - 1 } put = put + w } 66 if total > n { 67 let one: *u8 = sys_mmap(8) 68 one[0] = 0 as u8 69 if sys_lseek(fd, total - 1, 0) != total - 1 { sys_close(fd); return 0 - 1 } 70 sys_write(fd, one, 1) 71 } 72 sys_close(fd) 73 return 0 74} 75func rg_same(a: *u8, b: *u8, off: i64, n: i64) -> i64 { 76 var i: i64 = 0 77 while i < n { if a[off + i] != b[off + i] { return 0 } i = i + 1 } 78 return 1 79} 80func rg_same2(a: *u8, aoff: i64, b: *u8, boff: i64, n: i64) -> i64 { 81 var i: i64 = 0 82 while i < n { if a[aoff + i] != b[boff + i] { return 0 } i = i + 1 } 83 return 1 84} 85func rg_run(elf: *u8, a1: *u8, a2: *u8, out: *u8, ol: *i64) -> i64 { 86 return gk_run_capture(elf, a1, a2, 0 as *u8, 0 as *u8, out, RG_CAP, ol) 87} 88 89func main(argc: i64, argv: *i64) -> i64 { 90 var elf: *u8 = "_build/nx_efi_fat32_image.sov.elf" as *u8 91 if argc >= 2 { elf = argv[1] as *u8 } 92 gv_head("NX-GPT-RELOCATE-GATE: SO0 -- the authored boot image relocates its backup GPT to a real device's end" as *u8) 93 let ctr: *i64 = gv_ctr() 94 gv_need("subject elf present" as *u8, gk_exists(elf), ctr) 95 gk_mkdir(RG_ROOT) 96 let out: *u8 = sys_mmap(RG_CAP) 97 let ol: *i64 = sys_mmap(16) as *i64 98 99 // ---- author a real image with a fake PE payload (the emitter checks MZ only) ---- 100 let fe: *u8 = sys_mmap(RG_FAKE_EFI_BYTES) 101 fe[0] = 77 as u8; fe[1] = 90 as u8 102 var fi: i64 = 2 103 while fi < RG_FAKE_EFI_BYTES { fe[fi] = (fi & 0xff) as u8; fi = fi + 1 } 104 rg_write_file(RG_EFI, fe, RG_FAKE_EFI_BYTES, 0) 105 rg_run(elf, RG_EFI, RG_BASE, out, ol) 106 gv_need("fixture-reached-the-condition: the emitter authored base.img GREEN at its declared size" as *u8, gk_out_has(out, ol[0], "NOS-USB GREEN" as *u8) * (gk_size(RG_BASE) == RG_IMG_BYTES), ctr) 107 let lp: *i64 = sys_mmap(16) as *i64 108 let base: *u8 = sys_read_file(RG_BASE, lp) 109 gv_need("base image readable whole" as *u8, lp[0] == RG_IMG_BYTES, ctr) 110 gv_check("T1 the authored image's backup header sits at ITS OWN last LBA (the condition a real stick breaks)" as *u8, rg_sig_at(base, RG_OLD_LAST * RG_SEC) * (rg_r64(base, RG_SEC + 32) == RG_OLD_LAST), ctr) 111 112 // ---- grow a copy to a 96 MiB device and relocate ---- 113 rg_write_file(RG_GROW, base, RG_IMG_BYTES, RG_GROW_BYTES) 114 gv_need("fixture-reached-the-condition: grow.img is a 96 MiB device carrying the image at its head" as *u8, gk_size(RG_GROW) == RG_GROW_BYTES, ctr) 115 let new_last: i64 = RG_GROW_BYTES / RG_SEC - 1 116 let new_arr: i64 = new_last - RG_ARR_SEC 117 let rc1: i64 = rg_run(elf, "relocate" as *u8, RG_GROW, out, ol) 118 gv_puts(out) 119 gv_check("T2 relocate reports GREEN with the device geometry and verified=1, exit 0" as *u8, gk_out_has(out, ol[0], "NOS-USB RELOCATE GREEN" as *u8) * gk_out_has(out, ol[0], "verified=1" as *u8) * (rc1 == 0), ctr) 120 let gl: *i64 = sys_mmap(16) as *i64 121 let grow: *u8 = sys_read_file(RG_GROW, gl) 122 gv_need("grown device readable whole after relocate" as *u8, gl[0] == RG_GROW_BYTES, ctr) 123 gv_check("T3 the backup header now sits at the DEVICE's last LBA, names itself there, and points back at LBA 1 and at the moved array" as *u8, rg_sig_at(grow, new_last * RG_SEC) * (rg_r64(grow, new_last * RG_SEC + 24) == new_last) * (rg_r64(grow, new_last * RG_SEC + 32) == 1) * (rg_r64(grow, new_last * RG_SEC + 72) == new_arr), ctr) 124 gv_check("T4 the primary header's AlternateLBA and LastUsableLBA moved to the device's end" as *u8, (rg_r64(grow, RG_SEC + 32) == new_last) * (rg_r64(grow, RG_SEC + 48) == new_arr - 1), ctr) 125 gv_check("T5 the protective MBR now spans the whole device" as *u8, rg_r32(grow, 446 + 12) == new_last, ctr) 126 gv_check("T6 both partition entries are byte-unchanged (relocation never edits a partition)" as *u8, rg_same(base, grow, 2 * RG_SEC, 2 * RG_ENTSZ), ctr) 127 gv_check("T7 the moved array is byte-identical to the primary array" as *u8, rg_same2(grow, new_arr * RG_SEC, grow, 2 * RG_SEC, RG_ARR_SEC * RG_SEC), ctr) 128 gv_check("T8 the old mid-disk backup header is retired (signature gone), so no reader can find two" as *u8, 1 - rg_sig_at(grow, RG_OLD_LAST * RG_SEC), ctr) 129 gv_check("T9 the ESP volume is untouched: its BPB still reads FAT32 and the payload's MZ is still at its cluster" as *u8, rg_same(base, grow, 1048576, 512) * rg_same(base, grow, 1590272 + 3 * RG_SEC, RG_FAKE_EFI_BYTES), ctr) 130 131 // ---- idempotence: a second run writes nothing ---- 132 let rc2: i64 = rg_run(elf, "relocate" as *u8, RG_GROW, out, ol) 133 let g2l: *i64 = sys_mmap(16) as *i64 134 let grow2: *u8 = sys_read_file(RG_GROW, g2l) 135 gv_check("T10 a second relocate reports ALREADY-RELOCATED (its own CRC check on the moved backup passes) with exit 0" as *u8, gk_out_has(out, ol[0], "ALREADY-RELOCATED" as *u8) * (rc2 == 0), ctr) 136 gv_check("T11 fixture-reached-the-condition: the second run left head and tail byte-identical" as *u8, (g2l[0] == RG_GROW_BYTES) * rg_same(grow, grow2, 0, 34 * RG_SEC) * rg_same(grow, grow2, new_arr * RG_SEC, (RG_ARR_SEC + 1) * RG_SEC), ctr) 137 138 // ---- refusals, each named, each write-free ---- 139 rg_write_file(RG_SMALL, base, RG_SMALL_BYTES, 0) 140 let rc3: i64 = rg_run(elf, "relocate" as *u8, RG_SMALL, out, ol) 141 let sl: *i64 = sys_mmap(16) as *i64 142 let small: *u8 = sys_read_file(RG_SMALL, sl) 143 gv_check("neg-control-a-device-smaller-than-the-image-is-REFUSED-by-rule-with-exit-2-and-nothing-written" as *u8, gk_out_has(out, ol[0], "REFUSED rule=device-smaller-than-image" as *u8) * (rc3 == 2) * (sl[0] == RG_SMALL_BYTES) * rg_same(base, small, 0, RG_SMALL_BYTES), ctr) 144 145 let ng: *u8 = sys_mmap(RG_IMG_BYTES) 146 var ni: i64 = 0 147 while ni < RG_IMG_BYTES { ng[ni] = base[ni]; ni = ni + 1 } 148 ng[510] = 0 as u8 149 ng[511] = 0 as u8 150 rg_write_file(RG_NOTGPT, ng, RG_IMG_BYTES, RG_GROW_BYTES) 151 let rc4: i64 = rg_run(elf, "relocate" as *u8, RG_NOTGPT, out, ol) 152 let nl: *i64 = sys_mmap(16) as *i64 153 let notgpt: *u8 = sys_read_file(RG_NOTGPT, nl) 154 gv_check("neg-control-a-non-GPT-device-is-REFUSED-by-rule-and-its-tail-stays-empty" as *u8, gk_out_has(out, ol[0], "REFUSED rule=not-gpt-no-mbr-signature" as *u8) * (rc4 == 2) * (1 - rg_sig_at(notgpt, new_last * RG_SEC)) * rg_same(ng, notgpt, 0, 34 * RG_SEC), ctr) 155 156 // a VALID header that is not ours: flip one disk-GUID byte and re-sign the CRC exactly as a firmware would 157 let fg: *u8 = sys_mmap(RG_IMG_BYTES) 158 var fj: i64 = 0 159 while fj < RG_IMG_BYTES { fg[fj] = base[fj]; fj = fj + 1 } 160 fg[RG_SEC + 56] = ((fg[RG_SEC + 56] as i64) ^ 0xff) as u8 161 rg_w32(fg, RG_SEC + 16, 0) 162 let fcrc: i64 = rg_crc32(fg, RG_SEC, RG_HDR_SZ) 163 rg_w32(fg, RG_SEC + 16, fcrc) 164 rg_write_file(RG_FOREIGN, fg, RG_IMG_BYTES, RG_GROW_BYTES) 165 let rc5: i64 = rg_run(elf, "relocate" as *u8, RG_FOREIGN, out, ol) 166 let fl: *i64 = sys_mmap(16) as *i64 167 let foreign: *u8 = sys_read_file(RG_FOREIGN, fl) 168 gv_check("neg-control-a-valid-GPT-with-a-FOREIGN-disk-GUID-is-REFUSED-by-rule (never-brick: only our own image is ever rewritten)" as *u8, gk_out_has(out, ol[0], "REFUSED rule=foreign-disk-guid" as *u8) * (rc5 == 2) * (1 - rg_sig_at(foreign, new_last * RG_SEC)) * rg_same(fg, foreign, 0, 34 * RG_SEC), ctr) 169 // recompute exactly as a parser does: CRC field zeroed during the sum, then compared to the stored value 170 let fsave: i64 = rg_r32(fg, RG_SEC + 16) 171 rg_w32(fg, RG_SEC + 16, 0) 172 let fchk: i64 = rg_crc32(fg, RG_SEC, RG_HDR_SZ) 173 rg_w32(fg, RG_SEC + 16, fsave) 174 gv_check("T12 fixture-reached-the-condition: the forged header really carried a valid CRC (the refusal was the GUID rule, not the CRC rule)" as *u8, fchk == fsave, ctr) 175 176 let rc: i64 = gv_verdict("NX-GPT-RELOCATE-GATE" as *u8, ctr, "SO0 nk0_gpt_relocate: the backup GPT lands at the real device's end, the primary follows, partitions and the ESP are untouched, the run is idempotent, and every refusal is named and write-free" as *u8) 177 sys_exit(rc) 178 return rc 179}