nx_hkdf_sha512.nx source
↩ module page · 99 lines · 3019 B
1// hkdf_sha512.nx -- HKDF-SHA-512 (RFC 5869).
2//
3// Final HKDF variant, parallel to hkdf.nx (SHA-256) and
4// hkdf_sha384.nx (SHA-384). Used where a downstream primitive
5// requires the full 512-bit output width or where the whole key
6// ladder is anchored on SHA-512.
7//
8// Output capacity: 255 * 64 = 16320 bytes. Ample for any TLS /
9// SSH session derivation.
10//
11// license_tier: INDEPENDENT_REDERIVE
12// genealogy_id: international-research-sources/ietf/rfc_5869
13//
14
15// nx_safety_envelope:
16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
17// sil_target: SIL1
18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
19// verdict: NOT_YET_EVALUATED
20
21import "nx_syscalls.nx"
22import "nx_hmac_sha512.nx"
23
24const HKDF512_HASH: i64 = 64
25const HKDF512_MAX_L: i64 = 16320
26
27func hkdf512_extract(salt: *u8, salt_len: i64,
28 ikm: *u8, ikm_len: i64,
29 prk: *u8) -> i64 {
30 if salt_len == 0 {
31 let zero_salt: *u8 = sys_mmap(HKDF512_HASH)
32 var i: i64 = 0
33 while i < HKDF512_HASH { zero_salt[i] = 0; i = i + 1 }
34 hmac_sha512(zero_salt, HKDF512_HASH, ikm, ikm_len, prk)
35 } else {
36 hmac_sha512(salt, salt_len, ikm, ikm_len, prk)
37 }
38 return 0
39}
40
41func hkdf512_expand(prk: *u8,
42 info: *u8, info_len: i64,
43 l: i64, out: *u8) -> i64 {
44 if l > HKDF512_MAX_L { return -1 }
45 if l < 0 { return -1 }
46
47 let t_prev: *u8 = sys_mmap(HKDF512_HASH)
48 let t_curr: *u8 = sys_mmap(HKDF512_HASH)
49 let buf_cap: i64 = HKDF512_HASH + info_len + 1
50 let buf: *u8 = sys_mmap(buf_cap)
51
52 var prev_len: i64 = 0
53 var produced: i64 = 0
54 var counter: i64 = 1
55 while produced < l {
56 var bi: i64 = 0
57 var k: i64 = 0
58 while k < prev_len { buf[bi + k] = t_prev[k]; k = k + 1 }
59 bi = bi + prev_len
60 k = 0
61 while k < info_len { buf[bi + k] = info[k]; k = k + 1 }
62 bi = bi + info_len
63 buf[bi] = counter & 0xFF
64 bi = bi + 1
65
66 hmac_sha512(prk, HKDF512_HASH, buf, bi, t_curr)
67
68 let remain: i64 = l - produced
69 var take: i64 = HKDF512_HASH
70 if remain < HKDF512_HASH { take = remain }
71 k = 0
72 while k < take { out[produced + k] = t_curr[k]; k = k + 1 }
73 produced = produced + take
74
75 k = 0
76 while k < HKDF512_HASH { t_prev[k] = t_curr[k]; k = k + 1 }
77 prev_len = HKDF512_HASH
78 counter = counter + 1
79 }
80 return 0
81}
82
83func main() -> i64 {
84 let ikm: *u8 = sys_mmap(22)
85 let salt: *u8 = sys_mmap(13)
86 let info: *u8 = sys_mmap(10)
87 let prk: *u8 = sys_mmap(64)
88 let okm: *u8 = sys_mmap(128)
89 var i: i64 = 0
90 while i < 22 { ikm[i] = 0x0B; i = i + 1 }
91 i = 0
92 while i < 13 { salt[i] = i as i64; i = i + 1 }
93 i = 0
94 while i < 10 { info[i] = 0xF0 + (i as i64); i = i + 1 }
95
96 hkdf512_extract(salt, 13, ikm, 22, prk)
97 hkdf512_expand(prk, info, 10, 128, okm)
98 return okm[0] as i64
99}