nx_hkdf_sha384.nx source
↩ module page · 101 lines · 3187 B
1// hkdf_sha384.nx -- HKDF-SHA-384 (RFC 5869).
2//
3// license_tier: INDEPENDENT_REDERIVE
4// genealogy_id: international-research-sources/ietf/rfc_5869
5//
6// Parallel to hkdf.nx but keyed on HMAC-SHA-384. Required for
7// TLS 1.3 cipher suites that use SHA-384 throughout the key
8// schedule (e.g. TLS_AES_256_GCM_SHA384 per RFC 8446 §B.4).
9//
10// Two-stage design (identical shape to hkdf.nx):
11// Extract(salt, IKM) -> PRK = HMAC-SHA-384(salt, IKM) [48-byte PRK]
12// Expand(PRK, info, L) -> OKM via counter-mode HMAC chain
13//
14// Output capacity: 255 * 48 = 12240 bytes. TLS 1.3 never needs
15// more than a few hundred, so this is ample.
16
17// nx_safety_envelope:
18// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
19// sil_target: SIL1
20// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
21// verdict: NOT_YET_EVALUATED
22
23import "nx_syscalls.nx"
24import "nx_hmac_sha384.nx"
25
26const HKDF384_HASH: i64 = 48
27const HKDF384_MAX_L: i64 = 12240
28
29func hkdf384_extract(salt: *u8, salt_len: i64,
30 ikm: *u8, ikm_len: i64,
31 prk: *u8) -> i64 {
32 if salt_len == 0 {
33 let zero_salt: *u8 = sys_mmap(HKDF384_HASH)
34 var i: i64 = 0
35 while i < HKDF384_HASH { zero_salt[i] = 0; i = i + 1 }
36 hmac_sha384(zero_salt, HKDF384_HASH, ikm, ikm_len, prk)
37 } else {
38 hmac_sha384(salt, salt_len, ikm, ikm_len, prk)
39 }
40 return 0
41}
42
43func hkdf384_expand(prk: *u8,
44 info: *u8, info_len: i64,
45 l: i64, out: *u8) -> i64 {
46 if l > HKDF384_MAX_L { return -1 }
47 if l < 0 { return -1 }
48
49 let t_prev: *u8 = sys_mmap(HKDF384_HASH)
50 let t_curr: *u8 = sys_mmap(HKDF384_HASH)
51 let buf_cap: i64 = HKDF384_HASH + info_len + 1
52 let buf: *u8 = sys_mmap(buf_cap)
53
54 var prev_len: i64 = 0
55 var produced: i64 = 0
56 var counter: i64 = 1
57 while produced < l {
58 var bi: i64 = 0
59 var k: i64 = 0
60 while k < prev_len { buf[bi + k] = t_prev[k]; k = k + 1 }
61 bi = bi + prev_len
62 k = 0
63 while k < info_len { buf[bi + k] = info[k]; k = k + 1 }
64 bi = bi + info_len
65 buf[bi] = counter & 0xFF
66 bi = bi + 1
67
68 hmac_sha384(prk, HKDF384_HASH, buf, bi, t_curr)
69
70 let remain: i64 = l - produced
71 var take: i64 = HKDF384_HASH
72 if remain < HKDF384_HASH { take = remain }
73 k = 0
74 while k < take { out[produced + k] = t_curr[k]; k = k + 1 }
75 produced = produced + take
76
77 k = 0
78 while k < HKDF384_HASH { t_prev[k] = t_curr[k]; k = k + 1 }
79 prev_len = HKDF384_HASH
80 counter = counter + 1
81 }
82 return 0
83}
84
85func main() -> i64 {
86 let ikm: *u8 = sys_mmap(22)
87 let salt: *u8 = sys_mmap(13)
88 let info: *u8 = sys_mmap(10)
89 let prk: *u8 = sys_mmap(48)
90 let okm: *u8 = sys_mmap(64)
91 var i: i64 = 0
92 while i < 22 { ikm[i] = 0x0B; i = i + 1 }
93 i = 0
94 while i < 13 { salt[i] = i as i64; i = i + 1 }
95 i = 0
96 while i < 10 { info[i] = 0xF0 + (i as i64); i = i + 1 }
97
98 hkdf384_extract(salt, 13, ikm, 22, prk)
99 hkdf384_expand(prk, info, 10, 64, okm)
100 return okm[0] as i64
101}