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}