code wiki / (root) / nx_security_census_gate.nx

nx_security_census_gate.nx source

↩ module page · 41 lines · 2363 B

1// nx_security_census_gate.nx -- regression-by-construction for the security census's MEASURED CORE. 2// Proves the three load-bearing behaviours without needing the whole catalog live: 3// (1) coverage permille math (incl. the div-by-zero guard), 4// (2) WEAKEST-LINK weighting -- criticals (weight 3) dominate, so a count-majority of standard controls 5// cannot mask a missing critical one, 6// (3) the disk oracle BOTH WAYS -- a known-present organ reads HAVE, a known-GAP organ (the W4 target, 7// which must stay absent) reads GAP -- the same no-fabrication discipline as the seed-gate neg-control. 8// license_tier: ORIGINAL 9import "nx_security_census_lib.nx" 10import "nx_gate.nx" 11 12func main() -> i64 { 13 var fails: i64 = 0 14 15 // (1) permille math 16 if sc_permil(3, 10) != 300 { fails = fails + 1 } 17 if sc_permil(0, 10) != 0 { fails = fails + 1 } 18 if sc_permil(10, 10) != 1000 { fails = fails + 1 } 19 if sc_permil(5, 0) != 0 { fails = fails + 1 } // div-by-zero guard 20 21 // (2) weakest-link weighting: 2 critical + 2 standard, only the 2 standard present. 22 // count-wise that is 2/4 = 500; weakest-link makes it 2 / (2*3 + 2*1) = 2/8 = 250 -> criticals drag. 23 if sc_weight(1) != 3 { fails = fails + 1 } 24 if sc_weight(0) != 1 { fails = fails + 1 } 25 let tw: i64 = sc_weight(1) + sc_weight(1) + sc_weight(0) + sc_weight(0) 26 let hw: i64 = sc_weight(0) + sc_weight(0) 27 if tw != 8 { fails = fails + 1 } 28 if hw != 2 { fails = fails + 1 } 29 if sc_permil(hw, tw) != 250 { fails = fails + 1 } 30 31 // (3) disk oracle both ways (no fabrication) 32 if sc_have("runtime/nx_threat_model.nx" as *u8) != 1 { fails = fails + 1 } // known-present organ 33 if sc_have("runtime/nx_pq_handshake.nx" as *u8) != 0 { fails = fails + 1 } // known-GAP (W4 target: must stay absent) 34 if sc_have("runtime/nx_security_no_such_organ_zzz.nx" as *u8) != 0 { fails = fails + 1 } 35 36 gw("seccensus-gate: permille-math + weakest-link-weighting + disk-oracle(both ways) ... fails=" as *u8); gn(fails); gw("\n" as *u8) 37 if fails == 0 { gw("GATE nx_security_census verdict=GREEN pass=12/12 (weakest-link coverage math + HAVE/GAP disk oracle)\n" as *u8); sys_exit(0); return 0 } 38 gw("GATE nx_security_census verdict=RED fails=" as *u8); gn(fails); gw("\n" as *u8) 39 sys_exit(1) 40 return 1 41}