nx_tls13_aead1302_gate.nx source

1// nx_tls13_aead1302_gate.nx -- proves the 0x1302 (AES-256-GCM-SHA384) AEAD dispatch is REAL. 2// 3// WHY: our TLS client ADVERTISED 0x1302 and returned BAD_CIPHER, so every server preferring it 4// (nginx's default) was unreachable -- and the crawler then retired those hosts as if THEY were 5// dead. This gate covers the record-layer half: dispatch by cipher_suite to nx_aes256_gcm. 6// It is deliberately a ROUND-TRIP + NEGATIVE-CONTROL gate, not a hand-written golden: sealing 7// then opening under the same key must return the plaintext, a tampered tag must REFUSE, and an 8// unknown suite must still return BAD_CIPHER (-2). No invented vectors. 9// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 10import "nx_syscalls.nx" 11import "nx_gate_verdict.nx" 12import "nx_tls13_record.nx" 13 14func ag_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 15 16func main(argc: i64, argv: *i64) -> i64 { 17 let ctr: *i64 = gv_ctr() 18 ctr[0] = 0 19 ctr[1] = 0 20 ag_puts("=== nx_tls13_aead1302 gate (0x1302 AES-256-GCM record dispatch) ===\n" as *u8) 21 22 let key: *u8 = sys_mmap(64) 23 let nonce: *u8 = sys_mmap(32) 24 let aad: *u8 = sys_mmap(32) 25 let pt: *u8 = sys_mmap(128) 26 let ct: *u8 = sys_mmap(128) 27 let tag: *u8 = sys_mmap(32) 28 let back: *u8 = sys_mmap(128) 29 var i: i64 = 0 30 while i < 32 { key[i] = (i + 7) as u8; i = i + 1 } 31 i = 0 32 while i < 12 { nonce[i] = (i * 3 + 1) as u8; i = i + 1 } 33 i = 0 34 while i < 5 { aad[i] = (23 + i) as u8; i = i + 1 } 35 let ptlen: i64 = 40 36 i = 0 37 while i < ptlen { pt[i] = (i * 5 + 2) as u8; i = i + 1 } 38 39 // T1 seal must succeed under 0x1302 (pre-fix this returned -2 BAD_CIPHER) 40 let sv: i64 = tls13_record_aead_seal(0x1302, key, nonce, aad, 5, pt, ptlen, ct, tag) 41 gv_check("T1 seal 0x1302 dispatches to AES-256-GCM (was BAD_CIPHER)" as *u8, (sv == 0) as i64, ctr) 42 43 // T2 round-trip: open returns the exact plaintext 44 let ov: i64 = tls13_record_aead_open(0x1302, key, nonce, aad, 5, ct, ptlen, tag, back) 45 var same: i64 = 1 46 i = 0 47 while i < ptlen { if back[i] != pt[i] { same = 0 } i = i + 1 } 48 var t2: i64 = 0 49 if ov == 0 { if same == 1 { t2 = 1 } } 50 gv_check("T2 round-trip: open(seal(pt)) == pt byte-for-byte" as *u8, t2, ctr) 51 52 // T3 NEGATIVE CONTROL -- a tampered tag must REFUSE (proves T2 is not vacuous) 53 tag[0] = (tag[0] as i64 ^ 0xff) as u8 54 let bv: i64 = tls13_record_aead_open(0x1302, key, nonce, aad, 5, ct, ptlen, tag, back) 55 gv_check("T3 NEG tampered tag REFUSED (round-trip is authenticated, not a memcpy)" as *u8, (bv != 0) as i64, ctr) 56 tag[0] = (tag[0] as i64 ^ 0xff) as u8 57 58 // T4 an unknown suite must still be BAD_CIPHER -- the dispatch stayed closed 59 let uv: i64 = tls13_record_aead_seal(0x1399, key, nonce, aad, 5, pt, ptlen, ct, tag) 60 gv_check("T4 unknown suite still BAD_CIPHER(-2) -- dispatch did not open up" as *u8, (uv == 0 - 2) as i64, ctr) 61 62 let rc: i64 = gv_verdict("TLS13-AEAD1302-GATE" as *u8, ctr, "0x1302 AES-256-GCM record dispatch: seal, authenticated round-trip, tamper-refusal, closed default" as *u8) 63 return rc 64}