nx_tls13_record.nx source
↩ module page · 380 lines · 15031 B
1// nx_tls13_record.nx -- TLS 1.3 record-layer protection (RFC 8446 §5.2).
2//
3// Phase 0b §K of the Nishi TLS 1.3 stack per
4// docs/NISHI_TLS13_GAP_AUDIT.md. The bridge between the shipped
5// ChaCha20-Poly1305 AEAD primitive and the actual TLS wire format.
6// Every encrypted record on a TLS 1.3 connection -- handshake or
7// application data, in either direction -- flows through this.
8//
9// Record wire format (RFC 8446 §5.1, §5.2):
10//
11// struct {
12// ContentType type = 23; // application_data wrapper
13// ProtocolVersion legacy_version = 0x0303;
14// uint16 length; // total of AEAD output
15// opaque encrypted_record[length]; // AEAD output (CT || tag)
16// } TLSCiphertext;
17//
18// Inner plaintext (what AEAD encrypts):
19//
20// struct {
21// opaque content[TLSPlaintext.length];
22// ContentType type; // the REAL content type
23// uint8 zeros[padding_length]; // optional padding
24// } TLSInnerPlaintext;
25//
26// Nonce construction (RFC 8446 §5.3):
27//
28// nonce = pad_left(seq_num, iv_len) XOR static_iv
29//
30// where static_iv is the per-direction traffic_iv derived from
31// nx_tls13_schedule. seq_num is a 64-bit counter; for IV length 12
32// (ChaCha20-Poly1305 + AES-GCM), the left-pad is 4 zero bytes.
33//
34// AAD construction (RFC 8446 §5.2):
35//
36// additional_data = TLSCiphertext header (the 5 bytes: type +
37// legacy_version + length)
38//
39// What it does today:
40// - encrypt: construct inner plaintext, derive nonce, encrypt+tag
41// - decrypt: verify tag (constant-time), strip padding, extract type
42// - sealed record verdict (OK / TAG_MISMATCH / BAD_PADDING /
43// EMPTY_INNER -- the last is the all-padding-no-real-content
44// attack from RFC 8446 §5.4)
45//
46// What it doesn't do yet:
47// - KeyUpdate (sequence-number reset + key rotation; Phase 0b §N)
48// - AES-256-GCM (0x1302): needs an AES-256 cipher + SHA-384 schedule.
49// [AES-128-GCM (0x1301) IS done + wired -- see the dispatch below.]
50// - Sequence-number overflow guard (caller's state machine
51// responsibility -- the schedule docs say 2^64 - 1 is the
52// spec-mandated kill threshold)
53//
54// KAT verified:
55// - Round-trip: encrypt then decrypt restores plaintext + type
56// - Nonce changes with seq: encrypt(seq=0) != encrypt(seq=1)
57// - Tampered tag: decrypt returns TAG_MISMATCH
58// - Tampered AAD (wrong length): decrypt returns TAG_MISMATCH
59// - Padding: encrypt with padding_len > 0, decrypt strips it
60// - Empty inner (all padding, no content type): decrypt returns
61// EMPTY_INNER per RFC 8446 §5.4
62//
63// Composes with:
64// - nx_chacha20_poly1305 (AEAD primitive)
65// - nx_tls13_schedule (traffic_key + traffic_iv source)
66// - nx_tls13 (ContentType + ProtocolVersion constants)
67// - nx_tls13_client state machine (queued; manages seq counters)
68//
69// license_tier: INDEPENDENT_REDERIVE
70// genealogy_id: international-research-sources/ietf/rfc_8446
71// lineage_id: nishi_tls13_record_q10
72
73// nx_safety_envelope:
74// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
75// sil_target: SIL1
76// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
77// verdict: NOT_YET_EVALUATED
78
79import "nx_syscalls.nx"
80import "nx_chacha20_poly1305.nx"
81import "nx_aes128_gcm.nx"
82import "nx_aes256_gcm.nx" // 0x1302 AES-256-GCM-SHA384 dispatch (2026-08-05)
83// AES-128-GCM IS WIRED: the record dispatch below routes cipher_suite 0x1301 to nx_aes128_gcm_seal/open
84// (0x1303 -> chacha20-poly1305), and it decrypts live TLS handshakes. [Corrected 2026-07-03: this comment
85// previously said the wiring was "intentionally deferred" / over the 2048-const cap / Task #78-blocked --
86// STALE; the import above + the dispatch below prove it is live. asserted-not-proven doc defect, fixed.]
87
88const NX_TLS13_RECORD_IV_LEN: i64 = 12
89const NX_TLS13_RECORD_TAG_LEN: i64 = 16
90const NX_TLS13_RECORD_HEADER_LEN: i64 = 5 // TLSCiphertext header
91
92// Per RFC 8446 §5.1 plaintext fragments are <= 2^14 + 1 (the +1 is
93// the inner-content-type byte). TLSCiphertext adds 16 bytes for
94// the AEAD tag + optional padding. We cap at 2^14 + 256 to match
95// the RFC's TLSCiphertext.length ceiling.
96const NX_TLS13_MAX_INNER_PLAINTEXT: i64 = 16385 // 2^14 + 1
97const NX_TLS13_MAX_RECORD_PAYLOAD: i64 = 16640 // 2^14 + 256
98
99// ContentType values relevant to the record layer (RFC 8446 §5.1, §B.1).
100const NX_TLS13_CT_INVALID: i64 = 0
101const NX_TLS13_CT_CHANGE_CIPHER_SPEC: i64 = 20
102const NX_TLS13_CT_ALERT: i64 = 21
103const NX_TLS13_CT_HANDSHAKE: i64 = 22
104const NX_TLS13_CT_APPLICATION_DATA: i64 = 23
105
106const NX_TLS13_LEGACY_VERSION: i64 = 0x0303
107
108// Sealed record verdict.
109const NX_TLS13_REC_VERDICT_OK: i64 = 1
110const NX_TLS13_REC_VERDICT_TAG_MISMATCH: i64 = 2
111const NX_TLS13_REC_VERDICT_BAD_PADDING: i64 = 3
112const NX_TLS13_REC_VERDICT_EMPTY_INNER: i64 = 4
113const NX_TLS13_REC_VERDICT_TOO_LONG: i64 = 5
114const NX_TLS13_REC_VERDICT_TOO_SHORT: i64 = 6
115const NX_TLS13_REC_VERDICT_N: i64 = 7
116
117// Compute the per-record nonce per RFC 8446 §5.3.
118// nonce[0..3] = static_iv[0..3] ^ 0 (seq high bytes zero-padded)
119// nonce[4..12] = static_iv[4..12] ^ seq_num_big_endian
120//
121// In other words: left-pad seq to 12 bytes (4 zero bytes + 8-byte
122// big-endian seq) then XOR against static_iv elementwise.
123func tls13_record_build_nonce(static_iv: *u8, seq: i64, nonce_out: *u8) -> i64 {
124 nonce_out[0] = static_iv[0] & 0xff
125 nonce_out[1] = static_iv[1] & 0xff
126 nonce_out[2] = static_iv[2] & 0xff
127 nonce_out[3] = static_iv[3] & 0xff
128 nonce_out[4] = (static_iv[4] & 0xff) ^ ((seq >> 56) & 0xff)
129 nonce_out[5] = (static_iv[5] & 0xff) ^ ((seq >> 48) & 0xff)
130 nonce_out[6] = (static_iv[6] & 0xff) ^ ((seq >> 40) & 0xff)
131 nonce_out[7] = (static_iv[7] & 0xff) ^ ((seq >> 32) & 0xff)
132 nonce_out[8] = (static_iv[8] & 0xff) ^ ((seq >> 24) & 0xff)
133 nonce_out[9] = (static_iv[9] & 0xff) ^ ((seq >> 16) & 0xff)
134 nonce_out[10] = (static_iv[10] & 0xff) ^ ((seq >> 8) & 0xff)
135 nonce_out[11] = (static_iv[11] & 0xff) ^ ( seq & 0xff)
136 return 0
137}
138
139// Write the 5-byte TLSCiphertext header. total_len = length of the
140// AEAD-encrypted payload (ciphertext + tag). This IS the additional
141// authenticated data fed to the AEAD.
142func tls13_record_write_header(header_out: *u8, total_len: i64) -> i64 {
143 header_out[0] = NX_TLS13_CT_APPLICATION_DATA & 0xff
144 header_out[1] = (NX_TLS13_LEGACY_VERSION >> 8) & 0xff
145 header_out[2] = NX_TLS13_LEGACY_VERSION & 0xff
146 header_out[3] = (total_len >> 8) & 0xff
147 header_out[4] = total_len & 0xff
148 return NX_TLS13_RECORD_HEADER_LEN
149}
150
151// Encrypt a TLS 1.3 application record.
152//
153// Inputs:
154// key, iv = traffic_key and traffic_iv from nx_tls13_schedule
155// seq = per-direction sequence number (caller increments)
156// content, content_len, real_content_type = the plaintext + its
157// actual ContentType (handshake/alert/application)
158// padding_len = optional zero-byte padding (length-hiding); 0 = none
159// header_out = 5-byte TLSCiphertext header (caller buffer)
160// ct_out = ciphertext buffer (must hold content_len + 1 + padding_len)
161// tag_out = 16-byte AEAD tag buffer
162//
163// Returns NX_TLS13_REC_VERDICT_OK or a sealed non-OK verdict.
164// AEAD dispatcher. Routes to ChaCha20-Poly1305 (0x1303) or
165// AES-128-GCM (0x1301) per RFC 8446 §5.2. Wired 2026-05-20 after
166// the IR-extension + silent-dropping fix landed (AES seal/open are
167// 8-arg primitives; previously >6-arg path silently dropped args).
168// Per [[feedback-c-is-wheeler-test-only]]: substrate is daily-driver.
169//
170// Unknown cipher_suite returns -2 (NX_AEAD_VERDICT_BAD_CIPHER) so
171// caller can surface a clean error instead of garbling bytes.
172func tls13_record_aead_seal(cipher_suite: i64,
173 key: *u8, nonce: *u8,
174 aad: *u8, aad_len: i64,
175 pt: *u8, pt_len: i64,
176 ct_out: *u8, tag_out: *u8) -> i64 {
177 if cipher_suite == 0x1303 {
178 let v: i64 = nx_chacha20_poly1305_encrypt(
179 key, nonce, aad, aad_len, pt, pt_len, ct_out, tag_out
180 )
181 if v != NX_AEAD_VERDICT_OK { return 0 - 1 }
182 return 0
183 }
184 if cipher_suite == 0x1301 {
185 let v: i64 = nx_aes128_gcm_seal(
186 key, nonce, aad, aad_len, pt, pt_len, ct_out, tag_out
187 )
188 if v != 0 { return 0 - 1 }
189 return 0
190 }
191 // 0x1302 AES-256-GCM-SHA384 (2026-08-05). ADDITIVE and UNREACHABLE until
192 // recv_sh accepts the suite -- so the blast radius of a defect here is exactly
193 // the set of hosts that are 100% unreachable today. key is 32 bytes (AES-256),
194 // nonce 12; the SHA-384 half of the KEY SCHEDULE is the remaining rung.
195 if cipher_suite == 0x1302 {
196 let v: i64 = nx_aes256_gcm_seal(
197 key, nonce, aad, aad_len, pt, pt_len, ct_out, tag_out
198 )
199 if v != 0 { return 0 - 1 }
200 return 0
201 }
202 return 0 - 2 // BAD_CIPHER
203}
204
205func tls13_record_aead_open(cipher_suite: i64,
206 key: *u8, nonce: *u8,
207 aad: *u8, aad_len: i64,
208 ct: *u8, ct_len: i64, tag: *u8,
209 pt_out: *u8) -> i64 {
210 if cipher_suite == 0x1303 {
211 let v: i64 = nx_chacha20_poly1305_decrypt(
212 key, nonce, aad, aad_len, ct, ct_len, tag, pt_out
213 )
214 if v != NX_AEAD_VERDICT_OK { return 0 - 1 }
215 return 0
216 }
217 if cipher_suite == 0x1301 {
218 let v: i64 = nx_aes128_gcm_open(
219 key, nonce, aad, aad_len, ct, ct_len, tag, pt_out
220 )
221 if v != 0 { return 0 - 1 }
222 return 0
223 }
224 if cipher_suite == 0x1302 {
225 let v: i64 = nx_aes256_gcm_open(
226 key, nonce, aad, aad_len, ct, ct_len, tag, pt_out
227 )
228 if v != 0 { return 0 - 1 }
229 return 0
230 }
231 return 0 - 2 // BAD_CIPHER
232}
233
234// Cipher-suite-aware encrypt. cipher_suite is the TLS 1.3 wire value
235// (0x1301 = AES-128-GCM-SHA256, 0x1303 = ChaCha20-Poly1305-SHA256).
236func nx_tls13_record_encrypt_v2(
237 cipher_suite: i64,
238 key: *u8, iv: *u8, seq: i64,
239 content: *u8, content_len: i64,
240 real_content_type: i64,
241 padding_len: i64,
242 header_out: *u8,
243 ct_out: *u8,
244 tag_out: *u8
245) -> i64 {
246 let inner_len: i64 = content_len + 1 + padding_len
247 if inner_len > NX_TLS13_MAX_INNER_PLAINTEXT { return NX_TLS13_REC_VERDICT_TOO_LONG }
248 if content_len < 0 { return NX_TLS13_REC_VERDICT_TOO_SHORT }
249 if padding_len < 0 { return NX_TLS13_REC_VERDICT_BAD_PADDING }
250
251 let inner: *u8 = sys_mmap(inner_len + 16)
252 var i: i64 = 0
253 while i < content_len { inner[i] = content[i]; i = i + 1 }
254 inner[content_len] = real_content_type & 0xff
255 var p: i64 = 0
256 while p < padding_len { inner[content_len + 1 + p] = 0; p = p + 1 }
257
258 let total_payload: i64 = inner_len + NX_TLS13_RECORD_TAG_LEN
259 tls13_record_write_header(header_out, total_payload)
260
261 let nonce: *u8 = sys_mmap(16)
262 tls13_record_build_nonce(iv, seq, nonce)
263
264 let v: i64 = tls13_record_aead_seal(
265 cipher_suite,
266 key, nonce,
267 header_out, NX_TLS13_RECORD_HEADER_LEN,
268 inner, inner_len,
269 ct_out, tag_out
270 )
271 if v != 0 { return NX_TLS13_REC_VERDICT_TAG_MISMATCH }
272 return NX_TLS13_REC_VERDICT_OK
273}
274
275// Legacy ChaCha20-only wrapper for back-compat with callers that
276// haven't been migrated to the cipher_suite-aware v2 entry point.
277func nx_tls13_record_encrypt(
278 key: *u8, iv: *u8, seq: i64,
279 content: *u8, content_len: i64,
280 real_content_type: i64,
281 padding_len: i64,
282 header_out: *u8,
283 ct_out: *u8,
284 tag_out: *u8
285) -> i64 {
286 return nx_tls13_record_encrypt_v2(
287 0x1303,
288 key, iv, seq, content, content_len,
289 real_content_type, padding_len,
290 header_out, ct_out, tag_out
291 )
292}
293
294// Decrypt a TLS 1.3 application record.
295//
296// Inputs:
297// key, iv, seq = as encrypt
298// header = the 5 received bytes (used as AAD; caller MUST pass
299// the literal bytes seen on the wire)
300// ct, ct_len = encrypted record body (inner_len bytes; tag follows)
301// tag = 16-byte received tag
302// content_out = caller buffer >= ct_len (we strip type + padding)
303// real_content_type_out = *i64 to receive the real ContentType
304// real_content_len_out = *i64 to receive bytes written to content_out
305//
306// On TAG_MISMATCH the content/type/len outputs are NOT written
307// (caller must not read them). Tag check is constant-time first.
308func nx_tls13_record_decrypt_v2(
309 cipher_suite: i64,
310 key: *u8, iv: *u8, seq: i64,
311 header: *u8,
312 ct: *u8, ct_len: i64,
313 tag: *u8,
314 content_out: *u8,
315 real_content_type_out: *i64,
316 real_content_len_out: *i64
317) -> i64 {
318 if ct_len < 1 { return NX_TLS13_REC_VERDICT_TOO_SHORT }
319 if ct_len > NX_TLS13_MAX_INNER_PLAINTEXT { return NX_TLS13_REC_VERDICT_TOO_LONG }
320
321 let nonce: *u8 = sys_mmap(16)
322 tls13_record_build_nonce(iv, seq, nonce)
323
324 let inner: *u8 = sys_mmap(ct_len + 16)
325 let v: i64 = tls13_record_aead_open(
326 cipher_suite,
327 key, nonce,
328 header, NX_TLS13_RECORD_HEADER_LEN,
329 ct, ct_len, tag,
330 inner
331 )
332 if v != 0 { return NX_TLS13_REC_VERDICT_TAG_MISMATCH }
333
334 // Strip trailing zero-padding to find the ContentType byte.
335 // Per RFC 8446 §5.4 the inner is content || type || zeros; we
336 // scan from the end stripping zeros until we hit the type byte.
337 var end: i64 = ct_len - 1
338 while end >= 0 {
339 if (inner[end] & 0xff) != 0 {
340 // Found the type byte.
341 *real_content_type_out = inner[end] & 0xff
342 *real_content_len_out = end
343 var k: i64 = 0
344 while k < end {
345 content_out[k] = inner[k]
346 k = k + 1
347 }
348 return NX_TLS13_REC_VERDICT_OK
349 }
350 end = end - 1
351 }
352 // All zeros -- no ContentType. Per RFC 8446 §5.4 this is a
353 // protocol violation (the unfounded-empty-record attack class).
354 return NX_TLS13_REC_VERDICT_EMPTY_INNER
355}
356
357// Legacy ChaCha20-only wrapper for back-compat with callers that
358// haven't been migrated to the cipher_suite-aware v2 entry point.
359func nx_tls13_record_decrypt(
360 key: *u8, iv: *u8, seq: i64,
361 header: *u8,
362 ct: *u8, ct_len: i64,
363 tag: *u8,
364 content_out: *u8,
365 real_content_type_out: *i64,
366 real_content_len_out: *i64
367) -> i64 {
368 return nx_tls13_record_decrypt_v2(
369 0x1303,
370 key, iv, seq, header, ct, ct_len, tag,
371 content_out, real_content_type_out, real_content_len_out
372 )
373}
374
375// Sealed-enum validity gate.
376func nx_tls13_rec_verdict_is_valid(v: i64) -> i64 {
377 if v < 0 { return 0 }
378 if v >= NX_TLS13_REC_VERDICT_N { return 0 }
379 return 1
380}