nx_tls13_hrr.nx source

1// nx_tls13_hrr.nx -- HelloRetryRequest detection (RFC 8446 §4.1.4). 2// 3// Phase 0b §G of the Nishi TLS 1.3 stack per 4// docs/NISHI_TLS13_GAP_AUDIT.md. The trivial-but-load-bearing 5// detector that distinguishes a real ServerHello from a 6// HelloRetryRequest -- which arrives on the wire formatted 7// IDENTICALLY to a ServerHello but uses a specific magic value in 8// the Random field. 9// 10// Per RFC 8446 §4.1.3: 11// 12// When sent by the server in response to a ClientHello to request 13// a different key share or to update the cookie, HelloRetryRequest 14// has the same structure as ServerHello but with Random set to the 15// special value of the SHA-256 of "HelloRetryRequest": 16// 17// CF 21 AD 74 E5 9A 61 11 BE 1D 8C 02 1E 65 B8 91 18// C2 A2 11 16 7A BB 8C 5E 07 9E 09 E2 C8 A8 33 9C 19// 20// Receiving a ServerHello with the legacy Random matching this 21// value MUST be treated as a HelloRetryRequest. 22// 23// When the detector returns 1, the caller MUST: 24// 1. Call nx_tls13_transcript_replace_with_hrr (already shipped 25// Gap E) to substitute the original ClientHello with the 26// synthetic message_hash record 27// 2. Emit a new ClientHello with whatever the HRR's extensions 28// asked us to change (typically a different key_share group; 29// the supported_groups extension in the HRR tells us which) 30// 31// This module DOES NOT do either of the above -- it just gives the 32// caller's state machine the boolean it needs to fork on. The 33// rewrite of the transcript + emission of CH2 belongs in the state 34// machine driver (Gap L). 35// 36// What it does today: 37// - fill caller buffer with the 32-byte HRR magic random 38// - boolean: is the message we just received actually HRR? 39// 40// What it doesn't do yet: 41// - parse the cookie extension (RFC 8446 §4.2.2; HRR can carry 42// one and CH2 MUST echo it) 43// - parse the "what group does the server prefer" hint (it 44// comes via a key_share extension whose body is just the 45// selected NamedGroup, no actual key) 46// 47// KAT verified: 48// - tls13_hrr_magic_random fills exact 32 spec bytes 49// - hand-built ServerHello with HRR random -> is_hrr returns 1 50// - hand-built ServerHello with normal random -> is_hrr returns 0 51// - malformed ServerHello (wrong msg_type, truncated) -> is_hrr returns 0 52// 53// Composes with: 54// - nx_tls13_hello (uses tls13_server_hello_parse + the random offset) 55// - nx_tls13_transcript (caller plugs replace_with_hrr after detect) 56// 57// license_tier: INDEPENDENT_REDERIVE 58// genealogy_id: international-research-sources/ietf/rfc_8446 59// lineage_id: nishi_tls13_hrr_q10 60 61// nx_safety_envelope: 62// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 63// sil_target: SIL1 64// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 65// verdict: NOT_YET_EVALUATED 66 67import "nx_syscalls.nx" 68import "nx_tls13_hello.nx" 69 70// Fill `out_32` with the HRR magic Random bytes per RFC 8446 §4.1.3. 71func tls13_hrr_magic_random(out_32: *u8) -> i64 { 72 out_32[0]=0xcf; out_32[1]=0x21; out_32[2]=0xad; out_32[3]=0x74 73 out_32[4]=0xe5; out_32[5]=0x9a; out_32[6]=0x61; out_32[7]=0x11 74 out_32[8]=0xbe; out_32[9]=0x1d; out_32[10]=0x8c; out_32[11]=0x02 75 out_32[12]=0x1e; out_32[13]=0x65; out_32[14]=0xb8; out_32[15]=0x91 76 out_32[16]=0xc2; out_32[17]=0xa2; out_32[18]=0x11; out_32[19]=0x16 77 out_32[20]=0x7a; out_32[21]=0xbb; out_32[22]=0x8c; out_32[23]=0x5e 78 out_32[24]=0x07; out_32[25]=0x9e; out_32[26]=0x09; out_32[27]=0xe2 79 out_32[28]=0xc8; out_32[29]=0xa8; out_32[30]=0x33; out_32[31]=0x9c 80 return 0 81} 82 83// Return 1 if `buf[0..n]` is a ServerHello whose Random matches the 84// HRR magic value (i.e. it's actually a HelloRetryRequest), 0 if 85// it's a normal ServerHello, and 0 if it fails to parse as a 86// ServerHello at all (malformed bytes are NOT HRR by definition). 87// 88// Caller may still want to call tls13_server_hello_parse separately 89// to extract structure offsets; this function intentionally swallows 90// parse errors so the caller's state machine doesn't have to special- 91// case "is HRR but also TRUNCATED." 92func tls13_hello_is_hrr(buf: *u8, n: i64) -> i64 { 93 let lv: *i64 = sys_mmap(16) as *i64 94 let ro: *i64 = sys_mmap(16) as *i64 95 let cs: *i64 = sys_mmap(16) as *i64 96 let eo: *i64 = sys_mmap(16) as *i64 97 let el: *i64 = sys_mmap(16) as *i64 98 let v: i64 = tls13_server_hello_parse(buf, n, lv, ro, cs, eo, el) 99 if v != NX_TLS13_HELLO_VERDICT_OK { return 0 } 100 let magic: *u8 = sys_mmap(64) 101 tls13_hrr_magic_random(magic) 102 var i: i64 = 0 103 while i < 32 { 104 if (buf[(*ro) + i] & 0xff) != (magic[i] & 0xff) { return 0 } 105 i = i + 1 106 } 107 return 1 108}