nx_hkdf.nx source

1// hkdf.nx -- HKDF-SHA-256 (RFC 5869). 2// 3// HMAC-based Extract-and-Expand Key Derivation Function. Central 4// to TLS 1.3 (RFC 8446 §7.1) key schedule: 5// 6// Early Secret = HKDF-Extract(0, PSK) 7// Handshake Secret = HKDF-Extract(Derive-Secret(Early, ""), ECDHE) 8// Master Secret = HKDF-Extract(Derive-Secret(Handshake, ""), 0) 9// <traffic secrets> = Derive-Secret(<stage>, "<label>", transcript) 10// 11// Two-stage design: 12// Extract(salt, IKM) -> PRK 13// Treats IKM as an entropy source; produces a uniformly-random 14// pseudorandom key. Implemented as HMAC-SHA-256(salt, IKM). 15// Expand(PRK, info, L) -> OKM 16// Deterministically derives L bytes of keying material from PRK 17// and a context string `info`. Iterates HMAC over a counter. 18// 19// Properties (RFC 5869 §3.3): 20// - Deterministic: same (salt, IKM, info, L) -> same OKM. 21// - Context-binding: different `info` -> independent OKMs. 22// - Output limited to 255 * HashLen = 8160 bytes for SHA-256. 23// 24// Invariants: 25// HK1 PRK is always exactly HashLen (32 bytes for SHA-256). 26// HK2 Expand iterates exactly ceil(L / HashLen) times; each 27// iteration feeds the previous output back in, creating a 28// chain that prevents block-substitution attacks. 29// HK3 Counter bytes are 1-indexed; wraps at 255 per RFC 5869 30// §2.3. We cap L at 8160 and refuse larger requests. 31// HK4 No branches on salt/IKM/info VALUES; branches only on 32// LENGTHS. 33// 34// license_tier: INDEPENDENT_REDERIVE 35// genealogy_id: international-research-sources/ietf/rfc_5869 36// 37// nx_safety_envelope: (schema: nishi-library/seeds/safety-critical-standards.toml) 38// intended_use: "HKDF-SHA-256 key derivation -- TLS 1.3 39// record-protection schedule (RFC 8446 §7.1) + 40// Noise protocol KDF + any KDF needing 41// Extract-then-Expand pattern" 42// sil_target: SIL3 (key derivation; output reused 43// across security boundaries) 44// asil_target: QM 45// dal_target: DAL B 46// iec_62304_class: B 47// evidence: [no_floating_point, sealed_enum_complete, 48// bit_equal_reproducible, 49// RFC_5869_test_vectors_A1_A2_A3_VERIFIED, 50// inherits_nx_hmac_evidence_chain, 51// constant_time_by_construction] 52// hazard_register: [bug-tape-info-string-concat-injection, 53// bug-tape-okm-length-exceeds-255-blocks, 54// bug-tape-salt-not-domain-separated] 55// residual_risk: "info context string MUST be domain- 56// separated by caller (RFC 5869 §3.2); 57// substrate cannot enforce uniqueness across 58// protocol versions. okm_len capped at 59// 255*HashLen by RFC 5869 §2.3." 60// verdict: NOT_YET_EVALUATED 61 62import "nx_syscalls.nx" 63import "nx_hmac.nx" 64import "nx_hmac_sha384.nx" 65 66const HKDF_HASH: i64 = 32 // SHA-256 output 67const HKDF_MAX_L: i64 = 8160 // 255 * 32 68const HKDF_HASH384: i64 = 48 // SHA-384 output 69const HKDF_MAX_L384: i64 = 12240 // 255 * 48 70 71// HKDF-Extract. Writes 32-byte PRK to `prk`. `salt` may be NULL 72// (caller passes zero pointer + salt_len=0) in which case RFC 5869 73// mandates a zero-filled HashLen salt. 74func hkdf_extract(salt: *u8, salt_len: i64, 75 ikm: *u8, ikm_len: i64, 76 prk: *u8) -> i64 { 77 if salt_len == 0 { 78 let zero_salt: *u8 = sys_mmap(HKDF_HASH) 79 var i: i64 = 0 80 while i < HKDF_HASH { zero_salt[i] = 0; i = i + 1 } 81 hmac_sha256(zero_salt, HKDF_HASH, ikm, ikm_len, prk) 82 } else { 83 hmac_sha256(salt, salt_len, ikm, ikm_len, prk) 84 } 85 return 0 86} 87 88// HKDF-Expand. Writes `L` bytes of keying material to `out`. 89// Returns 0 on success, -1 if L exceeds the HKDF ceiling. 90func hkdf_expand(prk: *u8, 91 info: *u8, info_len: i64, 92 l: i64, out: *u8) -> i64 { 93 if l > HKDF_MAX_L { return -1 } 94 if l < 0 { return -1 } 95 96 // n = ceil(L / HashLen); each iteration appends one block. 97 // T(0) = empty; T(i) = HMAC(PRK, T(i-1) || info || i_byte). 98 let t_prev: *u8 = sys_mmap(HKDF_HASH) 99 let t_curr: *u8 = sys_mmap(HKDF_HASH) 100 let buf_cap: i64 = HKDF_HASH + info_len + 1 101 let buf: *u8 = sys_mmap(buf_cap) 102 103 var prev_len: i64 = 0 104 var produced: i64 = 0 105 var counter: i64 = 1 106 while produced < l { 107 // Build input: T(i-1) || info || counter 108 var bi: i64 = 0 109 var k: i64 = 0 110 while k < prev_len { buf[bi + k] = t_prev[k]; k = k + 1 } 111 bi = bi + prev_len 112 k = 0 113 while k < info_len { buf[bi + k] = info[k]; k = k + 1 } 114 bi = bi + info_len 115 buf[bi] = counter & 0xFF 116 bi = bi + 1 117 118 hmac_sha256(prk, HKDF_HASH, buf, bi, t_curr) 119 120 // Copy up to HashLen bytes of T(i) into output. 121 let remain: i64 = l - produced 122 var take: i64 = HKDF_HASH 123 if remain < HKDF_HASH { take = remain } 124 k = 0 125 while k < take { out[produced + k] = t_curr[k]; k = k + 1 } 126 produced = produced + take 127 128 // T(i) becomes T(i-1) for next round. 129 k = 0 130 while k < HKDF_HASH { t_prev[k] = t_curr[k]; k = k + 1 } 131 prev_len = HKDF_HASH 132 counter = counter + 1 133 } 134 return 0 135} 136 137// ===== HASH-PARAMETERIZED HKDF (2026-08-03) ========================== 138// WHY: TLS 1.3 cipher suite 0x1302 (AES-256-GCM-SHA384) uses SHA-384 for 139// the ENTIRE key schedule, not just the AEAD. Our client offered 0x1302 140// and then could not derive its keys -- servers that prefer it (VaM hub 141// among them) were unreachable, and the failure surfaced as a bare 142// handshake verdict=5. The primitives all existed: hmac_sha384 (this 143// module's new import), sha384_digest, nx_aes256_gcm_seal/open. The gap 144// was WIRING, not capability -- the banked adoption-gap class again. 145// 146// ADDITIVE BY CONSTRUCTION (Rule 19): the original hkdf_extract/expand 147// are UNTOUCHED above and remain the SHA-256 path every existing caller 148// already links; these _h twins take hash_len and dispatch. A caller that 149// passes 32 gets byte-identical output to the original -- asserted as a 150// regression tooth, not assumed. 151// 152// hash_len is REFUSED unless 32 or 48: a silent fallback to SHA-256 on an 153// unknown length would derive the WRONG keys and present as a decrypt 154// failure three layers away. Fail closed, at the definition site. 155 156// HKDF-Extract, hash-parameterized. PRK is exactly hash_len bytes. 157// Extract IS HMAC(salt, IKM) by definition (RFC 5869 s2.2), so this 158// stays a pure dispatch -- there is no second construction to get wrong. 159func hkdf_extract_h(salt: *u8, salt_len: i64, 160 ikm: *u8, ikm_len: i64, 161 hash_len: i64, prk: *u8) -> i64 { 162 if hash_len != HKDF_HASH { if hash_len != HKDF_HASH384 { return 0 - 2 } } 163 if salt_len == 0 { 164 let zero_salt: *u8 = sys_mmap(hash_len) 165 var i: i64 = 0 166 while i < hash_len { zero_salt[i] = 0; i = i + 1 } 167 if hash_len == HKDF_HASH384 { 168 hmac_sha384(zero_salt, hash_len, ikm, ikm_len, prk) 169 } else { 170 hmac_sha256(zero_salt, hash_len, ikm, ikm_len, prk) 171 } 172 return 0 173 } 174 if hash_len == HKDF_HASH384 { 175 hmac_sha384(salt, salt_len, ikm, ikm_len, prk) 176 } else { 177 hmac_sha256(salt, salt_len, ikm, ikm_len, prk) 178 } 179 return 0 180} 181 182// HKDF-Expand, hash-parameterized. The RFC 5869 s2.3 chain is identical 183// for either hash; only the block size and the 255-block ceiling move. 184func hkdf_expand_h(prk: *u8, hash_len: i64, 185 info: *u8, info_len: i64, 186 l: i64, out: *u8) -> i64 { 187 if hash_len != HKDF_HASH { if hash_len != HKDF_HASH384 { return 0 - 2 } } 188 var maxl: i64 = HKDF_MAX_L 189 if hash_len == HKDF_HASH384 { maxl = HKDF_MAX_L384 } 190 if l > maxl { return 0 - 1 } 191 if l < 0 { return 0 - 1 } 192 193 let t_prev: *u8 = sys_mmap(hash_len) 194 let t_curr: *u8 = sys_mmap(hash_len) 195 let buf_cap: i64 = hash_len + info_len + 1 196 let buf: *u8 = sys_mmap(buf_cap) 197 198 var prev_len: i64 = 0 199 var produced: i64 = 0 200 var counter: i64 = 1 201 while produced < l { 202 var bi: i64 = 0 203 var k: i64 = 0 204 while k < prev_len { buf[bi + k] = t_prev[k]; k = k + 1 } 205 bi = bi + prev_len 206 k = 0 207 while k < info_len { buf[bi + k] = info[k]; k = k + 1 } 208 bi = bi + info_len 209 buf[bi] = counter & 0xFF 210 bi = bi + 1 211 212 if hash_len == HKDF_HASH384 { 213 hmac_sha384(prk, hash_len, buf, bi, t_curr) 214 } else { 215 hmac_sha256(prk, hash_len, buf, bi, t_curr) 216 } 217 218 let remain: i64 = l - produced 219 var take: i64 = hash_len 220 if remain < hash_len { take = remain } 221 k = 0 222 while k < take { out[produced + k] = t_curr[k]; k = k + 1 } 223 produced = produced + take 224 225 k = 0 226 while k < hash_len { t_prev[k] = t_curr[k]; k = k + 1 } 227 prev_len = hash_len 228 counter = counter + 1 229 } 230 return 0 231} 232 233// Real KAT execution lives in runtime/nx_hkdf_test.nx (RFC 5869 234// §A.1-A.3, three worked SHA-256 examples). Removed stub main so 235// importing this module from a test or TLS-KDF file doesn't 236// double-define main. 237// SHA-384 coverage: runtime/_hdl_build/nx_hkdf384_gate.nx -- RFC 5869 A.1 238// through the new path (published vector), plus DEFINITIONAL identities 239// recomputed in the gate. No HKDF-SHA-384 test vector is published in RFC 240// 5869, and inventing one would be fabrication wearing a citation.