`hkdf.nx` source

↩ module page · 126 lines · 4698 B
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
34import "syscalls.nx"
35import "nx_hmac.nx"   // was hmac.nx -- CODE-IDENTICAL twin (49/49 stmts) on the LEGACY syscalls.nx+sha256.nx family.
36// Two files defining hmac_sha256 + main, with the expander deduping BY PATH NOT BY SYMBOL, made
37// every legacy importer a duplicate-symbol landmine for the nx_ family (debt 1785524913).
38
39const HKDF_HASH: i64 = 32    // SHA-256 output
40const HKDF_MAX_L: i64 = 8160 // 255 * 32
41
42// HKDF-Extract.  Writes 32-byte PRK to `prk`.  `salt` may be NULL
43// (caller passes zero pointer + salt_len=0) in which case RFC 5869
44// mandates a zero-filled HashLen salt.
45func hkdf_extract(salt: *u8, salt_len: i64,
46                  ikm: *u8, ikm_len: i64,
47                  prk: *u8) -> i64 {
48    if salt_len == 0 {
49        let zero_salt: *u8 = sys_mmap(HKDF_HASH)
50        var i: i64 = 0
51        while i < HKDF_HASH { zero_salt[i] = 0; i = i + 1 }
52        hmac_sha256(zero_salt, HKDF_HASH, ikm, ikm_len, prk)
53    } else {
54        hmac_sha256(salt, salt_len, ikm, ikm_len, prk)
55    }
56    return 0
57}
58
59// HKDF-Expand.  Writes `L` bytes of keying material to `out`.
60// Returns 0 on success, -1 if L exceeds the HKDF ceiling.
61func hkdf_expand(prk: *u8,
62                 info: *u8, info_len: i64,
63                 l: i64, out: *u8) -> i64 {
64    if l > HKDF_MAX_L { return -1 }
65    if l < 0 { return -1 }
66
67    // n = ceil(L / HashLen); each iteration appends one block.
68    // T(0) = empty; T(i) = HMAC(PRK, T(i-1) || info || i_byte).
69    let t_prev: *u8 = sys_mmap(HKDF_HASH)
70    let t_curr: *u8 = sys_mmap(HKDF_HASH)
71    let buf_cap: i64 = HKDF_HASH + info_len + 1
72    let buf: *u8 = sys_mmap(buf_cap)
73
74    var prev_len: i64 = 0
75    var produced: i64 = 0
76    var counter: i64 = 1
77    while produced < l {
78        // Build input: T(i-1) || info || counter
79        var bi: i64 = 0
80        var k: i64 = 0
81        while k < prev_len { buf[bi + k] = t_prev[k]; k = k + 1 }
82        bi = bi + prev_len
83        k = 0
84        while k < info_len { buf[bi + k] = info[k]; k = k + 1 }
85        bi = bi + info_len
86        buf[bi] = counter & 0xFF
87        bi = bi + 1
88
89        hmac_sha256(prk, HKDF_HASH, buf, bi, t_curr)
90
91        // Copy up to HashLen bytes of T(i) into output.
92        let remain: i64 = l - produced
93        var take: i64 = HKDF_HASH
94        if remain < HKDF_HASH { take = remain }
95        k = 0
96        while k < take { out[produced + k] = t_curr[k]; k = k + 1 }
97        produced = produced + take
98
99        // T(i) becomes T(i-1) for next round.
100        k = 0
101        while k < HKDF_HASH { t_prev[k] = t_curr[k]; k = k + 1 }
102        prev_len = HKDF_HASH
103        counter = counter + 1
104    }
105    return 0
106}
107
108// Compile-only smoke.  Real KAT (RFC 5869 Appendix A.1 test case 1)
109// validation pending execution harness.
110func main() -> i64 {
111    let ikm: *u8 = sys_mmap(22)
112    let salt: *u8 = sys_mmap(13)
113    let info: *u8 = sys_mmap(10)
114    let prk: *u8 = sys_mmap(32)
115    let okm: *u8 = sys_mmap(42)
116    var i: i64 = 0
117    while i < 22 { ikm[i] = 0x0B; i = i + 1 }
118    i = 0
119    while i < 13 { salt[i] = i as i64; i = i + 1 }
120    i = 0
121    while i < 10 { info[i] = 0xF0 + (i as i64); i = i + 1 }
122
123    hkdf_extract(salt, 13, ikm, 22, prk)
124    hkdf_expand(prk, info, 10, 42, okm)
125    return okm[0] as i64
126}
hkdf.nx source

`hkdf.nx` source
