code wiki / _hdl_build / nx_hkdf384_gate.nx
nx_hkdf384_gate.nx source
↩ module page · 142 lines · 7659 B
1// nx_hkdf384_gate.nx -- the SHA-384 half of HKDF, proven without inventing a vector.
2//
3// WHY THIS EXISTS. Our sovereign TLS client offers 0x1302 (AES-256-GCM-SHA384) and then cannot
4// derive its keys: the whole 1.3 key schedule runs on SHA-384 for that suite, while nx_hkdf.nx
5// was SHA-256 by construction. Servers that PREFER 0x1302 were unreachable and the failure
6// surfaced as a bare handshake verdict=5 three layers from the cause. Every primitive already
7// existed (hmac_sha384, sha384_digest, nx_aes256_gcm_seal/open) -- the gap was wiring, the
8// banked adoption-gap class. This gate covers the hash-parameterized hkdf_extract_h/expand_h.
9//
10// ★THE HONEST PROBLEM THIS GATE SOLVES: RFC 5869 publishes vectors for SHA-256 and SHA-1 ONLY.
11// There is NO published HKDF-SHA-384 test vector. Writing down whatever our code prints and
12// calling it a KAT is fabrication wearing a citation -- the exact "invented golden" class already
13// banked in this estate. So SHA-384 is proven by DEFINITIONAL IDENTITY instead: RFC 5869 defines
14// Extract as HMAC(salt, IKM) and Expand's T(1) as HMAC(PRK, info || 0x01), and this gate
15// recomputes both sides independently with hmac_sha384 and demands bit equality. A definition is
16// re-derivable by anyone; a screenshot of our output is not.
17// license_tier: ORIGINAL No hw writes (Rule 26).
18import "nx_syscalls.nx"
19import "nx_gate_verdict.nx"
20import "nx_hkdf.nx"
21
22const HG_H256: i64 = 32
23const HG_H384: i64 = 48
24
25func hg_eq(a: *u8, b: *u8, n: i64) -> i64 {
26 var i: i64 = 0
27 while i < n {
28 if a[i] != b[i] { return 0 }
29 i = i + 1
30 }
31 return 1
32}
33
34// RFC 5869 A.1 PRK, first 8 bytes: 077709362c2e32df0ddc3f0dc47bba63
35func hg_a1_prk_byte(i: i64) -> i64 {
36 if i == 0 { return 0x07 }
37 if i == 1 { return 0x77 }
38 if i == 2 { return 0x09 }
39 if i == 3 { return 0x36 }
40 if i == 4 { return 0x2c }
41 if i == 5 { return 0x2e }
42 if i == 6 { return 0x32 }
43 return 0xdf
44}
45
46func main(argc: i64, argv: *i64) -> i64 {
47 let ctr: *i64 = gv_ctr()
48 gv_head("nx_hkdf384_gate -- HKDF gains SHA-384 additively; the SHA-256 path must not move one bit" as *u8)
49
50 // RFC 5869 A.1 inputs: IKM = 22 x 0x0b, salt = 000102...0c (13 bytes), info = f0f1...f9
51 let ikm: *u8 = sys_mmap(64)
52 var i: i64 = 0
53 while i < 22 { ikm[i] = 0x0b; i = i + 1 }
54 let salt: *u8 = sys_mmap(64)
55 i = 0
56 while i < 13 { salt[i] = i; i = i + 1 }
57 let info: *u8 = sys_mmap(64)
58 i = 0
59 while i < 10 { info[i] = 0xf0 + i; i = i + 1 }
60
61 // T1: the ORIGINAL SHA-256 path still produces the published RFC 5869 A.1 PRK.
62 // This is the regression tooth for an additive edit to a crown-jewel primitive: everything
63 // in the estate links hkdf_extract, so "additive" must be MEASURED, never asserted.
64 let prk_old: *u8 = sys_mmap(64)
65 hkdf_extract(salt, 13, ikm, 22, prk_old)
66 var t1: i64 = 1
67 i = 0
68 while i < 8 {
69 if prk_old[i] != hg_a1_prk_byte(i) { t1 = 0 }
70 i = i + 1
71 }
72 gv_puts(" A.1 prk[0..8] =" as *u8)
73 i = 0
74 while i < 8 { gv_puts(" " as *u8); gv_num(prk_old[i]); i = i + 1 }
75 gv_puts("\n" as *u8)
76 gv_check("T1 THE PUBLISHED VECTOR STILL HOLDS: the untouched SHA-256 hkdf_extract reproduces RFC 5869 A.1's PRK -- an additive edit to a primitive every organ links is proven by regression, not by reading the diff" as *u8, t1, ctr)
77
78 // T2: the NEW dispatcher at hash_len=32 is BIT-IDENTICAL to the original. If these ever
79 // diverge, every existing caller silently changes keys the moment anyone repoints them.
80 let prk_new: *u8 = sys_mmap(64)
81 let rc2: i64 = hkdf_extract_h(salt, 13, ikm, 22, HG_H256, prk_new)
82 var t2: i64 = 0
83 if rc2 == 0 { t2 = hg_eq(prk_old, prk_new, HG_H256) }
84 gv_check("T2 THE DISPATCHER IS TRANSPARENT AT 32: hkdf_extract_h(hash_len=32) is byte-identical to the original hkdf_extract, so adopting the parameterized twin can never move an existing key schedule" as *u8, t2, ctr)
85
86 // T3: expand at 32 likewise unchanged, across a 42-byte output (A.1's L, spanning 2 blocks
87 // so the T(i-1) feedback chain is actually exercised).
88 let okm_old: *u8 = sys_mmap(128)
89 let okm_new: *u8 = sys_mmap(128)
90 hkdf_expand(prk_old, info, 10, 42, okm_old)
91 hkdf_expand_h(prk_new, HG_H256, info, 10, 42, okm_new)
92 var t3: i64 = hg_eq(okm_old, okm_new, 42)
93 gv_check("T3 EXPAND IS TRANSPARENT AT 32 ACROSS A MULTI-BLOCK OUTPUT: 42 bytes spans two SHA-256 blocks, so the T(i-1) feedback chain is exercised, not just the first HMAC" as *u8, t3, ctr)
94
95 // T4: SHA-384 Extract == HMAC-SHA-384(salt, IKM). RFC 5869 s2.2 DEFINES Extract as exactly
96 // that, so the identity is the specification restated -- recomputed here from the primitive
97 // rather than copied from our own output.
98 let prk384: *u8 = sys_mmap(64)
99 let rc4: i64 = hkdf_extract_h(salt, 13, ikm, 22, HG_H384, prk384)
100 let ref384: *u8 = sys_mmap(64)
101 hmac_sha384(salt, 13, ikm, 22, ref384)
102 var t4: i64 = 0
103 if rc4 == 0 { t4 = hg_eq(prk384, ref384, HG_H384) }
104 gv_puts(" sha384 prk[0..8] =" as *u8)
105 i = 0
106 while i < 8 { gv_puts(" " as *u8); gv_num(prk384[i]); i = i + 1 }
107 gv_puts("\n" as *u8)
108 gv_check("T4 SHA-384 EXTRACT MATCHES ITS OWN DEFINITION: RFC 5869 defines Extract as HMAC(salt,IKM) and the gate recomputes that side independently -- no published HKDF-SHA-384 vector exists, and an invented one would be fabrication" as *u8, t4, ctr)
109
110 // T5: SHA-384 Expand's first block == HMAC-SHA-384(PRK, info || 0x01), again the RFC's own
111 // chain definition recomputed here.
112 let okm384: *u8 = sys_mmap(128)
113 let rc5: i64 = hkdf_expand_h(prk384, HG_H384, info, 10, 96, okm384)
114 let chain: *u8 = sys_mmap(64)
115 i = 0
116 while i < 10 { chain[i] = info[i]; i = i + 1 }
117 chain[10] = 1
118 let ref_t1: *u8 = sys_mmap(64)
119 hmac_sha384(prk384, HG_H384, chain, 11, ref_t1)
120 var t5: i64 = 0
121 if rc5 == 0 { t5 = hg_eq(okm384, ref_t1, HG_H384) }
122 gv_check("T5 SHA-384 EXPAND FOLLOWS THE RFC CHAIN: T(1) equals HMAC(PRK, info||0x01) recomputed independently, and the 96-byte request spans two 48-byte blocks so the feedback path runs" as *u8, t5, ctr)
123
124 // T6 BITE, IN-RUN: the two hashes must produce DIFFERENT key material from identical inputs.
125 // If they ever agree, the dispatcher is ignoring hash_len and silently deriving SHA-256 keys
126 // for a SHA-384 suite -- which would present as a decrypt failure far from this file. This is
127 // the tooth that makes T4/T5 measurements instead of tautologies.
128 var t6: i64 = 0
129 if hg_eq(prk_old, prk384, HG_H256) == 0 { t6 = 1 }
130 gv_check("T6 THE HASH SELECTION IS REAL: identical inputs yield different key material at 32 vs 48, so the dispatcher cannot be silently ignoring hash_len and deriving SHA-256 keys for a SHA-384 suite" as *u8, t6, ctr)
131
132 // T7: fail-closed on an unsupported length. A silent SHA-256 fallback here would be the worst
133 // possible failure -- wrong keys, no error, diagnosed three layers away at the record layer.
134 let junk: *u8 = sys_mmap(64)
135 var t7: i64 = 0
136 if hkdf_extract_h(salt, 13, ikm, 22, 64, junk) == 0 - 2 {
137 if hkdf_expand_h(prk384, 20, info, 10, 32, junk) == 0 - 2 { t7 = 1 }
138 }
139 gv_check("T7 AN UNSUPPORTED HASH LENGTH IS REFUSED, NOT ROUNDED: both verbs return -2 rather than falling back to SHA-256, because a silent fallback would derive wrong keys with no error at the point of the mistake" as *u8, t7, ctr)
140
141 return gv_verdict("HKDF384-GATE" as *u8, ctr, "HKDF is hash-parameterized: SHA-256 path bit-identical, SHA-384 proven by definitional identity with an in-run bite" as *u8)
142}