nx_tls13_mtls_finished.nx source
↩ module page · 196 lines · 11888 B
1// nx_tls13_mtls_finished.nx -- R7: the mTLS-aware client Finished handler (the dual-snapshot key schedule).
2//
3// In mutual TLS the server receives the client's Finished AFTER the client Certificate + CertificateVerify,
4// so the transcript at that point runs THROUGH ClientCertVerify. RFC 8446 §4.4.4 says the client Finished MAC
5// is over that (current) transcript -- but §7.1 says the application traffic secrets are derived over the
6// transcript THROUGH SERVER FINISHED. A plain recv_cf uses ONE snapshot for both => wrong app keys under mTLS.
7// This handler takes th_app (the through-ServerFinished snapshot, captured by the run loop right after emit_sf)
8// explicitly: it verifies the Finished MAC over the CURRENT transcript snapshot, and derives the app keys over
9// th_app. Extracted from the run loop so this exact split is GATED (not just compile-checked): the gate proves
10// the function uses th_app for app keys and the current transcript for the MAC, by passing two DIFFERENT values.
11// license_tier: ORIGINAL expect_exit: 0
12import "nx_syscalls.nx"
13import "nx_tls13.nx"
14import "nx_tls13_record.nx"
15import "nx_tls13_transcript.nx"
16import "nx_tls13_kdf.nx"
17import "nx_hmac.nx"
18import "nx_hkdf.nx"
19import "nx_tls13_server_session.nx"
20
21const NX_MFIN_CV_LEN: i64 = 32
22const NX_MFIN_REC_HEADER: i64 = 5
23const NX_MFIN_REC_TAG: i64 = 16
24
25func nx_mfin_eq32(a: *u8, b: *u8) -> i64 {
26 var diff: i64 = 0; var i: i64 = 0
27 while i < 32 { diff = diff | ((a[i] as i64) ^ (b[i] as i64)); i = i + 1 }
28 if diff == 0 { return 1 }
29 return 0
30}
31func nx_mfin_empty_hash(h: *u8) -> i64 {
32 h[0]=0xe3 as u8;h[1]=0xb0 as u8;h[2]=0xc4 as u8;h[3]=0x42 as u8;h[4]=0x98 as u8;h[5]=0xfc as u8;h[6]=0x1c as u8;h[7]=0x14 as u8
33 h[8]=0x9a as u8;h[9]=0xfb as u8;h[10]=0xf4 as u8;h[11]=0xc8 as u8;h[12]=0x99 as u8;h[13]=0x6f as u8;h[14]=0xb9 as u8;h[15]=0x24 as u8
34 h[16]=0x27 as u8;h[17]=0xae as u8;h[18]=0x41 as u8;h[19]=0xe4 as u8;h[20]=0x64 as u8;h[21]=0x9b as u8;h[22]=0x93 as u8;h[23]=0x4c as u8
35 h[24]=0xa4 as u8;h[25]=0x95 as u8;h[26]=0x99 as u8;h[27]=0x1b as u8;h[28]=0x78 as u8;h[29]=0x52 as u8;h[30]=0xb8 as u8;h[31]=0x55 as u8
36 return 0
37}
38
39// MAC verified over the CURRENT transcript (through ClientCertVerify); app keys derived over th_app (through
40// ServerFinished). Returns NX_TLS13_SSESSION_OK -> CONNECTED.
41func nx_tls13_mtls_recv_finished(s: *Tls13ServerSession, record: *u8, record_len: i64, th_app: *u8) -> i64 {
42 if record[0] != 0x17 { return NX_TLS13_SSESSION_PROTOCOL_ERR }
43 let body_len: i64 = ((record[3] as i64) << 8) | (record[4] as i64)
44 let ct_len: i64 = body_len - NX_MFIN_REC_TAG
45 if ct_len < 1 { return NX_TLS13_SSESSION_PROTOCOL_ERR }
46 let ct: *u8 = (record as i64 + NX_MFIN_REC_HEADER) as *u8
47 let tag: *u8 = (record as i64 + NX_MFIN_REC_HEADER + ct_len) as *u8
48 let pt: *u8 = sys_mmap(ct_len + 16); let rct: *i64 = sys_mmap(8) as *i64; let rlen: *i64 = sys_mmap(8) as *i64
49 if nx_tls13_record_decrypt_v2(s.cipher_suite, s.client_hs_traffic_key, s.client_hs_iv, s.client_seq,
50 record, ct, ct_len, tag, pt, rct, rlen) != NX_TLS13_REC_VERDICT_OK { return NX_TLS13_SSESSION_PROTOCOL_ERR }
51 if rct[0] != CT_HANDSHAKE { return NX_TLS13_SSESSION_PROTOCOL_ERR }
52 if (pt[0] & 0xff) != (HT_FINISHED & 0xff) { return NX_TLS13_SSESSION_PROTOCOL_ERR }
53
54 let empty: *u8 = sys_mmap(1)
55 let fkc: *u8 = sys_mmap(NX_MFIN_CV_LEN)
56 if tls13_hkdf_expand_label(s.client_hs_traffic_secret, "finished", 8, empty, 0, NX_MFIN_CV_LEN, fkc) != NX_TLS13_KDF_VERDICT_OK { return NX_TLS13_SSESSION_INTERNAL }
57 let th_mac: *u8 = sys_mmap(NX_MFIN_CV_LEN)
58 if nx_tls13_transcript_snapshot(s.transcript, th_mac) != NX_TLS13_TX_VERDICT_OK { return NX_TLS13_SSESSION_INTERNAL }
59 let expected: *u8 = sys_mmap(NX_MFIN_CV_LEN)
60 hmac_sha256(fkc, NX_MFIN_CV_LEN, th_mac, NX_MFIN_CV_LEN, expected)
61 if nx_mfin_eq32((pt as i64 + 4) as *u8, expected) != 1 { return NX_TLS13_SSESSION_PROTOCOL_ERR }
62
63 let eh: *u8 = sys_mmap(32); nx_mfin_empty_hash(eh)
64 let empty_derived: *u8 = sys_mmap(32)
65 if tls13_hkdf_expand_label(s.handshake_secret, "derived", 7, eh, 32, 32, empty_derived) != NX_TLS13_KDF_VERDICT_OK { return NX_TLS13_SSESSION_INTERNAL }
66 let zero_ikm: *u8 = sys_mmap(32); let master: *u8 = sys_mmap(32)
67 if hkdf_extract(empty_derived, 32, zero_ikm, 32, master) != 0 { return NX_TLS13_SSESSION_INTERNAL }
68 s.master_secret = master
69 let cap_secret: *u8 = sys_mmap(32)
70 if tls13_derive_secret(master, "c ap traffic", 12, th_app, 32, cap_secret) != NX_TLS13_KDF_VERDICT_OK { return NX_TLS13_SSESSION_INTERNAL }
71 s.client_app_traffic_secret = cap_secret
72 let sap_secret: *u8 = sys_mmap(32)
73 if tls13_derive_secret(master, "s ap traffic", 12, th_app, 32, sap_secret) != NX_TLS13_KDF_VERDICT_OK { return NX_TLS13_SSESSION_INTERNAL }
74 s.server_app_traffic_secret = sap_secret
75 let akl: i64 = nx_tls13_aead_key_len(s.cipher_suite)
76 let ck: *u8 = sys_mmap(akl); tls13_hkdf_expand_label(cap_secret, "key", 3, empty, 0, akl, ck); s.client_app_traffic_key = ck
77 let civ: *u8 = sys_mmap(12); tls13_hkdf_expand_label(cap_secret, "iv", 2, empty, 0, 12, civ); s.client_app_iv = civ
78 let sk: *u8 = sys_mmap(akl); tls13_hkdf_expand_label(sap_secret, "key", 3, empty, 0, akl, sk); s.server_app_traffic_key = sk
79 let siv: *u8 = sys_mmap(12); tls13_hkdf_expand_label(sap_secret, "iv", 2, empty, 0, 12, siv); s.server_app_iv = siv
80
81 s.client_seq = s.client_seq + 1
82 s.state = NX_TLS13_SSTATE_CONNECTED
83 return NX_TLS13_SSESSION_OK
84}
85
86// ===================== gate: prove the DUAL snapshot (MAC over current, app-keys over th_app) =====================
87func mf_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
88func mf_row(name: *u8, ok: i64) -> i64 { if ok == 1 { mf_w(" PASS " as *u8) } else { mf_w(" FAIL " as *u8) } mf_w(name); mf_w("\n" as *u8); return ok }
89
90func mf_mksession(hs: *u8, chts: *u8, key: *u8, iv: *u8) -> *Tls13ServerSession {
91 let s: *Tls13ServerSession = sys_mmap(264) as *Tls13ServerSession
92 s.cipher_suite = 0x1303
93 s.handshake_secret = hs
94 s.client_hs_traffic_secret = chts
95 s.client_hs_traffic_key = key
96 s.client_hs_iv = iv
97 s.client_seq = 0
98 s.transcript = nx_tls13_transcript_new()
99 // give the transcript some content => its snapshot (the "current"/through-ClientCV hash) differs from th_app
100 nx_tls13_transcript_update(s.transcript, "current-transcript-through-client-certverify" as *u8, 44)
101 s.state = NX_TLS13_SSTATE_SF_SENT
102 return s
103}
104
105// build a client Finished record whose MAC is over `th_mac`, sealed under (key,iv,seq=0).
106func mf_build_finished_rec(chts: *u8, th_mac: *u8, key: *u8, iv: *u8, rec: *u8) -> i64 {
107 let empty: *u8 = sys_mmap(1)
108 let fkc: *u8 = sys_mmap(32)
109 tls13_hkdf_expand_label(chts, "finished", 8, empty, 0, 32, fkc)
110 let mac: *u8 = sys_mmap(32)
111 hmac_sha256(fkc, 32, th_mac, 32, mac)
112 let msg: *u8 = sys_mmap(40)
113 msg[0] = HT_FINISHED & 0xff; msg[1] = 0 as u8; msg[2] = 0 as u8; msg[3] = 32 as u8
114 var i: i64 = 0; while i < 32 { msg[4 + i] = mac[i]; i = i + 1 }
115 let header: *u8 = sys_mmap(5); let ctb: *u8 = sys_mmap(56); let tagb: *u8 = sys_mmap(16)
116 if nx_tls13_record_encrypt_v2(0x1303, key, iv, 0, msg, 36, CT_HANDSHAKE, 0, header, ctb, tagb) != NX_TLS13_REC_VERDICT_OK { return 0 - 1 }
117 var w: i64 = 0
118 var hi: i64 = 0; while hi < 5 { rec[w + hi] = header[hi]; hi = hi + 1 } w = w + 5
119 var ci: i64 = 0; while ci < 37 { rec[w + ci] = ctb[ci]; ci = ci + 1 } w = w + 37
120 var ti: i64 = 0; while ti < 16 { rec[w + ti] = tagb[ti]; ti = ti + 1 } w = w + 16
121 return w
122}
123
124// independent expected client app key over a given transcript hash (same KDF; differs only by the snapshot).
125func mf_expected_capkey(hs: *u8, thash: *u8, out: *u8) -> i64 {
126 let empty: *u8 = sys_mmap(1)
127 let eh: *u8 = sys_mmap(32); nx_mfin_empty_hash(eh)
128 let ed: *u8 = sys_mmap(32); tls13_hkdf_expand_label(hs, "derived", 7, eh, 32, 32, ed)
129 let zero: *u8 = sys_mmap(32); let master: *u8 = sys_mmap(32); hkdf_extract(ed, 32, zero, 32, master)
130 let cs: *u8 = sys_mmap(32); tls13_derive_secret(master, "c ap traffic", 12, thash, 32, cs)
131 tls13_hkdf_expand_label(cs, "key", 3, empty, 0, 32, out)
132 return 0
133}
134
135func main() -> i64 {
136 mf_w("nx_tls13 mTLS Finished gate (DUAL snapshot: MAC over current transcript, app-keys over th_app; R7)\n" as *u8)
137 let hs: *u8 = sys_mmap(32); var a: i64 = 0; while a < 32 { hs[a] = (0x10 + a) as u8; a = a + 1 }
138 let chts: *u8 = sys_mmap(32); a = 0; while a < 32 { chts[a] = (0x40 + a) as u8; a = a + 1 }
139 let key: *u8 = sys_mmap(32); a = 0; while a < 32 { key[a] = (0x70 + a) as u8; a = a + 1 }
140 let iv: *u8 = sys_mmap(12); a = 0; while a < 12 { iv[a] = (0x90 + a) as u8; a = a + 1 }
141 // th_app (through-ServerFinished) -- a DISTINCT value from the current transcript hash
142 let th_app: *u8 = sys_mmap(32); a = 0; while a < 32 { th_app[a] = (0xAA ^ a) as u8; a = a + 1 }
143
144 var pass: i64 = 0
145
146 // valid client Finished: MAC over the CURRENT transcript snapshot
147 let s1: *Tls13ServerSession = mf_mksession(hs, chts, key, iv)
148 let th_cur: *u8 = sys_mmap(32); nx_tls13_transcript_snapshot(s1.transcript, th_cur)
149 let rec: *u8 = sys_mmap(96); let rlen: i64 = mf_build_finished_rec(chts, th_cur, key, iv, rec)
150 let r1: i64 = nx_tls13_mtls_recv_finished(s1, rec, rlen, th_app)
151 var t1: i64 = 0
152 if r1 == NX_TLS13_SSESSION_OK { t1 = 1 }
153 pass = pass + mf_row("T1 client Finished (MAC over current transcript) ACCEPTED" as *u8, t1)
154
155 var t2: i64 = 0
156 if s1.state == NX_TLS13_SSTATE_CONNECTED { t2 = 1 }
157 pass = pass + mf_row("T2 handshake reaches CONNECTED" as *u8, t2)
158
159 // THE dual-snapshot proof: app keys must be derived over th_app, NOT over the current transcript
160 let exp_app: *u8 = sys_mmap(32); mf_expected_capkey(hs, th_app, exp_app)
161 var t3: i64 = 0
162 if nx_mfin_eq32(s1.client_app_traffic_key, exp_app) == 1 { t3 = 1 }
163 pass = pass + mf_row("T3 app keys derived over th_app (through-ServerFinished), NOT the current transcript" as *u8, t3)
164
165 // negative: the same keys must NOT equal a derivation over the current transcript (proves they differ)
166 let exp_cur: *u8 = sys_mmap(32); mf_expected_capkey(hs, th_cur, exp_cur)
167 var t4: i64 = 0
168 if nx_mfin_eq32(s1.client_app_traffic_key, exp_cur) == 0 { t4 = 1 }
169 pass = pass + mf_row("T4 app keys are NOT the current-transcript derivation (the two snapshots really differ)" as *u8, t4)
170
171 // a Finished whose MAC is over th_app (wrong) must be REJECTED -> proves the MAC uses the current transcript
172 let s2: *Tls13ServerSession = mf_mksession(hs, chts, key, iv)
173 let rec2: *u8 = sys_mmap(96); let rlen2: i64 = mf_build_finished_rec(chts, th_app, key, iv, rec2)
174 let r5: i64 = nx_tls13_mtls_recv_finished(s2, rec2, rlen2, th_app)
175 var t5: i64 = 0
176 if r5 != NX_TLS13_SSESSION_OK { t5 = 1 }
177 pass = pass + mf_row("T5 Finished MAC'd over th_app (not the current transcript) is REJECTED" as *u8, t5)
178
179 // tampered record -> AEAD failure
180 let s3: *Tls13ServerSession = mf_mksession(hs, chts, key, iv)
181 let th_cur3: *u8 = sys_mmap(32); nx_tls13_transcript_snapshot(s3.transcript, th_cur3)
182 let rec3: *u8 = sys_mmap(96); let rlen3: i64 = mf_build_finished_rec(chts, th_cur3, key, iv, rec3)
183 rec3[7] = (rec3[7] ^ 0x80) as u8
184 let r6: i64 = nx_tls13_mtls_recv_finished(s3, rec3, rlen3, th_app)
185 var t6: i64 = 0
186 if r6 != NX_TLS13_SSESSION_OK { t6 = 1 }
187 pass = pass + mf_row("T6 tampered Finished record rejected (AEAD)" as *u8, t6)
188
189 if pass == 6 {
190 mf_w("NX-TLS13-MTLS-FINISHED GATE GREEN 6/6 (dual snapshot PROVEN: MAC over current, app-keys over th_app)\n" as *u8)
191 sys_exit(0)
192 }
193 mf_w("NX-TLS13-MTLS-FINISHED GATE RED\n" as *u8)
194 sys_exit(1)
195 return 1
196}