_k_r2_001b2b_gate.nx source

1// _k_r2_001b2b_gate.nx -- the K-R2-001b2b gate (virtio-MMIO AVAIL-CONSUME + USED-RING 2// WRITEBACK layer; the third slice of the K-R2-001b virtqueue epic, on top of b2a's 3// descriptor-DMA). Drives the full author->handshake->queue-config->descriptor-DMA-> 4// avail/used chain with NO mocks: runs the REAL nx_virtio_hs_emit (the team AUTHORS the 5// rv64 image + the TABLE-COMPUTED golden transcript from the avail/used spec), then RUNS 6// the image on the SOVEREIGN rv64 emulator (rv64im_min_sim + the rv64im_min_virtio device 7// now, on the SECOND QueueNotify kick, reading the avail ring head, walking the descriptor 8// (b2a DMA), WRITING the used ring (used.ring[0].id/.len) + BUMPING used.idx back into guest 9// RAM, and latching used.idx into the QueueUsedIdxPeek RO register -- the PRIMARY, gating 10// lane: Nishi owns the runtime) and asserts the captured serial transcript CONTAINS the 11// emitter's golden ("VIO ACK DRV FEAT OK VQ DESC USED\n" -- after the descriptor-DMA the 12// driver published the avail ring, kicked QueueNotify, the device consumed it + wrote the 13// used ring, then the driver READ QueueUsedIdxPeek BACK and verified it == used_idx_expected: 14// the used-ring writeback binding proof) AND the sovereign emu reports a clean SiFive- 15// finisher halt. 16// 17// Then the ALIGNMENT lane: qemu-system-riscv64 -machine virt -global 18// virtio-mmio.force-legacy=true with a REAL virtio-blk-device backing. The gate authors a 19// SECOND image from a base-rewritten spec (the blk device lands at slot 0x10008000) and runs 20// the SAME driver against the REAL legacy virtio-blk transport: it completes the handshake + 21// queue config, lays the SAME descriptor + the SAME avail ring into qemu guest RAM, and kicks 22// the real QueueNotify -- the real legacy transport genuinely walks the ring. The 23// QueueUsedIdxPeek result register is a sovereign-model instrument the real device does not 24// expose (it reads 0), so on qemu the used-ring read-back verify gracefully drops ONLY 25// " USED" (and the sovereign-only QueueDescPeek already drops " DESC"); the gate asserts the 26// qemu transcript contains the b1 prefix golden ("VIO ACK DRV FEAT OK VQ") -- proving the 27// SAME driver lays the avail ring + kicks the real device -> lanes AGREE on every register 28// the real transport can observe. 29// 30// Finally a TAMPER test: corrupt the QueueUsedIdxPeek-EXPECTED constant in the sovereign 31// image (the driver loads its own QueueUsedIdxPeek read-back into t3 via lw and compares 32// against this li-loaded expected in t4; bumping the expected's immediate makes t3 != t4) -> 33// the read-back verify branches PAST stage 7 straight to the finisher -> the transcript loses 34// ONLY its " USED" canary (the "VIO ACK DRV FEAT OK VQ DESC" tail survives) -> the gate MUST 35// go RED. Evidence -> knowledge/status/virtio_blk.log (USEDGATE row; the queue row's ||MARK= 36// reads it). Sovereign orchestration (fork/dup3/execve/wait4). license_tier: ORIGINAL 37import "nx_syscalls.nx" 38 39// the unique rv64 encoding of `lw t3, 0x64(t2)` -- the QueueUsedIdxPeek read-back load (f3=2, 40// sign-extend; used.idx is a small non-negative int). The UsedIdxPeek-expected constant the 41// driver compares against is the li that follows it (lui at +4, addi at +8); corrupting the 42// addi's high immediate byte (+11) is the avail/used tamper. 43const G_QUSEDIDXPEEK_LOAD_WORD: i64 = 0x0643ae03 // lw t3, 0x064(t2) (QueueUsedIdxPeek read-back) 44 45func 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 } 46func 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 } 47func 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 } 48 49// run nx_virtio_hs_emit <spec>; return child wait status (0 = ok) 50func g_run_emit(spec: *u8) -> i64 { 51 let pid: i64 = sys_fork() 52 if pid == 0 { 53 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4) 54 if dn >= 0 { sys_dup3(dn, 1, 0) } 55 let argv: *i64 = sys_mmap(32) as *i64 56 argv[0] = "_offc/nx_virtio_hs_emit.elf" as *u8 as i64 57 argv[1] = spec as i64 58 argv[2] = 0 59 let envp: *i64 = sys_mmap(16) as *i64 60 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 61 envp[1] = 0 62 sys_execve("_offc/nx_virtio_hs_emit.elf" as *u8, argv, envp) 63 sys_exit(127) 64 } 65 let st: *i64 = sys_mmap(16) as *i64 66 sys_wait4(pid, st, 0) 67 return st[0] 68} 69 70// run the SOVEREIGN rv64 emulator on binpath; serial -> outpath; return wait status 71func g_run_sov(binpath: *u8, outpath: *u8) -> i64 { 72 let pid: i64 = sys_fork() 73 if pid == 0 { 74 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 75 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 76 let argv: *i64 = sys_mmap(32) as *i64 77 argv[0] = "_offc/nx_boot_run_sov.elf" as *u8 as i64 78 argv[1] = binpath as i64 79 argv[2] = 0 80 let envp: *i64 = sys_mmap(16) as *i64 81 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 82 envp[1] = 0 83 sys_execve("_offc/nx_boot_run_sov.elf" as *u8, argv, envp) 84 sys_exit(127) 85 } 86 let st: *i64 = sys_mmap(16) as *i64 87 sys_wait4(pid, st, 0) 88 return st[0] 89} 90 91// run qemu-system-riscv64 virt + legacy virtio-blk-device on binpath; serial -> outpath. 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/_usedgate_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] = 0 111 let envp: *i64 = sys_mmap(16) as *i64 112 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64 113 envp[1] = 0 114 sys_execve("/usr/bin/qemu-system-riscv64" as *u8, argv, envp) 115 sys_exit(127) 116 } 117 let st: *i64 = sys_mmap(16) as *i64 118 sys_wait4(pid, st, 0) 119 return st[0] 120} 121 122// create a small raw backing file for the qemu virtio-blk device (4 sectors of zeros). 123func g_make_backing(path: *u8) -> i64 { 124 let fd: i64 = sys_openat_wr(path, 0x1a4) 125 if fd < 0 { return 0 - 1 } 126 let z: *u8 = sys_mmap(2048) 127 var i: i64 = 0 128 while i < 2048 { z[i] = 0 as u8; i = i + 1 } 129 sys_write(fd, z, 2048) 130 sys_close(fd) 131 return 0 132} 133 134// read whole file into buf (cap-1 max); return byte count (0 if absent) 135func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 136 let fd: i64 = sys_openat_rd(path) 137 if fd < 0 { return 0 } 138 var n: i64 = 0 139 var go: i64 = 1 140 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 } } 141 sys_close(fd) 142 return n 143} 144 145// does buf[0,n) contain pat (length pl)? 1/0 146func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 147 if pl <= 0 { return 0 } 148 var i: i64 = 0 149 while i + pl <= n { 150 var k: i64 = 0 151 var hit: i64 = 1 152 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 153 if hit == 1 { return 1 } 154 i = i + 1 155 } 156 return 0 157} 158 159// read a little-endian 32-bit word from buf at byte offset o. 160func g_w32(buf: *u8, o: i64) -> i64 { 161 let b0: i64 = buf[o] as i64 162 let b1: i64 = buf[o+1] as i64 163 let b2: i64 = buf[o+2] as i64 164 let b3: i64 = buf[o+3] as i64 165 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 166} 167 168// find the byte offset of the (unique) QueueUsedIdxPeek read-back load word in the image; -1 169// if absent. The UsedIdxPeek-expected li the driver compares against is at off+4 (lui) / 170// off+8 (addi); the addi's high immediate byte is at off+11. 171func g_find_usedidxpeek_load(buf: *u8, n: i64) -> i64 { 172 var o: i64 = 0 173 while o + 4 <= n { 174 if g_w32(buf, o) == G_QUSEDIDXPEEK_LOAD_WORD { return o } 175 o = o + 4 176 } 177 return 0 - 1 178} 179 180func g_strlen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 181 182// does line [ls,le) of buf begin with key? 1/0 183func g_line_is(buf: *u8, ls: i64, le: i64, key: *u8) -> i64 { 184 var k: i64 = 0 185 while key[k] != (0 as u8) { 186 if ls + k >= le { return 0 } 187 if buf[ls + k] != key[k] { return 0 } 188 k = k + 1 189 } 190 return 1 191} 192 193// author the qemu-alignment spec: copy the main spec, but replace the `base ` line value 194// with the qemu blk slot and the `out ` line with the qemu image path. (The ring page + 195// data buffer addresses are guest-RAM addresses valid on both lanes -- left as is.) 196func g_write_qemu_spec(mainspec: *u8, derived: *u8, qemu_out: *u8) -> i64 { 197 let buf: *u8 = sys_mmap(8192) 198 let n: i64 = g_read(mainspec, buf, 8192) 199 if n <= 0 { return 0 - 1 } 200 let ofd: i64 = sys_openat_wr(derived, 0x1a4) 201 if ofd < 0 { return 0 - 1 } 202 var ls: i64 = 0 203 while ls < n { 204 var le: i64 = ls 205 var scan: i64 = 1 206 while scan == 1 { if le >= n { scan = 0 } else { if buf[le] == (10 as u8) { scan = 0 } else { le = le + 1 } } } 207 if g_line_is(buf, ls, le, "base " as *u8) == 1 { 208 g_fp(ofd, "base 0x10008000\n" as *u8) 209 } else { 210 if g_line_is(buf, ls, le, "out " as *u8) == 1 { 211 g_fp(ofd, "out " as *u8); g_fp(ofd, qemu_out); g_fp(ofd, "\n" as *u8) 212 } else { 213 sys_write(ofd, (buf as i64 + ls) as *u8, le - ls) 214 g_fp(ofd, "\n" as *u8) 215 } 216 } 217 ls = le + 1 218 } 219 sys_close(ofd) 220 return 0 221} 222 223func main() -> i64 { 224 let spec: *u8 = "knowledge/specs/virtio_blk_availused_virt.spec" as *u8 225 let binpath: *u8 = "runtime/_hdl_build/_virtio_availused_virt.bin" as *u8 226 let goldpath: *u8 = "runtime/_hdl_build/_virtio_availused_virt.bin.gold" as *u8 227 let qemu_spec: *u8 = "/tmp/_usedgate_qemu.spec" as *u8 228 let qemu_bin: *u8 = "/tmp/_usedgate_qemu.bin" as *u8 229 let backing: *u8 = "/tmp/_usedgate_backing.img" as *u8 230 let tamper_bin: *u8 = "/tmp/_usedgate_tamper.bin" as *u8 231 let sov_serial: *u8 = "/tmp/_usedgate_sov.txt" as *u8 232 let qemu_serial: *u8 = "/tmp/_usedgate_qemu.txt" as *u8 233 let sov_tamper: *u8 = "/tmp/_usedgate_sov_tamper.txt" as *u8 234 // the b2a prefix golden the qemu alignment lane asserts (the real device has neither 235 // QueueDescPeek nor QueueUsedIdxPeek, so on qemu the descriptor-DMA + used-ring verifies 236 // drop " DESC" and " USED", leaving the b1 prefix the real transport can observe). 237 let prefix_gold: *u8 = "VIO ACK DRV FEAT OK VQ" as *u8 238 // the b2a "DESC" tail the tamper must KEEP (only " USED" drops under the used-idx tamper). 239 let desconly_gold: *u8 = "VIO ACK DRV FEAT OK VQ DESC" as *u8 240 g_p("=== virtio-MMIO avail/used gate (K-R2-001b2b: SOVEREIGN rv64 avail-ring publish + device used-ring writeback + QueueUsedIdxPeek read-back + qemu virtio-blk alignment) ===\n" as *u8) 241 242 let lfd: i64 = sys_openat_append("knowledge/status/virtio_blk.log" as *u8, 0x1a4) 243 244 // STEP 1: author the SOVEREIGN image (base 0x10001000) + the golden transcript. 245 let est: i64 = g_run_emit(spec) 246 if est != 0 { 247 g_p("USEDGATE verdict=RED reason=emit-failed\n" as *u8) 248 if lfd >= 0 { g_fp(lfd, "USEDGATE verdict=RED reason=emit-failed\n" as *u8); sys_close(lfd) } 249 sys_exit(1); return 1 250 } 251 let gold: *u8 = sys_mmap(512) 252 let gn: i64 = g_read(goldpath, gold, 512) 253 gold[gn] = 0 as u8 254 if gn <= 0 { 255 g_p("USEDGATE verdict=RED reason=golden-missing\n" as *u8) 256 if lfd >= 0 { g_fp(lfd, "USEDGATE verdict=RED reason=golden-missing\n" as *u8); sys_close(lfd) } 257 sys_exit(1); return 1 258 } 259 260 // STEP 2 (PRIMARY): the Nishi sovereign rv64 emulator RUNS the image -- handshake + queue 261 // config + descriptor lay (b2a) + avail-ring publish + QueueNotify kick + device consume + 262 // used-ring writeback + QueueUsedIdxPeek read-back verify -> transcript must CONTAIN the 263 // full golden ("...DESC USED\n"). 264 let sst: i64 = g_run_sov(binpath, sov_serial) 265 let sbuf: *u8 = sys_mmap(65536) 266 let sbn: i64 = g_read(sov_serial, sbuf, 65536) 267 let trans_ok: i64 = g_buf_has(sbuf, sbn, gold, gn) 268 let halt_ok: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 269 var sov_ok: i64 = 0 270 if sst == 0 { if trans_ok == 1 { if halt_ok == 1 { sov_ok = 1 } } } 271 272 // STEP 3 (ALIGNMENT): author the qemu-base image (slot 0x10008000) + run qemu with a REAL 273 // legacy virtio-blk-device; the SAME driver lays the SAME descriptor + the SAME avail ring 274 // into qemu guest RAM and kicks the real QueueNotify (the real transport walks the ring). 275 // The sovereign-only QueueDescPeek/QueueUsedIdxPeek registers read 0 on the real device, so 276 // the descriptor-DMA + used-ring verifies drop " DESC"/" USED" there; assert the b1 prefix 277 // golden ("VIO ACK DRV FEAT OK VQ") appears, proving the driver runs identically against 278 // the real transport up to the avail publish + kick. 279 g_make_backing(backing) 280 g_write_qemu_spec(spec, qemu_spec, qemu_bin) 281 let qest: i64 = g_run_emit(qemu_spec) 282 var align: i64 = 0 283 if qest == 0 { 284 let qst: i64 = g_run_qemu(qemu_bin, qemu_serial, backing) 285 let qbuf: *u8 = sys_mmap(65536) 286 let qbn: i64 = g_read(qemu_serial, qbuf, 65536) 287 let qtrans: i64 = g_buf_has(qbuf, qbn, prefix_gold, g_strlen(prefix_gold)) 288 if qst == 0 { if qtrans == 1 { align = 1 } } 289 } 290 291 // STEP 4 (TAMPER): corrupt the QueueUsedIdxPeek-EXPECTED constant in the sovereign image. 292 // Scan for the unique QueueUsedIdxPeek read-back load word; the expected li the driver 293 // compares against is the addi at load+8. Bump that addi's high immediate byte (load+11) 294 // so the expected != the value the device latched -> the read-back verify branches to the 295 // finisher -> ONLY the " USED" canary drops (the "...DESC" tail survives) -> gate MUST RED. 296 let ibuf: *u8 = sys_mmap(8192) 297 let ibn: i64 = g_read(binpath, ibuf, 8192) 298 let lpos: i64 = g_find_usedidxpeek_load(ibuf, ibn) 299 var tamper_built: i64 = 0 300 if lpos >= 0 { 301 let ebyte: i64 = lpos + 11 // high immediate byte of the expected addi 302 ibuf[ebyte] = (ibuf[ebyte] + 1) as u8 303 let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4) 304 if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd); tamper_built = 1 } 305 } 306 var tamper_bites: i64 = 0 307 var tamper_keeps_desc: i64 = 0 308 if tamper_built == 1 { 309 let tst: i64 = g_run_sov(tamper_bin, sov_tamper) 310 let tbuf: *u8 = sys_mmap(65536) 311 let tbn: i64 = g_read(sov_tamper, tbuf, 65536) 312 let tamper_trans: i64 = g_buf_has(tbuf, tbn, gold, gn) // full golden should now MISS 313 let tamper_desc: i64 = g_buf_has(tbuf, tbn, desconly_gold, g_strlen(desconly_gold)) // DESC tail survives 314 if tamper_trans == 0 { tamper_bites = 1 } 315 if tamper_desc == 1 { tamper_keeps_desc = 1 } 316 } 317 318 g_p(" sovereign_emu=" as *u8) 319 if sov_ok == 1 { g_p("GREEN(transcript==golden+clean-halt)" as *u8) } else { g_p("RED" as *u8) } 320 g_p(" qemu_align=" as *u8) 321 if align == 1 { g_p("yes(real-virtio-blk @0x10008000, same descriptor+avail laid + real kick, VQ prefix)" as *u8) } else { g_p("no" as *u8) } 322 g_p(" tamper_bites=" as *u8) 323 if tamper_bites == 1 { g_p("yes(UsedIdxPeek-expected corrupt -> USED drops, DESC survives)\n" as *u8) } else { g_p("no\n" as *u8) } 324 325 var pass: i64 = 0 326 if sov_ok == 1 { if align == 1 { if tamper_bites == 1 { if tamper_keeps_desc == 1 { pass = 1 } } } } 327 328 if pass == 1 { 329 g_p("USEDGATE verdict=GREEN (sovereign rv64 emu drove the avail/used layer; avail ring published at the QueuePFN-bound ring page; QueueNotify kicked; device consumed the avail head, walked the descriptor, wrote the used ring + bumped used.idx in guest RAM; QueueUsedIdxPeek read-back verified == used_idx_expected; transcript==golden; clean halt; qemu virtio-blk-device cross-check lays the SAME descriptor+avail + kicks the real transport AGREEING on the VQ prefix; UsedIdxPeek tamper REJECTED -- USED drops, DESC survives)\n" as *u8) 330 if lfd >= 0 { 331 g_fp(lfd, "USEDGATE verdict=GREEN runtime=sovereign-emu transport=legacy-virtio-mmio layer=avail-used avail=ring[head]|idx used=ring[id|len]|idx ring=QueuePFN<<12 kick=QueueNotify dma=device-consume+writeback usedidxpeek-readback=verified transcript==golden align_qemu=yes(virtio-blk-device,VQ-prefix) tamper=rejected(USED-drops,DESC-survives) golden=" as *u8) 332 g_fp(lfd, gold) 333 g_fp(lfd, " epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8); sys_close(lfd) 334 } 335 sys_exit(0); return 0 336 } 337 g_p("USEDGATE verdict=RED (sov_ok/align/tamper not all green)\n" as *u8) 338 if lfd >= 0 { 339 g_fp(lfd, "USEDGATE verdict=RED sov_ok=" as *u8); g_fn(lfd, sov_ok) 340 g_fp(lfd, " align=" as *u8); g_fn(lfd, align) 341 g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites) 342 g_fp(lfd, " tamper_keeps_desc=" as *u8); g_fn(lfd, tamper_keeps_desc); g_fp(lfd, "\n" as *u8); sys_close(lfd) 343 } 344 sys_exit(1) 345 return 1 346}