code wiki / _hdl_build / _memalloc_gate.nx

_memalloc_gate.nx source

↩ module page · 106 lines · 5595 B

1// _memalloc_gate.nx -- gate for the kernel MEMORY-ALLOCATOR slice (bump alloc + store/load 2// round-trip). NO mocks: runs the REAL nx_memalloc_emit, RUNS the image on the SOVEREIGN rv64 emu, 3// asserts the serial CONTAINS the table-computed golden "MK" (every alloc round-tripped + a2 4// distinct from a1) + clean finisher halt. TAMPER: corrupt the value stored at a1 -> the lbu 5// read-back no longer matches the expected byte -> the KAT emits 'X' not 'MK' -> gate MUST go RED 6// (proves the load REALLY read what the store wrote). Evidence -> knowledge/status/memalloc.log. 7// license_tier: ORIGINAL 8import "nx_syscalls.nx" 9 10func 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 } 11func 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 } 12func 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 } 13 14func g_run1(prog: *u8, arg1: *u8, outpath: *u8) -> i64 { 15 let pid: i64 = sys_fork() 16 if pid == 0 { 17 if outpath != (0 as *u8) { let ofd: i64 = sys_openat_wr(outpath, 0x1a4); if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } } 18 else { let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4); if dn >= 0 { sys_dup3(dn, 1, 0) } } 19 let argv: *i64 = sys_mmap(32) as *i64 20 argv[0] = prog as i64 21 if arg1 != (0 as *u8) { argv[1] = arg1 as i64; argv[2] = 0 } else { argv[1] = 0 } 22 let envp: *i64 = sys_mmap(16) as *i64 23 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 24 sys_execve(prog, argv, envp) 25 sys_exit(127) 26 } 27 let st: *i64 = sys_mmap(16) as *i64 28 sys_wait4(pid, st, 0) 29 return st[0] 30} 31 32func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 33 let fd: i64 = sys_openat_rd(path) 34 if fd < 0 { return 0 } 35 var n: i64 = 0 36 var go: i64 = 1 37 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 } } 38 sys_close(fd) 39 return n 40} 41 42func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 43 if pl <= 0 { return 0 } 44 var i: i64 = 0 45 while i + pl <= n { 46 var k: i64 = 0 47 var hit: i64 = 1 48 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 49 if hit == 1 { return 1 } 50 i = i + 1 51 } 52 return 0 53} 54 55func main() -> i64 { 56 let binpath: *u8 = "runtime/_hdl_build/_memalloc_virt.bin" as *u8 57 let goldpath: *u8 = "runtime/_hdl_build/_memalloc_virt.bin.gold" as *u8 58 let tamper_bin: *u8 = "/tmp/_memgate_tamper.bin" as *u8 59 let sov_serial: *u8 = "/tmp/_memgate_sov.txt" as *u8 60 let sov_tamper: *u8 = "/tmp/_memgate_tamper.txt" as *u8 61 g_p("=== memory-allocator gate (bump alloc + store/load round-trip: SOVEREIGN rv64 emu + tamper) ===\n" as *u8) 62 let lfd: i64 = sys_openat_append("knowledge/status/memalloc.log" as *u8, 0x1a4) 63 64 let est: i64 = g_run1("/tmp/nx_memalloc_emit.sov.elf" as *u8, 0 as *u8, 0 as *u8) 65 if est != 0 { g_p("MEMALLOCGATE verdict=RED reason=emit-failed\n" as *u8); if lfd>=0 { g_fp(lfd,"MEMALLOCGATE verdict=RED reason=emit-failed\n" as *u8); sys_close(lfd) } sys_exit(1); return 1 } 66 let gold: *u8 = sys_mmap(16) 67 let gn: i64 = g_read(goldpath, gold, 16) 68 69 let sst: i64 = g_run1("_offc/nx_boot_run_sov.elf" as *u8, binpath, sov_serial) 70 let sbuf: *u8 = sys_mmap(65536) 71 let sbn: i64 = g_read(sov_serial, sbuf, 65536) 72 let trans_ok: i64 = g_buf_has(sbuf, sbn, gold, gn) 73 let halt_ok: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 74 var sov_ok: i64 = 0 75 if sst == 0 { if trans_ok == 1 { if halt_ok == 1 { sov_ok = 1 } } } 76 77 // TAMPER: corrupt the value stored at a1 (addi t1,x0,0xAA at byte 12; imm high byte 15). 78 let ibuf: *u8 = sys_mmap(8192) 79 let ibn: i64 = g_read(binpath, ibuf, 8192) 80 ibuf[12 + 3] = (ibuf[12 + 3] + 1) as u8 81 let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4) 82 if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd) } 83 let tst: i64 = g_run1("_offc/nx_boot_run_sov.elf" as *u8, tamper_bin, sov_tamper) 84 let tbuf: *u8 = sys_mmap(65536) 85 let tbn: i64 = g_read(sov_tamper, tbuf, 65536) 86 let tamper_trans: i64 = g_buf_has(tbuf, tbn, gold, gn) 87 var tamper_bites: i64 = 0 88 if tamper_trans == 0 { tamper_bites = 1 } 89 90 g_p(" sovereign_emu=" as *u8) 91 if sov_ok == 1 { g_p("GREEN(serial-contains-MK+clean-halt)" as *u8) } else { g_p("RED" as *u8) } 92 g_p(" tamper_bites=" as *u8) 93 if tamper_bites == 1 { g_p("yes\n" as *u8) } else { g_p("no\n" as *u8) } 94 95 var pass: i64 = 0 96 if sov_ok == 1 { if tamper_bites == 1 { pass = 1 } } 97 if pass == 1 { 98 g_p("MEMALLOCGATE verdict=GREEN (sovereign rv64 emu: bump-alloc + memory store/load round-trip verified; tamper REJECTED)\n" as *u8) 99 if lfd >= 0 { g_fp(lfd, "MEMALLOCGATE verdict=GREEN runtime=sovereign-emu mem=alloc-store-load-roundtrip distinct-allocs=yes tamper=rejected epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8); sys_close(lfd) } 100 sys_exit(0); return 0 101 } 102 g_p("MEMALLOCGATE verdict=RED (sov_ok/tamper not both green)\n" as *u8) 103 if lfd >= 0 { g_fp(lfd, "MEMALLOCGATE verdict=RED sov_ok=" as *u8); g_fn(lfd, sov_ok); g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites); g_fp(lfd, "\n" as *u8); sys_close(lfd) } 104 sys_exit(1) 105 return 1 106}