nx_tls12_record_gcm_gate.nx source

1// nx_tls12_record_gcm_gate.nx -- SOVEREIGN gate for the TLS 1.2 AES-128-GCM 2// record layer (RFC 5246 §6.2.3.3 + RFC 5288), validating the shipped 3// nx_tls12_record.nx organ (tls12_record_seal / tls12_record_open) and the 4// AES-128-GCM AEAD it composes (nx_aes128_gcm.nx). 5// 6// NOTE on organ name: the task brief calls the organ nx_tls12_record_gcm.nx; 7// the equivalent organ already shipped as nx_tls12_record.nx (verify-don't- 8// rebuild, no duplicate crypto). This gate targets that existing organ. 9// 10// ---- PUBLISHED KAT: AES-128-GCM "Test Case 4" ---- 11// Source: McGrew & Viega, "The Galois/Counter Mode of Operation (GCM)", 12// Appendix B, Test Case 4 -- the reference test set adopted by NIST 13// SP 800-38D. Reproduced byte-identically across openssl/ruby-openssl/etc. 14// K = feffe9928665731c6d6a8f9467308308 (16) 15// IV= cafebabefacedbaddecaf888 (12) 16// A = feedfacedeadbeeffeedfacedeadbeefabaddad2 (20) 17// P = d9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318 18// a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39 (60) 19// C = 42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329ac 20// a12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091 (60) 21// T = 5bc94fbc3221a5db94fae95ae7121a47 (16) 22// This proves the AEAD primitive the record layer composes, byte-exact, 23// with a non-empty AAD and a non-block-aligned (60-byte) plaintext. 24// 25// ---- TLS 1.2 record framing (the organ's own logic) ---- 26// CRITICAL: TLS 1.2's AAD DIFFERS from TLS 1.3's. Here 27// nonce(12) = salt(4, implicit from key_block) || explicit_nonce(8, on wire) 28// AAD(13) = seq_num(8) || type(1) || version(2=0x0303) || plaintext_len(2) 29// record = explicit_nonce(8) || ciphertext || tag(16) 30// Proven by: exact 13-byte AAD layout (RFC 5246 §6.2.3.3), exact nonce split, 31// composition vs the published AEAD, full seal->open round-trip, a tampered 32// tag (open MUST fail, constant-time compare in nx_aes128_gcm_tag_eq), and an 33// AAD-binding check (open under the wrong seq MUST fail). 34// expect_exit: 0 35// license_tier: ORIGINAL 36 37import "nx_syscalls.nx" 38import "nx_gate_emit_lib.nx" 39import "nx_aes128_gcm.nx" 40import "nx_tls12_record.nx" 41 42func ghx_nyb(c: i64) -> i64 { 43 if c >= 0x30 { if c <= 0x39 { return c - 0x30 } } 44 if c >= 0x61 { if c <= 0x66 { return c - 0x61 + 10 } } 45 if c >= 0x41 { if c <= 0x46 { return c - 0x41 + 10 } } 46 return 0 47} 48func ghx(hex: *u8, hexlen: i64, out: *u8) -> i64 { 49 var i: i64 = 0 50 while i < hexlen { 51 let hi: i64 = ghx_nyb(hex[i] as i64) 52 let lo: i64 = ghx_nyb(hex[i + 1] as i64) 53 out[i / 2] = ((hi << 4) | lo) as u8 54 i = i + 2 55 } 56 return hexlen / 2 57} 58func g_eqb(a: *u8, b: *u8, n: i64) -> i64 { 59 var i: i64 = 0 60 while i < n { if (a[i]&0xff)!=(b[i]&0xff) { return 0 } i = i + 1 } 61 return 1 62} 63 64func main() -> i64 { 65 g_puts("nx_tls12_record_gcm gate (GCM Test Case 4 KAT + TLS1.2 framing)\n" as *u8) 66 var pass: i64 = 0 67 var total: i64 = 0 68 69 // ---------- PUBLISHED AES-128-GCM Test Case 4 ---------- 70 let k: *u8 = sys_mmap(16); ghx("feffe9928665731c6d6a8f9467308308" as *u8, 32, k) 71 let iv: *u8 = sys_mmap(12); ghx("cafebabefacedbaddecaf888" as *u8, 24, iv) 72 let a: *u8 = sys_mmap(20); ghx("feedfacedeadbeeffeedfacedeadbeefabaddad2" as *u8, 40, a) 73 let p: *u8 = sys_mmap(60); ghx("d9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39" as *u8, 120, p) 74 let expc: *u8 = sys_mmap(60); ghx("42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091" as *u8, 120, expc) 75 let expt: *u8 = sys_mmap(16); ghx("5bc94fbc3221a5db94fae95ae7121a47" as *u8, 32, expt) 76 77 let gct: *u8 = sys_mmap(60); let gtag: *u8 = sys_mmap(16) 78 nx_aes128_gcm_seal(k, iv, a, 20, p, 60, gct, gtag) 79 pass = pass + g_check("GCM TC4 seal: ciphertext == published C" as *u8, g_eqb(gct, expc, 60)); total = total + 1 80 pass = pass + g_check("GCM TC4 seal: tag == published T" as *u8, g_eqb(gtag, expt, 16)); total = total + 1 81 82 let gpt: *u8 = sys_mmap(60) 83 let ov: i64 = nx_aes128_gcm_open(k, iv, a, 20, expc, 60, expt, gpt) 84 var open_ok: i64 = 0 85 if ov == 0 { if g_eqb(gpt, p, 60) == 1 { open_ok = 1 } } 86 pass = pass + g_check("GCM TC4 open: verifies (rc 0) + recovers P" as *u8, open_ok); total = total + 1 87 88 let badt: *u8 = sys_mmap(16) 89 var bi: i64 = 0 90 while bi < 16 { badt[bi] = expt[bi]; bi = bi + 1 } 91 badt[0] = (badt[0] ^ 0x80) as u8 92 let nv: i64 = nx_aes128_gcm_open(k, iv, a, 20, expc, 60, badt, gpt) 93 pass = pass + g_check("GCM TC4 open: tampered tag -> auth FAIL (rc -1)" as *u8, (nv == (0 - 1)) as i64); total = total + 1 94 95 // ---------- TLS 1.2 record framing ---------- 96 let rkey: *u8 = sys_mmap(16); ghx("404142434445464748494a4b4c4d4e4f" as *u8, 32, rkey) 97 let salt: *u8 = sys_mmap(4); ghx("deadbeef" as *u8, 8, salt) 98 let seq: *u8 = sys_mmap(8); ghx("0000000000000001" as *u8, 16, seq) 99 let rpt: *u8 = sys_mmap(20); ghx("6e69736869732d736f7665726569676e2d746c73" as *u8, 40, rpt) // "nishis-sovereign-tls" (20 bytes) 100 // content_type = 23 (application_data); plaintext_len = 20 (0x0014). 101 102 // 1) AAD layout == seq(8) || type(0x17) || version(0x0303) || len(0x0014) 103 let aad: *u8 = sys_mmap(13) 104 _r12_aad(seq, 23, 20, aad) 105 let expaad: *u8 = sys_mmap(13); ghx("00000000000000011703030014" as *u8, 26, expaad) 106 pass = pass + g_check("record AAD == seq||type||0x0303||len (RFC 5246 6.2.3.3)" as *u8, 107 g_eqb(aad, expaad, 13)); total = total + 1 108 109 // 2) nonce == salt(4) || explicit(8) 110 let non: *u8 = sys_mmap(12) 111 _r12_nonce(salt, seq, non) 112 let expnon: *u8 = sys_mmap(12); ghx("deadbeef0000000000000001" as *u8, 24, expnon) 113 pass = pass + g_check("record nonce == salt||explicit_nonce (RFC 5288)" as *u8, 114 g_eqb(non, expnon, 12)); total = total + 1 115 116 // 3) framing composition: record == explicit || AEAD(key,nonce,aad,pt) 117 let rout: *u8 = sys_mmap(64) 118 let rlen: i64 = tls12_record_seal(rkey, salt, seq, 23, rpt, 20, rout) 119 let refct: *u8 = sys_mmap(20); let reftag: *u8 = sys_mmap(16) 120 nx_aes128_gcm_seal(rkey, non, aad, 13, rpt, 20, refct, reftag) 121 var frame_ok: i64 = 1 122 if rlen != 8 + 20 + 16 { frame_ok = 0 } 123 if g_eqb(rout, seq, 8) != 1 { frame_ok = 0 } // explicit nonce echoed 124 let rout_ct: *u8 = (rout as i64 + 8) as *u8 125 let rout_tag: *u8 = (rout as i64 + 8 + 20) as *u8 126 if g_eqb(rout_ct, refct, 20) != 1 { frame_ok = 0 } 127 if g_eqb(rout_tag, reftag, 16) != 1 { frame_ok = 0 } 128 pass = pass + g_check("record seal == explicit||AEAD(key,nonce,aad,pt)" as *u8, frame_ok); total = total + 1 129 130 // 4) round-trip: open(seal) recovers plaintext, returns its length 131 let ropt: *u8 = sys_mmap(20) 132 let rv: i64 = tls12_record_open(rkey, salt, seq, 23, rout, rlen, ropt) 133 var rt_ok: i64 = 0 134 if rv == 20 { if g_eqb(ropt, rpt, 20) == 1 { rt_ok = 1 } } 135 pass = pass + g_check("record round-trip: open recovers plaintext (len 20)" as *u8, rt_ok); total = total + 1 136 137 // 5) tamper: flip a tag byte in the sealed record -> open MUST fail 138 rout_tag[3] = (rout_tag[3] ^ 0x01) as u8 139 let tv: i64 = tls12_record_open(rkey, salt, seq, 23, rout, rlen, ropt) 140 pass = pass + g_check("record tamper: flipped tag -> open FAILS (-1)" as *u8, (tv == (0 - 1)) as i64); total = total + 1 141 rout_tag[3] = (rout_tag[3] ^ 0x01) as u8 // restore 142 143 // 6) AAD binding: open under the WRONG sequence number -> MUST fail 144 let badseq: *u8 = sys_mmap(8); ghx("0000000000000002" as *u8, 16, badseq) 145 let av: i64 = tls12_record_open(rkey, salt, badseq, 23, rout, rlen, ropt) 146 pass = pass + g_check("record AAD binding: wrong seq -> open FAILS (-1)" as *u8, (av == (0 - 1)) as i64); total = total + 1 147 148 g_puts("gate: " as *u8); g_pn(pass); g_puts("/" as *u8); g_pn(total); g_puts("\n" as *u8) 149 if pass == total { return 0 } 150 return 1 151}