_k_r2_001c2_gate.nx source

1// _k_r2_001c2_gate.nx -- the K-R2-001c2 gate (virtio-NET MMIO QUEUE-CONFIGURATION REGISTER 2// layer; the second slice of the K-R2-001c net virtqueue epic). It is the K-R2-001b1 3// queue-config gate applied to the SECOND virtio device, virtio-net (DeviceID=1) @ base 4// 0x10002000. NO mocks: runs the REAL nx_virtio_hs_emit (the SAME emitter the blk b-series 5// and the net c1 handshake use -- data-only on base/device-id/banner/queue-config, so it 6// stays byte-for-byte backward-compatible), then RUNS the emitted image on the SOVEREIGN 7// rv64 emulator (rv64im_min_sim + the second rv64im_min_virtio net instance @ 0x10002000, 8// which already carries the legacy virtqueue-config registers QueueSel / QueueNumMax / 9// QueueNum / QueueAlign / QueuePFN / QueueNotify resolved per-instance -- the PRIMARY, gating 10// lane: Nishi owns the runtime) and asserts the captured serial transcript CONTAINS the 11// emitter's golden ("VNET ACK DRV FEAT OK VQ\n" -- after the net handshake the driver 12// selected a virtqueue, read QueueNumMax, latched the ring size, bound the guest ring 13// page-frame via QueuePFN, kicked QueueNotify, and READ QueuePFN BACK to confirm the binding) 14// AND the sovereign emu reports a clean SiFive-finisher halt. The blk device @ 0x10001000 is 15// left BYTE-UNTOUCHED (its own gates VIRTGATE..SECTGATE still pass, re-proven by re-run). 16// 17// Then the ALIGNMENT lane: qemu-system-riscv64 -machine virt -global 18// virtio-mmio.force-legacy=true with a REAL virtio-blk-device (first) + a REAL 19// virtio-net-device (second). qemu fills its virtio-mmio slots in REVERSE, so the first 20// device (blk) lands at the top slot 0x10008000 and the SECOND device (net) lands at the next 21// slot DOWN, 0x10007000. The gate authors a SECOND net image from a base-rewritten spec 22// (base = the qemu net reverse-slot 0x10007000) and runs THAT on qemu; the SAME queue-config 23// driver completes against the REAL legacy virtio-net transport (QueuePFN read-back is 24// genuinely RW on the real net device) and emits the SAME golden -> lanes AGREE. 25// 26// Finally a TAMPER test: corrupt the QueuePFN-EXPECTED constant in the sovereign image (the 27// driver loads its own QueuePFN read-back into t3 and compares against the li-loaded expected 28// in t4; the expected li is the addi following the unique `lw t3,0x40(t2)` read-back load). 29// Bumping the addi's high immediate byte makes the read-back verify branch PAST stage 5 30// straight to the finisher -> the transcript loses ONLY its " VQ" canary (the handshake tail 31// survives) -> the gate MUST go RED. Evidence -> knowledge/status/virtio_net.log 32// (NETVQCFGGATE row; the queue row's ||MARK= reads it). 33// Sovereign orchestration (fork/dup3/execve/wait4). license_tier: ORIGINAL 34import "nx_syscalls.nx" 35 36// the unique rv64 encoding of `lw t3, 0x40(t2)` -- the QueuePFN read-back load. The 37// QueuePFN-expected constant the driver compares against is the li that follows it (lui 38// at +4, addi at +8); corrupting the addi's immediate is the queue-config tamper. 39const G_QPFN_LOAD_WORD: i64 = 0x0403ae03 // lw t3, 0x040(t2) (QueuePFN read-back) 40const G_QEMU_BASE: i64 = 0x10007000 // the slot qemu-virt assigns the SECOND device (net) 41 42func g_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 43func g_fp(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 } 44func g_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;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{bb[i]=t[k-1-i];i=i+1}; sys_write(fd,bb,k); return 0 } 45 46// run nx_virtio_hs_emit <spec>; return child wait status (0 = ok) 47func g_run_emit(spec: *u8) -> i64 { 48 let pid: i64 = sys_fork() 49 if pid == 0 { 50 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4) 51 if dn >= 0 { sys_dup3(dn, 1, 0) } 52 let argv: *i64 = sys_mmap(32) as *i64 53 argv[0] = "_offc/nx_virtio_hs_emit.elf" as *u8 as i64 54 argv[1] = spec as i64 55 argv[2] = 0 56 let envp: *i64 = sys_mmap(16) as *i64 57 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 58 envp[1] = 0 59 sys_execve("_offc/nx_virtio_hs_emit.elf" as *u8, argv, envp) 60 sys_exit(127) 61 } 62 let st: *i64 = sys_mmap(16) as *i64 63 sys_wait4(pid, st, 0) 64 return st[0] 65} 66 67// run the SOVEREIGN rv64 emulator on binpath; serial -> outpath; return wait status 68func g_run_sov(binpath: *u8, outpath: *u8) -> i64 { 69 let pid: i64 = sys_fork() 70 if pid == 0 { 71 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 72 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 73 let argv: *i64 = sys_mmap(32) as *i64 74 argv[0] = "_offc/nx_boot_run_sov.elf" as *u8 as i64 75 argv[1] = binpath as i64 76 argv[2] = 0 77 let envp: *i64 = sys_mmap(16) as *i64 78 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 79 envp[1] = 0 80 sys_execve("_offc/nx_boot_run_sov.elf" as *u8, argv, envp) 81 sys_exit(127) 82 } 83 let st: *i64 = sys_mmap(16) as *i64 84 sys_wait4(pid, st, 0) 85 return st[0] 86} 87 88// run qemu-system-riscv64 virt + legacy virtio-blk-device (first) + virtio-net-device 89// (second) on binpath; serial -> outpath. The net device lands at qemu reverse slot 90// 0x10007000 (blk takes the top slot 0x10008000); the derived-base net image targets that 91// slot. The blk backing image must exist; the gate creates it first via g_make_backing. 92func g_run_qemu(binpath: *u8, outpath: *u8, backing: *u8) -> i64 { 93 let pid: i64 = sys_fork() 94 if pid == 0 { 95 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 96 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 97 let argv: *i64 = sys_mmap(128) as *i64 98 argv[0] = "/usr/bin/qemu-system-riscv64" as *u8 as i64 99 argv[1] = "-machine" as *u8 as i64 100 argv[2] = "virt" as *u8 as i64 101 argv[3] = "-global" as *u8 as i64 102 argv[4] = "virtio-mmio.force-legacy=true" as *u8 as i64 103 argv[5] = "-nographic" as *u8 as i64 104 argv[6] = "-bios" as *u8 as i64 105 argv[7] = binpath as i64 106 argv[8] = "-drive" as *u8 as i64 107 argv[9] = "file=/tmp/_vnetvqgate_backing.img,if=none,format=raw,id=hd0" as *u8 as i64 108 argv[10] = "-device" as *u8 as i64 109 argv[11] = "virtio-blk-device,drive=hd0" as *u8 as i64 110 argv[12] = "-device" as *u8 as i64 111 argv[13] = "virtio-net-device" as *u8 as i64 112 argv[14] = 0 113 let envp: *i64 = sys_mmap(16) as *i64 114 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 115 envp[1] = 0 116 sys_execve("/usr/bin/qemu-system-riscv64" as *u8, argv, envp) 117 sys_exit(127) 118 } 119 let st: *i64 = sys_mmap(16) as *i64 120 sys_wait4(pid, st, 0) 121 return st[0] 122} 123 124// create a small raw backing file for the qemu virtio-blk device (4 sectors of zeros). 125func g_make_backing(path: *u8) -> i64 { 126 let fd: i64 = sys_openat_wr(path, 0x1a4) 127 if fd < 0 { return 0 - 1 } 128 let z: *u8 = sys_mmap(2048) 129 var i: i64 = 0 130 while i < 2048 { z[i] = 0 as u8; i = i + 1 } 131 sys_write(fd, z, 2048) 132 sys_close(fd) 133 return 0 134} 135 136// read whole file into buf (cap-1 max); return byte count (0 if absent) 137func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 138 let fd: i64 = sys_openat_rd(path) 139 if fd < 0 { return 0 } 140 var n: i64 = 0 141 var go: i64 = 1 142 while go == 1 { let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap - 1 { go = 0 } } 143 sys_close(fd) 144 return n 145} 146 147// does buf[0,n) contain pat (length pl)? 1/0 148func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 149 if pl <= 0 { return 0 } 150 var i: i64 = 0 151 while i + pl <= n { 152 var k: i64 = 0 153 var hit: i64 = 1 154 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 155 if hit == 1 { return 1 } 156 i = i + 1 157 } 158 return 0 159} 160 161// read a little-endian 32-bit word from buf at byte offset o. 162func g_w32(buf: *u8, o: i64) -> i64 { 163 let b0: i64 = buf[o] as i64 164 let b1: i64 = buf[o+1] as i64 165 let b2: i64 = buf[o+2] as i64 166 let b3: i64 = buf[o+3] as i64 167 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 168} 169 170// find the byte offset of the (unique) QueuePFN read-back load word in the image; -1 if 171// absent. The QueuePFN-expected li the driver compares against is at off+4 (lui) / off+8 172// (addi); the addi's high immediate byte is at off+11. 173func g_find_qpfn_load(buf: *u8, n: i64) -> i64 { 174 var o: i64 = 0 175 while o + 4 <= n { 176 if g_w32(buf, o) == G_QPFN_LOAD_WORD { return o } 177 o = o + 4 178 } 179 return 0 - 1 180} 181 182func g_strlen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 183 184// does line [ls,le) of buf begin with key? 1/0 185func g_line_is(buf: *u8, ls: i64, le: i64, key: *u8) -> i64 { 186 var k: i64 = 0 187 while key[k] != (0 as u8) { 188 if ls + k >= le { return 0 } 189 if buf[ls + k] != key[k] { return 0 } 190 k = k + 1 191 } 192 return 1 193} 194 195// author the qemu-alignment spec: copy the main net spec, but replace the `base ` line value 196// with G_QEMU_BASE (the qemu net reverse-slot 0x10007000) and the `out ` line with the qemu 197// image path. Writes derived spec. 198func g_write_qemu_spec(mainspec: *u8, derived: *u8, qemu_out: *u8) -> i64 { 199 let buf: *u8 = sys_mmap(8192) 200 let n: i64 = g_read(mainspec, buf, 8192) 201 if n <= 0 { return 0 - 1 } 202 let ofd: i64 = sys_openat_wr(derived, 0x1a4) 203 if ofd < 0 { return 0 - 1 } 204 var ls: i64 = 0 205 while ls < n { 206 var le: i64 = ls 207 var scan: i64 = 1 208 while scan == 1 { if le >= n { scan = 0 } else { if buf[le] == (10 as u8) { scan = 0 } else { le = le + 1 } } } 209 if g_line_is(buf, ls, le, "base " as *u8) == 1 { 210 g_fp(ofd, "base 0x10007000\n" as *u8) 211 } else { 212 if g_line_is(buf, ls, le, "out " as *u8) == 1 { 213 g_fp(ofd, "out " as *u8); g_fp(ofd, qemu_out); g_fp(ofd, "\n" as *u8) 214 } else { 215 sys_write(ofd, (buf as i64 + ls) as *u8, le - ls) 216 g_fp(ofd, "\n" as *u8) 217 } 218 } 219 ls = le + 1 220 } 221 sys_close(ofd) 222 return 0 223} 224 225func main() -> i64 { 226 let spec: *u8 = "knowledge/specs/virtio_net_queuecfg_virt.spec" as *u8 227 let binpath: *u8 = "runtime/_hdl_build/_virtio_net_vqcfg_virt.bin" as *u8 228 let goldpath: *u8 = "runtime/_hdl_build/_virtio_net_vqcfg_virt.bin.gold" as *u8 229 let qemu_spec: *u8 = "/tmp/_vnetvqgate_qemu.spec" as *u8 230 let qemu_bin: *u8 = "/tmp/_vnetvqgate_qemu.bin" as *u8 231 let backing: *u8 = "/tmp/_vnetvqgate_backing.img" as *u8 232 let tamper_bin: *u8 = "/tmp/_vnetvqgate_tamper.bin" as *u8 233 let sov_serial: *u8 = "/tmp/_vnetvqgate_sov.txt" as *u8 234 let qemu_serial: *u8 = "/tmp/_vnetvqgate_qemu.txt" as *u8 235 let sov_tamper: *u8 = "/tmp/_vnetvqgate_sov_tamper.txt" as *u8 236 g_p("=== virtio-NET MMIO queue-config gate (K-R2-001c2: SOVEREIGN rv64 net virtqueue-config registers @0x10002000 + qemu virtio-net-device alignment @0x10007000) ===\n" as *u8) 237 238 let lfd: i64 = sys_openat_append("knowledge/status/virtio_net.log" as *u8, 0x1a4) 239 240 // STEP 1: author the SOVEREIGN net image (base 0x10002000) + the golden transcript. 241 let est: i64 = g_run_emit(spec) 242 if est != 0 { 243 g_p("NETVQCFGGATE verdict=RED reason=emit-failed\n" as *u8) 244 if lfd >= 0 { g_fp(lfd, "NETVQCFGGATE verdict=RED reason=emit-failed\n" as *u8); sys_close(lfd) } 245 sys_exit(1); return 1 246 } 247 let gold: *u8 = sys_mmap(512) 248 let gn: i64 = g_read(goldpath, gold, 512) 249 gold[gn] = 0 as u8 250 if gn <= 0 { 251 g_p("NETVQCFGGATE verdict=RED reason=golden-missing\n" as *u8) 252 if lfd >= 0 { g_fp(lfd, "NETVQCFGGATE verdict=RED reason=golden-missing\n" as *u8); sys_close(lfd) } 253 sys_exit(1); return 1 254 } 255 256 // STEP 2 (PRIMARY): the Nishi sovereign rv64 emulator RUNS the image -- net handshake + 257 // virtqueue config + QueuePFN read-back -> transcript must CONTAIN the golden. 258 let sst: i64 = g_run_sov(binpath, sov_serial) 259 let sbuf: *u8 = sys_mmap(65536) 260 let sbn: i64 = g_read(sov_serial, sbuf, 65536) 261 let trans_ok: i64 = g_buf_has(sbuf, sbn, gold, gn) 262 let halt_ok: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 263 var sov_ok: i64 = 0 264 if sst == 0 { if trans_ok == 1 { if halt_ok == 1 { sov_ok = 1 } } } 265 266 // STEP 3 (ALIGNMENT): author the qemu-base net image (slot 0x10007000) + run qemu with a 267 // REAL legacy virtio-blk-device (first) + virtio-net-device (second); assert the SAME 268 // golden appears (QueuePFN read-back is genuinely RW on the real net transport, so the 269 // driver's verify passes there too). 270 g_make_backing(backing) 271 g_write_qemu_spec(spec, qemu_spec, qemu_bin) 272 let qest: i64 = g_run_emit(qemu_spec) 273 var align: i64 = 0 274 if qest == 0 { 275 let qst: i64 = g_run_qemu(qemu_bin, qemu_serial, backing) 276 let qbuf: *u8 = sys_mmap(65536) 277 let qbn: i64 = g_read(qemu_serial, qbuf, 65536) 278 let qtrans: i64 = g_buf_has(qbuf, qbn, gold, gn) 279 if qst == 0 { if qtrans == 1 { align = 1 } } 280 } 281 282 // STEP 4 (TAMPER): corrupt the QueuePFN-EXPECTED constant in the sovereign image. Scan 283 // for the unique QueuePFN read-back load word; the expected li the driver compares 284 // against is the addi at load+8. Bump that addi's high immediate byte (load+11) so the 285 // expected != the value the driver actually wrote+read-back -> the read-back verify 286 // branches to the finisher -> ONLY the " VQ" canary drops -> gate MUST go RED. 287 let ibuf: *u8 = sys_mmap(8192) 288 let ibn: i64 = g_read(binpath, ibuf, 8192) 289 let lpos: i64 = g_find_qpfn_load(ibuf, ibn) 290 var tamper_built: i64 = 0 291 if lpos >= 0 { 292 let ebyte: i64 = lpos + 11 // high immediate byte of the expected addi 293 ibuf[ebyte] = (ibuf[ebyte] + 1) as u8 294 let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4) 295 if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd); tamper_built = 1 } 296 } 297 var tamper_bites: i64 = 0 298 if tamper_built == 1 { 299 let tst: i64 = g_run_sov(tamper_bin, sov_tamper) 300 let tbuf: *u8 = sys_mmap(65536) 301 let tbn: i64 = g_read(sov_tamper, tbuf, 65536) 302 let tamper_trans: i64 = g_buf_has(tbuf, tbn, gold, gn) // golden should now MISS 303 if tamper_trans == 0 { tamper_bites = 1 } 304 } 305 306 g_p(" sovereign_emu=" as *u8) 307 if sov_ok == 1 { g_p("GREEN(transcript==golden+clean-halt)" as *u8) } else { g_p("RED" as *u8) } 308 g_p(" qemu_align=" as *u8) 309 if align == 1 { g_p("yes(real-virtio-net @0x10007000, QueuePFN read-back)" as *u8) } else { g_p("no" as *u8) } 310 g_p(" tamper_bites=" as *u8) 311 if tamper_bites == 1 { g_p("yes(QueuePFN-expected corrupt -> VQ drops)\n" as *u8) } else { g_p("no\n" as *u8) } 312 313 var pass: i64 = 0 314 if sov_ok == 1 { if align == 1 { if tamper_bites == 1 { pass = 1 } } } 315 316 if pass == 1 { 317 g_p("NETVQCFGGATE verdict=GREEN (sovereign rv64 emu drove the virtio-NET virtqueue-config layer @0x10002000; QueueSel/QueueNumMax/QueueNum/QueuePFN/QueueNotify; QueuePFN read-back verified; transcript==golden; clean halt; qemu virtio-net-device cross-check @0x10007000 AGREES; QueuePFN tamper REJECTED; blk @0x10001000 untouched)\n" as *u8) 318 if lfd >= 0 { 319 g_fp(lfd, "NETVQCFGGATE verdict=GREEN runtime=sovereign-emu transport=legacy-virtio-mmio device=virtio-net device-id=1 net_base=0x10002000 layer=queue-config queues=QueueSel|QueueNumMax|QueueNum|QueueAlign|QueuePFN|QueueNotify queuepfn-readback=verified transcript==golden align_qemu=yes(virtio-net-device@0x10007000) tamper=rejected blk=untouched golden=" as *u8) 320 g_fp(lfd, gold) 321 g_fp(lfd, " epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8); sys_close(lfd) 322 } 323 sys_exit(0); return 0 324 } 325 g_p("NETVQCFGGATE verdict=RED (sov_ok/align/tamper not all green)\n" as *u8) 326 if lfd >= 0 { 327 g_fp(lfd, "NETVQCFGGATE verdict=RED sov_ok=" as *u8); g_fn(lfd, sov_ok) 328 g_fp(lfd, " align=" as *u8); g_fn(lfd, align) 329 g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites); g_fp(lfd, "\n" as *u8); sys_close(lfd) 330 } 331 sys_exit(1) 332 return 1 333}