nx_p256_keyshare_test.nx source
↩ module page · 175 lines · 6610 B
1// nx_p256_keyshare_test.nx -- B4-P256-KEYSHARE gate row.
2//
3// Proves the P-256 half of the TLS 1.3 key_share path:
4// A. RFC 5903 section 8.1 ECDH KAT, BOTH directions:
5// pub(i) == (g_ix, g_iy), pub(r) == (g_rx, g_ry)
6// shared(i, pub_r) == g_irx == shared(r, pub_i)
7// (vectors re-read from rfc-editor.org 2026-06-10, not memory)
8// B. Boundary rejects: off-curve point, bad format byte, bad length
9// C. p256_ecdh_derive_priv: deterministic, in-range, usable
10// D. tls13_ext_emit_key_share_dual: byte-exact wire format
11// (lengths, both group ids, both pubkeys in place)
12//
13// Distinct exit code per assertion; exit 0 = row PASS.
14//
15// expect_exit: 0
16// license_tier: ORIGINAL
17
18import "nx_syscalls.nx"
19import "nx_u256.nx"
20import "nx_p256_field.nx"
21import "nx_p256_point.nx"
22import "nx_p256_point_add.nx"
23import "nx_p256_scalar_mul.nx"
24import "nx_p256_modn.nx"
25import "nx_p256_ecdh.nx"
26import "nx_tls13.nx"
27import "nx_tls13_ext.nx"
28
29// Write 16 big-endian bytes (4 u32 words, MSW first) at out.
30func kat_w4(out: *u8, w0: i64, w1: i64, w2: i64, w3: i64) -> i64 {
31 let ws: *i64 = sys_mmap(32) as *i64
32 ws[0] = w0; ws[1] = w1; ws[2] = w2; ws[3] = w3
33 var i: i64 = 0
34 while i < 4 {
35 let w: i64 = ws[i]
36 out[i * 4] = ((w >> 24) & 0xff) as u8
37 out[i * 4 + 1] = ((w >> 16) & 0xff) as u8
38 out[i * 4 + 2] = ((w >> 8) & 0xff) as u8
39 out[i * 4 + 3] = (w & 0xff) as u8
40 i = i + 1
41 }
42 return 0
43}
44
45func kat_eq32(a: *u8, b: *u8) -> i64 {
46 var i: i64 = 0
47 while i < 32 {
48 if a[i] != b[i] { return 0 }
49 i = i + 1
50 }
51 return 1
52}
53
54func main() -> i64 {
55 // ---- RFC 5903 8.1 vectors (big-endian byte buffers) ----
56 let priv_i: *u8 = sys_mmap(32)
57 kat_w4(priv_i, 0xC88F01F5, 0x10D9AC3F, 0x70A292DA, 0xA2316DE5)
58 kat_w4(priv_i + 16, 0x44E9AAB8, 0xAFE84049, 0xC62A9C57, 0x862D1433)
59
60 let pub_i_kat: *u8 = sys_mmap(65)
61 pub_i_kat[0] = 4 as u8
62 kat_w4(pub_i_kat + 1, 0xDAD0B653, 0x94221CF9, 0xB051E1FE, 0xCA5787D0)
63 kat_w4(pub_i_kat + 17, 0x98DFE637, 0xFC90B9EF, 0x945D0C37, 0x72581180)
64 kat_w4(pub_i_kat + 33, 0x5271A046, 0x1CDB8252, 0xD61F1C45, 0x6FA3E59A)
65 kat_w4(pub_i_kat + 49, 0xB1F45B33, 0xACCF5F58, 0x389E0577, 0xB8990BB3)
66
67 let priv_r: *u8 = sys_mmap(32)
68 kat_w4(priv_r, 0xC6EF9C5D, 0x78AE012A, 0x011164AC, 0xB397CE20)
69 kat_w4(priv_r + 16, 0x88685D8F, 0x06BF9BE0, 0xB283AB46, 0x476BEE53)
70
71 let pub_r_kat: *u8 = sys_mmap(65)
72 pub_r_kat[0] = 4 as u8
73 kat_w4(pub_r_kat + 1, 0xD12DFB52, 0x89C8D4F8, 0x1208B702, 0x70398C34)
74 kat_w4(pub_r_kat + 17, 0x2296970A, 0x0BCCB74C, 0x736FC755, 0x4494BF63)
75 kat_w4(pub_r_kat + 33, 0x56FBF3CA, 0x366CC23E, 0x8157854C, 0x13C58D6A)
76 kat_w4(pub_r_kat + 49, 0xAC23F046, 0xADA30F83, 0x53E74F33, 0x039872AB)
77
78 let shared_kat: *u8 = sys_mmap(32)
79 kat_w4(shared_kat, 0xD6840F6B, 0x42F6EDAF, 0xD13116E0, 0xE1256520)
80 kat_w4(shared_kat + 16, 0x2FEF8E9E, 0xCE7DCE03, 0x812464D0, 0x4B9442DE)
81
82 // ---- A1: pub(i) matches g_i ----
83 let pub_i: *u8 = sys_mmap(65)
84 if p256_ecdh_pub(priv_i, pub_i) != NX_P256_ECDH_OK { return 1 }
85 var i: i64 = 0
86 while i < 65 {
87 if pub_i[i] != pub_i_kat[i] { return 2 }
88 i = i + 1
89 }
90
91 // ---- A2: pub(r) matches g_r ----
92 let pub_r: *u8 = sys_mmap(65)
93 if p256_ecdh_pub(priv_r, pub_r) != NX_P256_ECDH_OK { return 3 }
94 i = 0
95 while i < 65 {
96 if pub_r[i] != pub_r_kat[i] { return 4 }
97 i = i + 1
98 }
99
100 // ---- A3: shared(i, pub_r) == g_irx ----
101 let sh1: *u8 = sys_mmap(32)
102 if p256_ecdh_shared(priv_i, pub_r_kat, 65, sh1) != NX_P256_ECDH_OK { return 5 }
103 if kat_eq32(sh1, shared_kat) != 1 { return 6 }
104
105 // ---- A4: shared(r, pub_i) == g_irx (symmetry) ----
106 let sh2: *u8 = sys_mmap(32)
107 if p256_ecdh_shared(priv_r, pub_i_kat, 65, sh2) != NX_P256_ECDH_OK { return 7 }
108 if kat_eq32(sh2, shared_kat) != 1 { return 8 }
109
110 // ---- B1: off-curve point rejected ----
111 let bad: *u8 = sys_mmap(65)
112 i = 0
113 while i < 65 { bad[i] = pub_r_kat[i]; i = i + 1 }
114 bad[10] = (bad[10] + (1 as u8)) as u8
115 let sh3: *u8 = sys_mmap(32)
116 if p256_ecdh_shared(priv_i, bad, 65, sh3) != NX_P256_ECDH_BAD_POINT { return 9 }
117
118 // ---- B2: format byte != 0x04 rejected ----
119 i = 0
120 while i < 65 { bad[i] = pub_r_kat[i]; i = i + 1 }
121 bad[0] = 2 as u8
122 if p256_ecdh_shared(priv_i, bad, 65, sh3) != NX_P256_ECDH_BAD_POINT { return 10 }
123
124 // ---- B3: wrong length rejected ----
125 if p256_ecdh_shared(priv_i, pub_r_kat, 33, sh3) != NX_P256_ECDH_BAD_POINT { return 11 }
126
127 // ---- B4: zero scalar rejected ----
128 let zero: *u8 = sys_mmap(32)
129 if p256_ecdh_shared(zero, pub_r_kat, 65, sh3) != NX_P256_ECDH_BAD_PRIV { return 12 }
130
131 // ---- C: derive_priv deterministic + usable ----
132 let seed: *u8 = sys_mmap(32)
133 i = 0
134 while i < 32 { seed[i] = (0x40 + i) as u8; i = i + 1 }
135 let d1: *u8 = sys_mmap(32)
136 let d2: *u8 = sys_mmap(32)
137 if p256_ecdh_derive_priv(seed, d1) != NX_P256_ECDH_OK { return 13 }
138 if p256_ecdh_derive_priv(seed, d2) != NX_P256_ECDH_OK { return 14 }
139 if kat_eq32(d1, d2) != 1 { return 15 }
140 let dpub: *u8 = sys_mmap(65)
141 if p256_ecdh_pub(d1, dpub) != NX_P256_ECDH_OK { return 16 }
142 if dpub[0] != (4 as u8) { return 17 }
143
144 // ---- D: dual key_share wire format ----
145 let x25519_pub: *u8 = sys_mmap(32)
146 i = 0
147 while i < 32 { x25519_pub[i] = (0xA0 + i) as u8; i = i + 1 }
148 let ks: *u8 = sys_mmap(256)
149 let n: i64 = tls13_ext_emit_key_share_dual(x25519_pub, pub_i_kat, ks, 256)
150 if n != 111 { return 18 }
151 // ext_type = 51, ext_len = 107, shares_len = 105
152 if ((ks[0] & 0xff) << 8) | (ks[1] & 0xff) != 51 { return 19 }
153 if ((ks[2] & 0xff) << 8) | (ks[3] & 0xff) != 107 { return 20 }
154 if ((ks[4] & 0xff) << 8) | (ks[5] & 0xff) != 105 { return 21 }
155 // entry 1: x25519 (0x001d), len 32, bytes in place
156 if ((ks[6] & 0xff) << 8) | (ks[7] & 0xff) != 29 { return 22 }
157 if ((ks[8] & 0xff) << 8) | (ks[9] & 0xff) != 32 { return 23 }
158 i = 0
159 while i < 32 {
160 if ks[10 + i] != x25519_pub[i] { return 24 }
161 i = i + 1
162 }
163 // entry 2: secp256r1 (0x0017), len 65, bytes in place
164 if ((ks[42] & 0xff) << 8) | (ks[43] & 0xff) != 23 { return 25 }
165 if ((ks[44] & 0xff) << 8) | (ks[45] & 0xff) != 65 { return 26 }
166 i = 0
167 while i < 65 {
168 if ks[46 + i] != pub_i_kat[i] { return 27 }
169 i = i + 1
170 }
171 // buffer-overflow guard honest
172 if tls13_ext_emit_key_share_dual(x25519_pub, pub_i_kat, ks, 110) >= 0 { return 28 }
173
174 return 0
175}