code wiki / _hdl_build / _ctxsw_gate.nx
_ctxsw_gate.nx source
↩ module page · 88 lines · 4831 B
1// _ctxsw_gate.nx -- LOCK for CONTEXT SWITCH between address spaces (satp swap, X-PAGE-CTXSW-001). NO mocks.
2// Proves multiprocess virtual memory: the SAME virtual address (0xC0009000) reads DIFFERENT physical memory
3// depending on the active page table, and swapping satp performs the switch. Drives nx_ctxsw_emit:
4// T1 real-switch : 2nd satp = table B -> load VA(satp=A)=sentinel_A, swap, load VA(satp=B)=sentinel_B -> CSW
5// T2 control : 2nd satp = table A (NO switch) -> both loads hit table A -> t4=sentinel_A!=sentinel_B
6// -> CSW never prints (the swap is load-bearing: without it the VA can't read 2 values)
7// GREEN only if T1 && T2. Evidence -> knowledge/status/priv.log (CTXSWGATE). license_tier: ORIGINAL
8import "nx_syscalls.nx"
9
10const CS_EMIT: *u8 = "_offc/nx_ctxsw_emit.elf"
11const CS_SOV: *u8 = "_offc/nx_boot_run_sov.elf"
12
13func 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 }
14func 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 }
15func 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 }
16
17func g_run(prog: *u8, a1: *u8, a2: *u8, outpath: *u8) -> i64 {
18 let pid: i64 = sys_fork()
19 if pid == 0 {
20 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) } }
21 let argv: *i64 = sys_mmap(32) as *i64
22 argv[0] = prog as i64
23 var k: i64 = 1
24 if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 }
25 if a2 != (0 as *u8) { argv[k] = a2 as i64; k = k + 1 }
26 argv[k] = 0
27 let envp: *i64 = sys_mmap(16) as *i64
28 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0
29 sys_execve(prog, argv, envp)
30 sys_exit(127)
31 }
32 let st: *i64 = sys_mmap(16) as *i64
33 sys_wait4(pid, st, 0)
34 return (st[0] >> 8) & 0xff
35}
36func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
37 let fd: i64 = sys_openat_rd(path)
38 if fd < 0 { return 0 }
39 var n: i64 = 0
40 var go: i64 = 1
41 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 } }
42 sys_close(fd)
43 return n
44}
45func g_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 {
46 if pl <= 0 { return 0 }
47 var i: i64 = 0
48 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 }
49 return 0
50}
51func g_case(satp2: *u8, binp: *u8, txt: *u8, buf: *u8) -> i64 {
52 g_run(CS_EMIT, satp2, binp, "/tmp/_cs_emit.out" as *u8)
53 g_run(CS_SOV, binp, 0 as *u8, txt)
54 return g_read(txt, buf, 65536)
55}
56func 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 }
57
58func main() -> i64 {
59 let b: *u8 = sys_mmap(65536)
60
61 // T1 real context switch (2nd satp = table B) -> same VA reads two address spaces -> CSW
62 var n: i64 = g_case("0x80005" as *u8, "/tmp/_cs_ok.bin" as *u8, "/tmp/_cs_ok.txt" as *u8, b)
63 var t1: i64 = 0
64 if g_has(b, n, "CSW" as *u8, 3) == 1 { if g_has(b, n, "BOOTSOV verdict=GREEN" as *u8, 21) == 1 { t1 = 1 } }
65
66 // T2 control (2nd satp = table A, NO switch) -> same VA reads the SAME value -> no CSW
67 n = g_case("0x80001" as *u8, "/tmp/_cs_noswap.bin" as *u8, "/tmp/_cs_noswap.txt" as *u8, b)
68 var t2: i64 = 0
69 if g_has(b, n, "CSW" as *u8, 3) == 0 { t2 = 1 }
70
71 var ok: i64 = 0
72 if t1 == 1 { if t2 == 1 { ok = 1 } }
73
74 g_p("CTXSW gate (satp-swap context switch: same VA -> two address spaces)\n" as *u8)
75 g_row("T1 real-switch A->B (->CSW) " as *u8, t1)
76 g_row("T2 no-switch control (->!CSW)" as *u8, t2)
77
78 let lf: i64 = sys_openat_append("knowledge/status/priv.log" as *u8, 0x1a4)
79 if ok == 1 {
80 g_p("CTXSWGATE verdict=GREEN keystone=satp-swap-context-switch probe=ctxsw same-VA=0xC0009000 tableA-sentinel!=tableB-sentinel swap-is-load-bearing=yes\n" as *u8)
81 if lf >= 0 { g_fp(lf, "CTXSWGATE verdict=GREEN keystone=satp-swap-context-switch probe=ctxsw same-VA-two-address-spaces + swap-load-bearing-control epoch=" as *u8); g_fn(lf, sys_now_realtime_sec()); g_fp(lf, "\n" as *u8); sys_close(lf) }
82 sys_exit(0); return 0
83 }
84 g_p("CTXSWGATE verdict=RED (t1=" as *u8); g_fn(1, t1); g_p(" t2=" as *u8); g_fn(1, t2); g_p(")\n" as *u8)
85 if lf >= 0 { g_fp(lf, "CTXSWGATE verdict=RED t1=" as *u8); g_fn(lf, t1); g_fp(lf, " t2=" as *u8); g_fn(lf, t2); g_fp(lf, "\n" as *u8); sys_close(lf) }
86 sys_exit(1)
87 return 1
88}