nx_tls13_record.nx source
↩ module page · 412 lines · 16768 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
97
98// ---- REQUEST FRAGMENTATION ARITHMETIC (pure, therefore GATEABLE without a socket) -----------------
99// RFC 8446 5.1 bounds a record at 2^14 bytes of plaintext, and the inner plaintext adds one
100// content-type byte -- so the largest CONTENT a record may carry is NX_TLS13_MAX_INNER_PLAINTEXT - 1.
101// A caller sending more than that must split across records.
102//
103// WHY THESE ARE FUNCTIONS AND NOT A LOOP BODY: the split used to be three inline expressions inside
104// nx_https_req_complete, behind a live TLS session, which meant the only way to test it was to open a
105// socket -- and a gate that opens a socket goes RED when someone else's network does. Pulled out here
106// they are pure integer arithmetic over one argument, so a gate can walk the boundary exhaustively.
107// The bound is READ from the constant above rather than restated: a second 16384 anywhere in this
108// estate is the duplicate-ruler defect, and it drifts the moment either copy is touched.
109func nx_tls13_frag_max() -> i64 { return NX_TLS13_MAX_INNER_PLAINTEXT - 1 }
110
111// Bytes carried by the record that starts at `off`. Zero when the request is already exhausted.
112func nx_tls13_frag_len(req_len: i64, off: i64) -> i64 {
113 if req_len <= 0 { return 0 }
114 if off >= req_len { return 0 }
115 if off < 0 { return 0 }
116 let m: i64 = nx_tls13_frag_max()
117 var f: i64 = req_len - off
118 if f > m { f = m }
119 return f
120}
121
122// How many records a request of req_len bytes needs. An EMPTY request needs none -- stated explicitly
123// because ceiling division of zero is the case every hand-rolled version gets wrong.
124func nx_tls13_frag_count(req_len: i64) -> i64 {
125 if req_len <= 0 { return 0 }
126 let m: i64 = nx_tls13_frag_max()
127 return (req_len + m - 1) / m
128}
129const NX_TLS13_MAX_RECORD_PAYLOAD: i64 = 16640 // 2^14 + 256
130
131// ContentType values relevant to the record layer (RFC 8446 §5.1, §B.1).
132const NX_TLS13_CT_INVALID: i64 = 0
133const NX_TLS13_CT_CHANGE_CIPHER_SPEC: i64 = 20
134const NX_TLS13_CT_ALERT: i64 = 21
135const NX_TLS13_CT_HANDSHAKE: i64 = 22
136const NX_TLS13_CT_APPLICATION_DATA: i64 = 23
137
138const NX_TLS13_LEGACY_VERSION: i64 = 0x0303
139
140// Sealed record verdict.
141const NX_TLS13_REC_VERDICT_OK: i64 = 1
142const NX_TLS13_REC_VERDICT_TAG_MISMATCH: i64 = 2
143const NX_TLS13_REC_VERDICT_BAD_PADDING: i64 = 3
144const NX_TLS13_REC_VERDICT_EMPTY_INNER: i64 = 4
145const NX_TLS13_REC_VERDICT_TOO_LONG: i64 = 5
146const NX_TLS13_REC_VERDICT_TOO_SHORT: i64 = 6
147const NX_TLS13_REC_VERDICT_N: i64 = 7
148
149// Compute the per-record nonce per RFC 8446 §5.3.
150// nonce[0..3] = static_iv[0..3] ^ 0 (seq high bytes zero-padded)
151// nonce[4..12] = static_iv[4..12] ^ seq_num_big_endian
152//
153// In other words: left-pad seq to 12 bytes (4 zero bytes + 8-byte
154// big-endian seq) then XOR against static_iv elementwise.
155func tls13_record_build_nonce(static_iv: *u8, seq: i64, nonce_out: *u8) -> i64 {
156 nonce_out[0] = static_iv[0] & 0xff
157 nonce_out[1] = static_iv[1] & 0xff
158 nonce_out[2] = static_iv[2] & 0xff
159 nonce_out[3] = static_iv[3] & 0xff
160 nonce_out[4] = (static_iv[4] & 0xff) ^ ((seq >> 56) & 0xff)
161 nonce_out[5] = (static_iv[5] & 0xff) ^ ((seq >> 48) & 0xff)
162 nonce_out[6] = (static_iv[6] & 0xff) ^ ((seq >> 40) & 0xff)
163 nonce_out[7] = (static_iv[7] & 0xff) ^ ((seq >> 32) & 0xff)
164 nonce_out[8] = (static_iv[8] & 0xff) ^ ((seq >> 24) & 0xff)
165 nonce_out[9] = (static_iv[9] & 0xff) ^ ((seq >> 16) & 0xff)
166 nonce_out[10] = (static_iv[10] & 0xff) ^ ((seq >> 8) & 0xff)
167 nonce_out[11] = (static_iv[11] & 0xff) ^ ( seq & 0xff)
168 return 0
169}
170
171// Write the 5-byte TLSCiphertext header. total_len = length of the
172// AEAD-encrypted payload (ciphertext + tag). This IS the additional
173// authenticated data fed to the AEAD.
174func tls13_record_write_header(header_out: *u8, total_len: i64) -> i64 {
175 header_out[0] = NX_TLS13_CT_APPLICATION_DATA & 0xff
176 header_out[1] = (NX_TLS13_LEGACY_VERSION >> 8) & 0xff
177 header_out[2] = NX_TLS13_LEGACY_VERSION & 0xff
178 header_out[3] = (total_len >> 8) & 0xff
179 header_out[4] = total_len & 0xff
180 return NX_TLS13_RECORD_HEADER_LEN
181}
182
183// Encrypt a TLS 1.3 application record.
184//
185// Inputs:
186// key, iv = traffic_key and traffic_iv from nx_tls13_schedule
187// seq = per-direction sequence number (caller increments)
188// content, content_len, real_content_type = the plaintext + its
189// actual ContentType (handshake/alert/application)
190// padding_len = optional zero-byte padding (length-hiding); 0 = none
191// header_out = 5-byte TLSCiphertext header (caller buffer)
192// ct_out = ciphertext buffer (must hold content_len + 1 + padding_len)
193// tag_out = 16-byte AEAD tag buffer
194//
195// Returns NX_TLS13_REC_VERDICT_OK or a sealed non-OK verdict.
196// AEAD dispatcher. Routes to ChaCha20-Poly1305 (0x1303) or
197// AES-128-GCM (0x1301) per RFC 8446 §5.2. Wired 2026-05-20 after
198// the IR-extension + silent-dropping fix landed (AES seal/open are
199// 8-arg primitives; previously >6-arg path silently dropped args).
200// Per [[feedback-c-is-wheeler-test-only]]: substrate is daily-driver.
201//
202// Unknown cipher_suite returns -2 (NX_AEAD_VERDICT_BAD_CIPHER) so
203// caller can surface a clean error instead of garbling bytes.
204func tls13_record_aead_seal(cipher_suite: i64,
205 key: *u8, nonce: *u8,
206 aad: *u8, aad_len: i64,
207 pt: *u8, pt_len: i64,
208 ct_out: *u8, tag_out: *u8) -> i64 {
209 if cipher_suite == 0x1303 {
210 let v: i64 = nx_chacha20_poly1305_encrypt(
211 key, nonce, aad, aad_len, pt, pt_len, ct_out, tag_out
212 )
213 if v != NX_AEAD_VERDICT_OK { return 0 - 1 }
214 return 0
215 }
216 if cipher_suite == 0x1301 {
217 let v: i64 = nx_aes128_gcm_seal(
218 key, nonce, aad, aad_len, pt, pt_len, ct_out, tag_out
219 )
220 if v != 0 { return 0 - 1 }
221 return 0
222 }
223 // 0x1302 AES-256-GCM-SHA384 (2026-08-05). ADDITIVE and UNREACHABLE until
224 // recv_sh accepts the suite -- so the blast radius of a defect here is exactly
225 // the set of hosts that are 100% unreachable today. key is 32 bytes (AES-256),
226 // nonce 12; the SHA-384 half of the KEY SCHEDULE is the remaining rung.
227 if cipher_suite == 0x1302 {
228 let v: i64 = nx_aes256_gcm_seal(
229 key, nonce, aad, aad_len, pt, pt_len, ct_out, tag_out
230 )
231 if v != 0 { return 0 - 1 }
232 return 0
233 }
234 return 0 - 2 // BAD_CIPHER
235}
236
237func tls13_record_aead_open(cipher_suite: i64,
238 key: *u8, nonce: *u8,
239 aad: *u8, aad_len: i64,
240 ct: *u8, ct_len: i64, tag: *u8,
241 pt_out: *u8) -> i64 {
242 if cipher_suite == 0x1303 {
243 let v: i64 = nx_chacha20_poly1305_decrypt(
244 key, nonce, aad, aad_len, ct, ct_len, tag, pt_out
245 )
246 if v != NX_AEAD_VERDICT_OK { return 0 - 1 }
247 return 0
248 }
249 if cipher_suite == 0x1301 {
250 let v: i64 = nx_aes128_gcm_open(
251 key, nonce, aad, aad_len, ct, ct_len, tag, pt_out
252 )
253 if v != 0 { return 0 - 1 }
254 return 0
255 }
256 if cipher_suite == 0x1302 {
257 let v: i64 = nx_aes256_gcm_open(
258 key, nonce, aad, aad_len, ct, ct_len, tag, pt_out
259 )
260 if v != 0 { return 0 - 1 }
261 return 0
262 }
263 return 0 - 2 // BAD_CIPHER
264}
265
266// Cipher-suite-aware encrypt. cipher_suite is the TLS 1.3 wire value
267// (0x1301 = AES-128-GCM-SHA256, 0x1303 = ChaCha20-Poly1305-SHA256).
268func nx_tls13_record_encrypt_v2(
269 cipher_suite: i64,
270 key: *u8, iv: *u8, seq: i64,
271 content: *u8, content_len: i64,
272 real_content_type: i64,
273 padding_len: i64,
274 header_out: *u8,
275 ct_out: *u8,
276 tag_out: *u8
277) -> i64 {
278 let inner_len: i64 = content_len + 1 + padding_len
279 if inner_len > NX_TLS13_MAX_INNER_PLAINTEXT { return NX_TLS13_REC_VERDICT_TOO_LONG }
280 if content_len < 0 { return NX_TLS13_REC_VERDICT_TOO_SHORT }
281 if padding_len < 0 { return NX_TLS13_REC_VERDICT_BAD_PADDING }
282
283 let inner: *u8 = sys_mmap(inner_len + 16)
284 var i: i64 = 0
285 while i < content_len { inner[i] = content[i]; i = i + 1 }
286 inner[content_len] = real_content_type & 0xff
287 var p: i64 = 0
288 while p < padding_len { inner[content_len + 1 + p] = 0; p = p + 1 }
289
290 let total_payload: i64 = inner_len + NX_TLS13_RECORD_TAG_LEN
291 tls13_record_write_header(header_out, total_payload)
292
293 let nonce: *u8 = sys_mmap(16)
294 tls13_record_build_nonce(iv, seq, nonce)
295
296 let v: i64 = tls13_record_aead_seal(
297 cipher_suite,
298 key, nonce,
299 header_out, NX_TLS13_RECORD_HEADER_LEN,
300 inner, inner_len,
301 ct_out, tag_out
302 )
303 if v != 0 { return NX_TLS13_REC_VERDICT_TAG_MISMATCH }
304 return NX_TLS13_REC_VERDICT_OK
305}
306
307// Legacy ChaCha20-only wrapper for back-compat with callers that
308// haven't been migrated to the cipher_suite-aware v2 entry point.
309func nx_tls13_record_encrypt(
310 key: *u8, iv: *u8, seq: i64,
311 content: *u8, content_len: i64,
312 real_content_type: i64,
313 padding_len: i64,
314 header_out: *u8,
315 ct_out: *u8,
316 tag_out: *u8
317) -> i64 {
318 return nx_tls13_record_encrypt_v2(
319 0x1303,
320 key, iv, seq, content, content_len,
321 real_content_type, padding_len,
322 header_out, ct_out, tag_out
323 )
324}
325
326// Decrypt a TLS 1.3 application record.
327//
328// Inputs:
329// key, iv, seq = as encrypt
330// header = the 5 received bytes (used as AAD; caller MUST pass
331// the literal bytes seen on the wire)
332// ct, ct_len = encrypted record body (inner_len bytes; tag follows)
333// tag = 16-byte received tag
334// content_out = caller buffer >= ct_len (we strip type + padding)
335// real_content_type_out = *i64 to receive the real ContentType
336// real_content_len_out = *i64 to receive bytes written to content_out
337//
338// On TAG_MISMATCH the content/type/len outputs are NOT written
339// (caller must not read them). Tag check is constant-time first.
340func nx_tls13_record_decrypt_v2(
341 cipher_suite: i64,
342 key: *u8, iv: *u8, seq: i64,
343 header: *u8,
344 ct: *u8, ct_len: i64,
345 tag: *u8,
346 content_out: *u8,
347 real_content_type_out: *i64,
348 real_content_len_out: *i64
349) -> i64 {
350 if ct_len < 1 { return NX_TLS13_REC_VERDICT_TOO_SHORT }
351 if ct_len > NX_TLS13_MAX_INNER_PLAINTEXT { return NX_TLS13_REC_VERDICT_TOO_LONG }
352
353 let nonce: *u8 = sys_mmap(16)
354 tls13_record_build_nonce(iv, seq, nonce)
355
356 let inner: *u8 = sys_mmap(ct_len + 16)
357 let v: i64 = tls13_record_aead_open(
358 cipher_suite,
359 key, nonce,
360 header, NX_TLS13_RECORD_HEADER_LEN,
361 ct, ct_len, tag,
362 inner
363 )
364 if v != 0 { return NX_TLS13_REC_VERDICT_TAG_MISMATCH }
365
366 // Strip trailing zero-padding to find the ContentType byte.
367 // Per RFC 8446 §5.4 the inner is content || type || zeros; we
368 // scan from the end stripping zeros until we hit the type byte.
369 var end: i64 = ct_len - 1
370 while end >= 0 {
371 if (inner[end] & 0xff) != 0 {
372 // Found the type byte.
373 *real_content_type_out = inner[end] & 0xff
374 *real_content_len_out = end
375 var k: i64 = 0
376 while k < end {
377 content_out[k] = inner[k]
378 k = k + 1
379 }
380 return NX_TLS13_REC_VERDICT_OK
381 }
382 end = end - 1
383 }
384 // All zeros -- no ContentType. Per RFC 8446 §5.4 this is a
385 // protocol violation (the unfounded-empty-record attack class).
386 return NX_TLS13_REC_VERDICT_EMPTY_INNER
387}
388
389// Legacy ChaCha20-only wrapper for back-compat with callers that
390// haven't been migrated to the cipher_suite-aware v2 entry point.
391func nx_tls13_record_decrypt(
392 key: *u8, iv: *u8, seq: i64,
393 header: *u8,
394 ct: *u8, ct_len: i64,
395 tag: *u8,
396 content_out: *u8,
397 real_content_type_out: *i64,
398 real_content_len_out: *i64
399) -> i64 {
400 return nx_tls13_record_decrypt_v2(
401 0x1303,
402 key, iv, seq, header, ct, ct_len, tag,
403 content_out, real_content_type_out, real_content_len_out
404 )
405}
406
407// Sealed-enum validity gate.
408func nx_tls13_rec_verdict_is_valid(v: i64) -> i64 {
409 if v < 0 { return 0 }
410 if v >= NX_TLS13_REC_VERDICT_N { return 0 }
411 return 1
412}