code wiki / _hdl_build / nx_pub_deploy_gate.nx
nx_pub_deploy_gate.nx source
↩ module page · 63 lines · 4282 B
1// nx_pub_deploy_gate.nx -- R3 proof for THE NISHI PUBLISHER deploy step: STAGE -> VERIFY -> PROMOTE, fail-closed.
2// (1) a GOOD artifact stages, re-hashes equal to the approved sha, and is promoted to live; (2) a TAMPERED
3// artifact -- the src is CHANGED after the sha was approved (TOCTOU) -- is REJECTED, and live is NEVER written;
4// (3) NEG-CONTROL: a deploy asked to verify against a WRONG sha is rejected too, proving the verify actually
5// compares (not an always-pass). Sovereign, per-wsid isolated. license_tier: ORIGINAL expect_exit: 0
6import "nx_syscalls.nx"
7import "nx_publisher.nx"
8import "nx_runpath.nx"
9
10func g_w(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_n(v: i64) -> i64 { var m: i64=v; if m<0{g_w("-" as *u8);m=0-m} let t:*u8=sys_mmap(24); var k:i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var i:i64=0; let o:*u8=sys_mmap(24); while i<k{o[i]=t[k-1-i];i=i+1} sys_write(1,o,k); return 0 }
12func g_row(id: *u8, ok: i64, pass: *i64) -> i64 { g_w(" " as *u8); g_w(id); g_w(": " as *u8); if ok==1 { g_w("OK\n" as *u8); pass[0]=pass[0]+1 } else { g_w("FAIL\n" as *u8) } return 0 }
13func dg_make(path: *u8, content: *u8) -> i64 {
14 let fd: i64 = sys_openat_wr(path, 0x1a4); if fd < 0 { return 0 }
15 var n: i64 = 0; while content[n]!=(0 as u8){n=n+1}
16 sys_write(fd, content, n); sys_close(fd); return 1
17}
18
19func main() -> i64 {
20 let pass: *i64 = sys_mmap(8) as *i64; pass[0]=0
21 g_w("=== NX-PUBLISHER DEPLOY GATE (stage -> verify -> promote, FAIL-CLOSED) ===\n" as *u8)
22 let wsid: *u8 = sys_mmap(64); rp_wsid(wsid); rp_ensure(wsid)
23 let src: *u8 = sys_mmap(512); rp_path(wsid, "dep_src" as *u8, src)
24 let stage: *u8 = sys_mmap(512); rp_path(wsid, "dep_stage" as *u8, stage)
25 let live: *u8 = sys_mmap(512); rp_path(wsid, "dep_live" as *u8, live)
26 let src2: *u8 = sys_mmap(512); rp_path(wsid, "dep_src2" as *u8, src2)
27 let stage2: *u8 = sys_mmap(512); rp_path(wsid, "dep_stage2" as *u8, stage2)
28 let live2: *u8 = sys_mmap(512); rp_path(wsid, "dep_live2" as *u8, live2)
29 let stage3: *u8 = sys_mmap(512); rp_path(wsid, "dep_stage3" as *u8, stage3)
30 let live3: *u8 = sys_mmap(512); rp_path(wsid, "dep_live3" as *u8, live3)
31
32 // (1) GOOD: approve sha of src, deploy unchanged -> promote.
33 dg_make(src, "good artifact v1\n" as *u8)
34 let sha: *u8 = sys_mmap(72); pub_sha_file(src, sha)
35 let r1: i64 = pub_deploy(sha, src, stage, live)
36 let good_live: i64 = pub_exists(live)
37 let good_match: i64 = pub_sha_match(live, sha)
38
39 // (2) TAMPERED: approve sha of src2, then CHANGE src2 before deploy -> reject, live2 untouched.
40 dg_make(src2, "approved content\n" as *u8)
41 let sha2: *u8 = sys_mmap(72); pub_sha_file(src2, sha2)
42 dg_make(src2, "TAMPERED malicious payload\n" as *u8)
43 let r2: i64 = pub_deploy(sha2, src2, stage2, live2)
44 let tampered_live: i64 = pub_exists(live2)
45
46 // (3) NEG-CONTROL: deploy good src but verify against an all-zero (wrong) sha -> reject, live3 untouched.
47 let wrong: *u8 = sys_mmap(72); var wi: i64=0; while wi<64 { wrong[wi]=48 as u8; wi=wi+1 } wrong[64]=0 as u8
48 let r3: i64 = pub_deploy(wrong, src, stage3, live3)
49 let wrong_live: i64 = pub_exists(live3)
50
51 g_w(" good: deploy="); g_n(r1); g_w(" live_exists="); g_n(good_live); g_w(" sha_match="); g_n(good_match); g_w("\n")
52 g_w(" tampered: deploy="); g_n(r2); g_w(" live_exists="); g_n(tampered_live); g_w("\n")
53 g_w(" wrong-sha:deploy="); g_n(r3); g_w(" live_exists="); g_n(wrong_live); g_w("\n")
54
55 g_row("PROMOTE: good artifact staged, verified, promoted to live (sha matches)" as *u8, ((r1==1) as i64) & ((good_live==1) as i64) & ((good_match==1) as i64), pass)
56 g_row("FAIL-CLOSED: tampered artifact (src changed post-approval) REJECTED" as *u8, (r2==0) as i64, pass)
57 g_row("LIVE UNTOUCHED: the rejected artifact never reached live" as *u8, (tampered_live==0) as i64, pass)
58 g_row("VERIFY REAL (neg-control): a wrong expected-sha is rejected, live not written" as *u8, ((r3==0) as i64) & ((wrong_live==0) as i64), pass)
59
60 g_w("PUB-DEPLOY rows=4 pass="); g_n(pass[0])
61 if pass[0]==4 { g_w(" verdict=GREEN\n"); sys_exit(0); return 0 }
62 g_w(" verdict=RED\n"); sys_exit(1); return 1
63}