_ubit_gate.nx source

1// _ubit_gate.nx -- LOCK for Sv39 USER/SUPERVISOR page isolation (U-bit + mstatus.SUM, X-PAGE-UBIT-001). 2// Proves the CPU enforces the U-bit per privilege (riscv-priv-spec): an S-mode access to a USER page is 3// DENIED unless mstatus.SUM; a supervisor page is always S-accessible. Drives nx_ubit_emit (data-PTE + 4// mstatus-extra args) on the sovereign emu with SINGLE-AXIS controls so each rule is proven distinctly: 5// T1 S + U-page + SUM : data 0x2000001F (U=1), mstatus +SUM(0x40000) -> access ALLOWED -> "UOK" 6// T2 S + U-page + no-SUM: data 0x2000001F (U=1), mstatus +0 -> DENIED -> load-page-fault -> "UPF" 7// T3 S + sup-page+ no-SUM: data 0x2000000F (U=0), mstatus +0 -> ALLOWED (supervisor page) -> "UOK" 8// T1 vs T2 differ ONLY in SUM -> proves SUM gating. T2 vs T3 differ ONLY in the U bit -> proves the U-bit. 9// GREEN only if T1..T3 hold. Evidence -> knowledge/status/priv.log (UBITGATE). license_tier: ORIGINAL 10import "nx_syscalls.nx" 11 12const UB_EMIT: *u8 = "_offc/nx_ubit_emit.elf" 13const UB_SOV: *u8 = "_offc/nx_boot_run_sov.elf" 14 15func 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 } 16func 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 } 17func 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 } 18 19// fork + run prog with up to 3 argv args (null = omit) + stdout/stderr redirect to outpath. 20func g_run(prog: *u8, a1: *u8, a2: *u8, a3: *u8, outpath: *u8) -> i64 { 21 let pid: i64 = sys_fork() 22 if pid == 0 { 23 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) } } 24 let argv: *i64 = sys_mmap(32) as *i64 25 argv[0] = prog as i64 26 var k: i64 = 1 27 if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 } 28 if a2 != (0 as *u8) { argv[k] = a2 as i64; k = k + 1 } 29 if a3 != (0 as *u8) { argv[k] = a3 as i64; k = k + 1 } 30 argv[k] = 0 31 let envp: *i64 = sys_mmap(16) as *i64 32 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 33 sys_execve(prog, argv, envp) 34 sys_exit(127) 35 } 36 let st: *i64 = sys_mmap(16) as *i64 37 sys_wait4(pid, st, 0) 38 return (st[0] >> 8) & 0xff 39} 40func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 41 let fd: i64 = sys_openat_rd(path) 42 if fd < 0 { return 0 } 43 var n: i64 = 0 44 var go: i64 = 1 45 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 } } 46 sys_close(fd) 47 return n 48} 49func g_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 50 if pl <= 0 { return 0 } 51 var i: i64 = 0 52 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 } 53 return 0 54} 55// emit(data_pte, mstatus -> binpath) then run the emu(binpath -> txt); return serial bytes in buf. 56func g_case(data_pte: *u8, mstatus: *u8, binp: *u8, txt: *u8, buf: *u8) -> i64 { 57 g_run(UB_EMIT, data_pte, mstatus, binp, "/tmp/_ub_emit.out" as *u8) 58 g_run(UB_SOV, binp, 0 as *u8, 0 as *u8, txt) 59 return g_read(txt, buf, 65536) 60} 61func 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 } 62 63func main() -> i64 { 64 let b: *u8 = sys_mmap(65536) 65 66 // T1 S + U-page + SUM -> allowed -> UOK 67 var n: i64 = g_case("0x2000001F" as *u8, "0x40000" as *u8, "/tmp/_ub_sum.bin" as *u8, "/tmp/_ub_sum.txt" as *u8, b) 68 var t1: i64 = 0 69 if g_has(b, n, "UOK" as *u8, 3) == 1 { if g_has(b, n, "BOOTSOV verdict=GREEN" as *u8, 21) == 1 { t1 = 1 } } 70 71 // T2 S + U-page + no-SUM -> denied -> UPF (and no UOK) 72 n = g_case("0x2000001F" as *u8, "0x0" as *u8, "/tmp/_ub_nosum.bin" as *u8, "/tmp/_ub_nosum.txt" as *u8, b) 73 var t2: i64 = 0 74 if g_has(b, n, "UPF" as *u8, 3) == 1 { if g_has(b, n, "UOK" as *u8, 3) == 0 { t2 = 1 } } 75 76 // T3 S + supervisor-page + no-SUM -> allowed (U=0 needs no SUM) -> UOK 77 n = g_case("0x2000000F" as *u8, "0x0" as *u8, "/tmp/_ub_sup.bin" as *u8, "/tmp/_ub_sup.txt" as *u8, b) 78 var t3: i64 = 0 79 if g_has(b, n, "UOK" as *u8, 3) == 1 { t3 = 1 } 80 81 var passes: i64 = 0 82 if t1==1 { passes=passes+1 } 83 if t2==1 { passes=passes+1 } 84 if t3==1 { passes=passes+1 } 85 var ok: i64 = 0 86 if passes == 3 { ok = 1 } 87 88 g_p("UBIT gate (Sv39 user/supervisor isolation: U-bit + mstatus.SUM)\n" as *u8) 89 g_row("T1 S+U-page+SUM (->UOK) " as *u8, t1) 90 g_row("T2 S+U-page+noSUM (->UPF) " as *u8, t2) 91 g_row("T3 S+sup-page+noSUM (->UOK)" as *u8, t3) 92 93 let lf: i64 = sys_openat_append("knowledge/status/priv.log" as *u8, 0x1a4) 94 if ok == 1 { 95 g_p("UBITGATE verdict=GREEN keystone=sv39-user-supervisor-isolation probe=ubit-sum S-to-userpage=denied-without-SUM allowed-with-SUM sup-page=always-allowed single-axis-controls=yes\n" as *u8) 96 if lf >= 0 { g_fp(lf, "UBITGATE verdict=GREEN keystone=sv39-user-supervisor-isolation probe=ubit-sum U-bit+SUM enforced single-axis-controls epoch=" as *u8); g_fn(lf, sys_now_realtime_sec()); g_fp(lf, "\n" as *u8); sys_close(lf) } 97 sys_exit(0); return 0 98 } 99 g_p("UBITGATE verdict=RED (user/supervisor isolation not fully proven) passes=" as *u8); g_fn(1, passes); g_p("\n" as *u8) 100 if lf >= 0 { g_fp(lf, "UBITGATE verdict=RED passes=" as *u8); g_fn(lf, passes); g_fp(lf, "\n" as *u8); sys_close(lf) } 101 sys_exit(1) 102 return 1 103}