nx_restage_gate.nx source
↩ module page · 30 lines · 2625 B
1// nx_restage_gate.nx -- proves the SAFETY core of nx_restage (the target sanitizer = the security
2// boundary: a restage caller must never escape _offc via the target name). The copy/ELF-verify/atomic
3// path is proven LIVE (self-stage RESTAGED bytes=17236, magic 7f454c46). exit 0 == all pass.
4// license_tier: ORIGINAL expect_exit: 0
5import "nx_restage.nx"
6
7func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
8
9func main(argc: i64, argv: *i64) -> i64 {
10 gp("=== nx_restage_gate: target-sanitizer safety KATs ===\n" as *u8)
11 var pass: i64 = 0
12 var total: i64 = 0
13 // T1 valid names accepted
14 total=total+1; if r_san("nx_swcompare_sota" as *u8)==1 { pass=pass+1; gp(" PASS T1 valid name accepted\n" as *u8) } else { gp(" FAIL T1\n" as *u8) }
15 total=total+1; if r_san("nx_restage" as *u8)==1 { pass=pass+1; gp(" PASS T2 valid name accepted\n" as *u8) } else { gp(" FAIL T2\n" as *u8) }
16 // T3 path-escape rejected (the security tooth)
17 total=total+1; if r_san("../etc/passwd" as *u8)==0 { pass=pass+1; gp(" PASS T3 path-escape REJECTED\n" as *u8) } else { gp(" FAIL T3 path-escape leaked\n" as *u8) }
18 total=total+1; if r_san("a/b" as *u8)==0 { pass=pass+1; gp(" PASS T4 slash REJECTED\n" as *u8) } else { gp(" FAIL T4\n" as *u8) }
19 total=total+1; if r_san("foo.elf" as *u8)==0 { pass=pass+1; gp(" PASS T5 dot REJECTED\n" as *u8) } else { gp(" FAIL T5\n" as *u8) }
20 total=total+1; if r_san("a b" as *u8)==0 { pass=pass+1; gp(" PASS T6 space REJECTED\n" as *u8) } else { gp(" FAIL T6\n" as *u8) }
21 // T7 empty rejected
22 total=total+1; if r_san("" as *u8)==0 { pass=pass+1; gp(" PASS T7 empty REJECTED\n" as *u8) } else { gp(" FAIL T7\n" as *u8) }
23 // T8 overlong (>=64) rejected
24 total=total+1; if r_san("aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" as *u8)==0 { pass=pass+1; gp(" PASS T8 overlong REJECTED\n" as *u8) } else { gp(" FAIL T8\n" as *u8) }
25 gp("nx_restage_gate " as *u8)
26 let b: *u8=sys_mmap(8); var m: i64=pass; var k: i64=0; if m==0{b[0]=48 as u8;k=1} while m>0{b[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var i: i64=0; let o: *u8=sys_mmap(8); while i<k{o[i]=b[k-1-i];i=i+1} sys_write(1,o,k)
27 gp("/" as *u8); let b2: *u8=sys_mmap(8); var m2: i64=total; var k2: i64=0; if m2==0{b2[0]=48 as u8;k2=1} while m2>0{b2[k2]=(48+(m2%10)) as u8;m2=m2/10;k2=k2+1} var i2: i64=0; let o2: *u8=sys_mmap(8); while i2<k2{o2[i2]=b2[k2-1-i2];i2=i2+1} sys_write(1,o2,k2)
28 if pass==total { gp(" verdict=GREEN\n" as *u8); sys_exit(0); return 0 }
29 gp(" RED\n" as *u8); sys_exit(1); return 1
30}