code wiki / _hdl_build / nx_p384_ecdh_gate.nx

nx_p384_ecdh_gate.nx source

↩ module page · 165 lines · 7660 B

1// nx_p384_ecdh_gate.nx -- KAT for the P-384 ECDHE curve math against RFC 5903 section 8.2. 2// WHY: nx_p384_ecdh.nx was built + DEPLOYED LIVE on the TLS client (triple key_share x25519+P256+P384) 3// but was BEHAVIORALLY UNPROVEN -- no TLS 1.3 server this stack talks to has ever picked secp384r1 4// (they all prefer x25519), so the curve code has never once executed against a known answer. Deployed 5// and never-exercised is exactly the shape that ships a silent crypto bug: the day a server DOES pick 6// P-384, a wrong scalar mult is a failed handshake at best. This gate proves the math independent of 7// any server, using the published IKE/IKEv2 vectors (fetched from rfc-editor.org 2026-07-25, not recalled). 8// 9// Vectors (RFC 5903 8.2, IANA DH group 20): 10// i = initiator private (48B) gix/giy = its public point 11// r = responder private (48B) grx/gry = its public point 12// girx = shared secret = X(i*g^r) = X(r*g^i) <- proven BOTH directions here 13// T5 is the discriminating NEGATIVE control: one flipped byte in the peer's X must NOT still agree 14// (without it a stubbed/constant shared-secret path would pass T3/T4 vacuously). 15// D001: emits a `verdict=` anchor. license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 16import "nx_syscalls.nx" 17import "nx_p384_ecdh.nx" 18import "nx_gate_lib.nx" 19 20const PKG_BUF: i64 = 8192 21const PKG_EXIT_RED: i64 = 1 22 23// CONVERTED 2026-07-25 (seq938): private pkg_ helpers removed; this gate composes nx_gate_lib.nx. 24// Thin wrappers keep every call site untouched (same fold technique used on nx_flip_gate). 25func pkg_puts(s: *u8) -> i64 { return gl_puts(s) } 26func pkg_putn(v: i64) -> i64 { return gl_putn(v) } 27func pkg_hexv(c: i64) -> i64 { 28 if c >= 48 { if c <= 57 { return c - 48 } } 29 if c >= 97 { if c <= 102 { return c - 87 } } 30 if c >= 65 { if c <= 70 { return c - 55 } } 31 return 0 - 1 32} 33func pkg_unhex(s: *u8, out: *u8) -> i64 { 34 var i: i64 = 0 35 var n: i64 = 0 36 var bad: i64 = 0 37 while s[i] != (0 as u8) { 38 let hi: i64 = pkg_hexv(s[i] as i64) 39 let lo: i64 = pkg_hexv(s[i+1] as i64) 40 if hi < 0 { bad = 1 } 41 if lo < 0 { bad = 1 } 42 if bad == 0 { out[n] = ((hi << 4) | lo) as u8; n = n + 1 } 43 i = i + 2 44 } 45 if bad == 1 { return 0 - 1 } 46 return n 47} 48func pkg_eq(a: *u8, b: *u8, n: i64) -> i64 { 49 var i: i64 = 0 50 var ok: i64 = 1 51 while i < n { if a[i] != b[i] { ok = 0 } i = i + 1 } 52 return ok 53} 54func pkg_check(nm: *u8, ok: i64, counts: *i64) -> i64 { return gl_check(nm, ok, counts) } 55 56func main() -> i64 { 57 let counts: *i64 = sys_mmap(32) as *i64 58 counts[0] = 0 59 counts[1] = 0 60 61 // ---- RFC 5903 8.2 vectors (hex, whitespace stripped) ---- 62 let hi_priv: *u8 = "099F3C7034D4A2C699884D73A375A67F7624EF7C6B3C0F160647B67414DCE655E35B538041E649EE3FAEF896783AB194" as *u8 63 let hgix: *u8 = "667842D7D180AC2CDE6F74F37551F55755C7645C20EF73E31634FE72B4C55EE6DE3AC808ACB4BDB4C88732AEE95F41AA" as *u8 64 let hgiy: *u8 = "9482ED1FC0EEB9CAFC4984625CCFC23F65032149E0E144ADA024181535A0F38EEB9FCFF3C2C947DAE69B4C634573A81C" as *u8 65 let hr_priv: *u8 = "41CB0779B4BDB85D47846725FBEC3C9430FAB46CC8DC5060855CC9BDA0AA2942E0308312916B8ED2960E4BD55A7448FC" as *u8 66 let hgrx: *u8 = "E558DBEF53EECDE3D3FCCFC1AEA08A89A987475D12FD950D83CFA41732BC509D0D1AC43A0336DEF96FDA41D0774A3571" as *u8 67 let hgry: *u8 = "DCFBEC7AACF3196472169E838430367F66EEBE3C6E70C416DD5F0C68759DD1FFF83FA40142209DFF5EAAD96DB9E6386C" as *u8 68 let hgirx: *u8 = "11187331C279962D93D604243FD592CB9D0A926F422E47187521287E7156C5C4D603135569B9E9D09CF5D4A270F59746" as *u8 69 70 let i_priv: *u8 = sys_mmap(64) 71 let gix: *u8 = sys_mmap(64) 72 let giy: *u8 = sys_mmap(64) 73 let r_priv: *u8 = sys_mmap(64) 74 let grx: *u8 = sys_mmap(64) 75 let gry: *u8 = sys_mmap(64) 76 let girx: *u8 = sys_mmap(64) 77 let n1: i64 = pkg_unhex(hi_priv, i_priv) 78 let n2: i64 = pkg_unhex(hgix, gix) 79 let n3: i64 = pkg_unhex(hgiy, giy) 80 let n4: i64 = pkg_unhex(hr_priv, r_priv) 81 let n5: i64 = pkg_unhex(hgrx, grx) 82 let n6: i64 = pkg_unhex(hgry, gry) 83 let n7: i64 = pkg_unhex(hgirx, girx) 84 // T0: the vectors themselves decoded to 48 bytes each (a bad literal would fake every later result) 85 var vok: i64 = 1 86 if n1 != 48 { vok = 0 } 87 if n2 != 48 { vok = 0 } 88 if n3 != 48 { vok = 0 } 89 if n4 != 48 { vok = 0 } 90 if n5 != 48 { vok = 0 } 91 if n6 != 48 { vok = 0 } 92 if n7 != 48 { vok = 0 } 93 pkg_check("T0-vectors-decode-48B" as *u8, vok, counts) 94 95 // ---- T1: initiator public key = i*G matches gix||giy ---- 96 let ipub: *u8 = sys_mmap(128) 97 let v1: i64 = p384_ecdh_pub(i_priv, ipub) 98 var ok1: i64 = 1 99 if v1 != NX_P384_ECDH_OK { ok1 = 0 } 100 if ipub[0] != (4 as u8) { ok1 = 0 } 101 if pkg_eq(ipub + 1, gix, 48) == 0 { ok1 = 0 } 102 if pkg_eq(ipub + 49, giy, 48) == 0 { ok1 = 0 } 103 pkg_check("T1-initiator-pubkey-matches-RFC" as *u8, ok1, counts) 104 105 // ---- T2: responder public key = r*G matches grx||gry ---- 106 let rpub: *u8 = sys_mmap(128) 107 let v2: i64 = p384_ecdh_pub(r_priv, rpub) 108 var ok2: i64 = 1 109 if v2 != NX_P384_ECDH_OK { ok2 = 0 } 110 if pkg_eq(rpub + 1, grx, 48) == 0 { ok2 = 0 } 111 if pkg_eq(rpub + 49, gry, 48) == 0 { ok2 = 0 } 112 pkg_check("T2-responder-pubkey-matches-RFC" as *u8, ok2, counts) 113 114 // ---- T3: i * g^r == girx ---- 115 let sh1: *u8 = sys_mmap(64) 116 let v3: i64 = p384_ecdh_shared(i_priv, rpub, 97, sh1) 117 var ok3: i64 = 1 118 if v3 != NX_P384_ECDH_OK { ok3 = 0 } 119 if pkg_eq(sh1, girx, 48) == 0 { ok3 = 0 } 120 pkg_check("T3-shared-i-times-gr-matches-RFC" as *u8, ok3, counts) 121 122 // ---- T4: r * g^i == girx (the SAME secret from the other side) ---- 123 let sh2: *u8 = sys_mmap(64) 124 let v4: i64 = p384_ecdh_shared(r_priv, ipub, 97, sh2) 125 var ok4: i64 = 1 126 if v4 != NX_P384_ECDH_OK { ok4 = 0 } 127 if pkg_eq(sh2, girx, 48) == 0 { ok4 = 0 } 128 pkg_check("T4-shared-r-times-gi-matches-RFC" as *u8, ok4, counts) 129 130 // ---- T5 NEGATIVE CONTROL: corrupt one byte of the peer point -> must NOT yield the RFC secret ---- 131 // (an off-curve point should be REFUSED; if it is somehow accepted the secret must still differ) 132 let badpub: *u8 = sys_mmap(128) 133 var ci: i64 = 0 134 while ci < 97 { badpub[ci] = rpub[ci]; ci = ci + 1 } 135 badpub[1] = (badpub[1] ^ (1 as u8)) as u8 136 let sh3: *u8 = sys_mmap(64) 137 let v5: i64 = p384_ecdh_shared(i_priv, badpub, 97, sh3) 138 var ok5: i64 = 0 139 if v5 != NX_P384_ECDH_OK { ok5 = 1 } 140 else { if pkg_eq(sh3, girx, 48) == 0 { ok5 = 1 } } 141 pkg_check("T5-neg-corrupt-peer-point-rejected" as *u8, ok5, counts) 142 143 // ---- T6: a short peer share is refused at the boundary (length validation) ---- 144 let sh4: *u8 = sys_mmap(64) 145 let v6: i64 = p384_ecdh_shared(i_priv, rpub, 96, sh4) 146 var ok6: i64 = 0 147 if v6 == NX_P384_ECDH_BAD_POINT { ok6 = 1 } 148 pkg_check("T6-neg-short-peer-share-refused" as *u8, ok6, counts) 149 150 // DURABLE EVIDENCE (seq986): the clock dispatcher records only THAT a job ran, never its exit code, 151 152 // and discards stdout -- so without this line an hourly RED is invisible. Written for nx_gate_rollup. 153 154 gl_log("knowledge/status/p384_ecdh_gate.log" as *u8, "NX-P384-ECDH-GATE" as *u8, counts) 155 156 pkg_puts("NX-P384-ECDH-GATE\n" as *u8) 157 pkg_puts("verdict=" as *u8) 158 if counts[1] == counts[0] { pkg_puts("GREEN" as *u8) } else { pkg_puts("RED" as *u8) } 159 pkg_puts(" pass=" as *u8); pkg_putn(counts[1]) 160 pkg_puts("/" as *u8); pkg_putn(counts[0]) 161 pkg_puts(" ref=RFC5903-8.2-group20\n" as *u8) 162 if counts[1] == counts[0] { sys_exit(0); return 0 } 163 sys_exit(PKG_EXIT_RED) 164 return PKG_EXIT_RED 165}