_perm_gate.nx source

1// _perm_gate.nx -- LOCK for Sv39 PAGE-PERMISSION enforcement (X-PAGE-PERM-001). NO mocks. 2// Proves the CPU enforces the leaf PTE permission bits PER ACCESS TYPE (riscv-priv-spec): a fetch needs 3// X (the NX-bit / W^X foundation: a data page is NOT executable), a load needs R. Each axis is proven 4// with a SINGLE-BIT-DIFFERENCE control so the gate shows the *specific* bit is enforced, not just "any 5// fault". Drives the already-param-able emits (nx_ifetch_emit code-PTE arg, nx_paging_emit data-PTE arg) 6// on the sovereign emu -- no new image emitter needed. 7// T1 fetch-needs-X : code page V|R|W (0x..07, NO X) -> the FETCH of the virtual PC raises an 8// instruction-page-fault -> handler "IPF", and "IOK" never prints. 9// T2 fetch-X-control: code page V|R|W|X (0x..0F) -> fetch succeeds -> "IOK". (only the X bit differs) 10// T3 load-needs-R : data page V|W|X (0x..0D, NO R) -> the LOAD faults -> "VOK" never prints. 11// T4 load-R-control: data page V|R|W|X (0x..0F) -> load succeeds -> "VOK". (only the R bit differs) 12// GREEN only if T1..T4 hold. Evidence -> knowledge/status/paging.log (PERMGATE). license_tier: ORIGINAL 13import "nx_syscalls.nx" 14 15const PM_IFEMIT: *u8 = "_offc/nx_ifetch_emit.elf" 16const PM_PGEMIT: *u8 = "_offc/nx_paging_emit.elf" 17const PM_SOV: *u8 = "_offc/nx_boot_run_sov.elf" 18 19func 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 } 20func 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 } 21func 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 } 22 23func g_run(prog: *u8, a1: *u8, a2: *u8, outpath: *u8) -> i64 { 24 let pid: i64 = sys_fork() 25 if pid == 0 { 26 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) } } 27 let argv: *i64 = sys_mmap(32) as *i64 28 argv[0] = prog as i64 29 var k: i64 = 1 30 if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 } 31 if a2 != (0 as *u8) { argv[k] = a2 as i64; k = k + 1 } 32 argv[k] = 0 33 let envp: *i64 = sys_mmap(16) as *i64 34 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 35 sys_execve(prog, argv, envp) 36 sys_exit(127) 37 } 38 let st: *i64 = sys_mmap(16) as *i64 39 sys_wait4(pid, st, 0) 40 return (st[0] >> 8) & 0xff 41} 42func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 43 let fd: i64 = sys_openat_rd(path) 44 if fd < 0 { return 0 } 45 var n: i64 = 0 46 var go: i64 = 1 47 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 } } 48 sys_close(fd) 49 return n 50} 51func g_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 52 if pl <= 0 { return 0 } 53 var i: i64 = 0 54 while i + pl <= n { var k: i64=0; var hit: i64=1; while k<pl { if buf[i+k]!=pat[k]{hit=0;k=pl}else{k=k+1} } if hit==1 { return 1 } i=i+1 } 55 return 0 56} 57// run emit(value->binpath) then the emu(binpath->txt); return bytes read of the emu serial into buf. 58func g_emit_run(emit: *u8, val: *u8, binp: *u8, txt: *u8, buf: *u8) -> i64 { 59 g_run(emit, val, binp, "/tmp/_pm_emit.out" as *u8) 60 g_run(PM_SOV, binp, 0 as *u8, txt) 61 return g_read(txt, buf, 65536) 62} 63func g_row(name: *u8, pass: i64) -> i64 { g_p(" " as *u8); g_p(name); if pass==1 { g_p(" PASS\n" as *u8) } else { g_p(" FAIL\n" as *u8) } return 0 } 64 65func main() -> i64 { 66 let b: *u8 = sys_mmap(65536) 67 68 // T1 fetch-needs-X: code page V|R|W (NO X) -> instruction-page-fault -> IPF, no IOK 69 var n: i64 = g_emit_run(PM_IFEMIT, "0x20000007" as *u8, "/tmp/_pm_nox.bin" as *u8, "/tmp/_pm_nox.txt" as *u8, b) 70 var t1: i64 = 0 71 if g_has(b, n, "IPF" as *u8, 3) == 1 { if g_has(b, n, "IOK" as *u8, 3) == 0 { t1 = 1 } } 72 73 // T2 fetch-X-control: only the X bit added -> IOK 74 n = g_emit_run(PM_IFEMIT, "0x2000000F" as *u8, "/tmp/_pm_x.bin" as *u8, "/tmp/_pm_x.txt" as *u8, b) 75 var t2: i64 = 0 76 if g_has(b, n, "IOK" as *u8, 3) == 1 { if g_has(b, n, "BOOTSOV verdict=GREEN" as *u8, 21) == 1 { t2 = 1 } } 77 78 // T3 load-needs-R: data page V|W|X (NO R) -> load-page-fault -> VOK never prints 79 n = g_emit_run(PM_PGEMIT, "0x2000000D" as *u8, "/tmp/_pm_nor.bin" as *u8, "/tmp/_pm_nor.txt" as *u8, b) 80 var t3: i64 = 0 81 if g_has(b, n, "VOK" as *u8, 3) == 0 { t3 = 1 } 82 83 // T4 load-R-control: only the R bit added -> VOK 84 n = g_emit_run(PM_PGEMIT, "0x2000000F" as *u8, "/tmp/_pm_r.bin" as *u8, "/tmp/_pm_r.txt" as *u8, b) 85 var t4: i64 = 0 86 if g_has(b, n, "VOK" as *u8, 3) == 1 { t4 = 1 } 87 88 var passes: i64 = 0 89 if t1==1 { passes=passes+1 } 90 if t2==1 { passes=passes+1 } 91 if t3==1 { passes=passes+1 } 92 if t4==1 { passes=passes+1 } 93 var ok: i64 = 0 94 if passes == 4 { ok = 1 } 95 96 g_p("PERM gate (Sv39 per-access permission enforcement: X-on-fetch / R-on-load)\n" as *u8) 97 g_row("T1 fetch-needs-X (no-X->IPF)" as *u8, t1) 98 g_row("T2 fetch-X-control (->IOK) " as *u8, t2) 99 g_row("T3 load-needs-R (no-R->!VOK)" as *u8, t3) 100 g_row("T4 load-R-control (->VOK) " as *u8, t4) 101 102 let lf: i64 = sys_openat_append("knowledge/status/paging.log" as *u8, 0x1a4) 103 if ok == 1 { 104 g_p("PERMGATE verdict=GREEN keystone=sv39-page-permission-enforcement probe=page-perm X-on-fetch=enforced(no-X->instr-page-fault) R-on-load=enforced(no-R->load-page-fault) single-bit-controls=yes\n" as *u8) 105 if lf >= 0 { g_fp(lf, "PERMGATE verdict=GREEN keystone=sv39-page-permission-enforcement probe=page-perm X-fetch+R-load enforced single-bit-controls epoch=" as *u8); g_fn(lf, sys_now_realtime_sec()); g_fp(lf, "\n" as *u8); sys_close(lf) } 106 sys_exit(0); return 0 107 } 108 g_p("PERMGATE verdict=RED (perm enforcement not fully proven) passes=" as *u8); g_fn(1, passes); g_p("\n" as *u8) 109 if lf >= 0 { g_fp(lf, "PERMGATE verdict=RED passes=" as *u8); g_fn(lf, passes); g_fp(lf, "\n" as *u8); sys_close(lf) } 110 sys_exit(1) 111 return 1 112}