nx_tls13_transcript384_gate.nx source

1// nx_tls13_transcript384_gate.nx -- proves the dual-hash transcript (R9, 2026-08-05). 2// 3// WHY: TLS 1.3 picks the transcript hash FROM THE CIPHER SUITE, known only at ServerHello. 4// A single streaming SHA-256 therefore can never serve 0x1302 (AES-256-GCM-SHA384), which is 5// nginx's DEFAULT preference -- so those hosts were unreachable and the crawler then RETIRED 6// them. The transcript now runs BOTH hashes from the first byte. 7// 8// HONEST PROVING METHOD: no invented goldens. The SHA-384 transcript is proven by DEFINITIONAL 9// IDENTITY against sha384_digest -- which is itself NIST-KAT'd in nx_sha384_kat_test.nx. Feeding 10// the same bytes to the streaming transcript and to the one-shot digest MUST agree bit-for-bit. 11// The SHA-256 half is proven UNCHANGED against sha256_digest, which is the regression control: 12// this change must be invisible to every existing caller (client, server and mTLS all share 13// this object). 14// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 15import "nx_syscalls.nx" 16import "nx_gate_verdict.nx" 17import "nx_tls13_transcript.nx" 18import "nx_sha512.nx" 19 20func tg_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 21 22func main(argc: i64, argv: *i64) -> i64 { 23 let ctr: *i64 = gv_ctr() 24 ctr[0] = 0 25 ctr[1] = 0 26 tg_puts("=== nx_tls13_transcript384 gate (dual-hash transcript for 0x1302) ===\n" as *u8) 27 28 // three chunks, fed as separate updates -- exercises the STREAMING path, not a one-shot 29 let m1: *u8 = "abc" as *u8 30 let m2: *u8 = "defghijklmnop" as *u8 31 let m3: *u8 = "0123456789qrstuvwxyz-the-transcript-spans-updates" as *u8 32 let all: *u8 = sys_mmap(256) 33 var n: i64 = 0 34 var i: i64 = 0 35 while m1[i] != (0 as u8) { all[n] = m1[i]; n = n + 1; i = i + 1 } 36 i = 0 37 while m2[i] != (0 as u8) { all[n] = m2[i]; n = n + 1; i = i + 1 } 38 i = 0 39 while m3[i] != (0 as u8) { all[n] = m3[i]; n = n + 1; i = i + 1 } 40 41 let tx: *u8 = nx_tls13_transcript_new() 42 var l1: i64 = 0 43 while m1[l1] != (0 as u8) { l1 = l1 + 1 } 44 var l2: i64 = 0 45 while m2[l2] != (0 as u8) { l2 = l2 + 1 } 46 var l3: i64 = 0 47 while m3[l3] != (0 as u8) { l3 = l3 + 1 } 48 nx_tls13_transcript_update(tx, m1, l1) 49 nx_tls13_transcript_update(tx, m2, l2) 50 nx_tls13_transcript_update(tx, m3, l3) 51 52 // T1 SHA-384 streaming transcript == one-shot sha384_digest (NIST-KAT'd primitive) 53 let got384: *u8 = sys_mmap(64) 54 nx_tls13_transcript_snapshot384(tx, got384) 55 let want384: *u8 = sys_mmap(64) 56 sha384_digest(all, n, want384) 57 var ok384: i64 = 1 58 i = 0 59 while i < 48 { if got384[i] != want384[i] { ok384 = 0 } i = i + 1 } 60 gv_check("T1 SHA-384 transcript == sha384_digest over the same bytes (definitional identity)" as *u8, ok384, ctr) 61 62 // T2 REGRESSION CONTROL: the SHA-256 half must be UNCHANGED -- client, server and mTLS 63 // all share this object, so an existing caller must not observe any difference. 64 let got256: *u8 = sys_mmap(64) 65 nx_tls13_transcript_snapshot(tx, got256) 66 let want256: *u8 = sys_mmap(64) 67 sha256_digest(all, n, want256) 68 var ok256: i64 = 1 69 i = 0 70 while i < 32 { if got256[i] != want256[i] { ok256 = 0 } i = i + 1 } 71 gv_check("T2 CONTROL SHA-256 half UNCHANGED (existing callers see no difference)" as *u8, ok256, ctr) 72 73 // T3 NON-DESTRUCTIVE: snapshotting must not disturb the running state, so a further 74 // update still tracks the one-shot. This is the bug that once corrupted the SHA-256 path. 75 nx_tls13_transcript_update(tx, m1, l1) 76 i = 0 77 while i < l1 { all[n] = m1[i]; n = n + 1; i = i + 1 } 78 let got384b: *u8 = sys_mmap(64) 79 nx_tls13_transcript_snapshot384(tx, got384b) 80 let want384b: *u8 = sys_mmap(64) 81 sha384_digest(all, n, want384b) 82 var ok384b: i64 = 1 83 i = 0 84 while i < 48 { if got384b[i] != want384b[i] { ok384b = 0 } i = i + 1 } 85 gv_check("T3 snapshot384 is NON-DESTRUCTIVE (update after snapshot still tracks)" as *u8, ok384b, ctr) 86 87 // T4 NEGATIVE CONTROL: the two digests must DIFFER, proving T1 is not comparing a buffer 88 // with itself (the vacuity trap -- two failures that agree are not an equivalence). 89 var differ: i64 = 0 90 i = 0 91 while i < 32 { if got384[i] != got256[i] { differ = 1 } i = i + 1 } 92 gv_check("T4 NEG SHA-384 and SHA-256 snapshots DIFFER (T1/T2 are not the same buffer)" as *u8, differ, ctr) 93 94 let rc: i64 = gv_verdict("TLS13-TRANSCRIPT384-GATE" as *u8, ctr, "dual-hash transcript: SHA-384 by definitional identity, SHA-256 unchanged, non-destructive, distinct" as *u8) 95 return rc 96}