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}