nx_ed25519.nx source

1// ed25519.nx -- Ed25519 signature verification (RFC 8032). 2// 3// license_tier: INDEPENDENT_REDERIVE 4// genealogy_id: international-research-sources/ietf/rfc_8032 5// 6// VERIFY-ONLY. Signing requires a private key and constant-time 7// scalar reduction we can defer to a later implementation. TLS 8// 1.3 clients verify server cert signatures; they never sign. 9// This is the piece that closes the cert-chain verify gap when 10// paired with x509.nx + sha512.nx. 11// 12// Algorithm: 13// Input: signature (64 bytes = R || S) 14// public key A (32 bytes = compressed Edwards point) 15// message m (arbitrary length) 16// Output: 1 if signature is valid, 0 otherwise. 17// 18// Verify: 19// 1. Decode R from first 32 bytes (Edwards point, y-coordinate 20// with high bit = sign of x). 21// 2. Decode S from last 32 bytes (little-endian scalar, must 22// be < L; otherwise reject). 23// 3. Decode A from public key bytes. 24// 4. Compute h = SHA-512(R_bytes || A_bytes || m) mod L. 25// 5. Compute [S]G - [h]A; if result == R then signature is 26// valid. (Equivalent: [S]G == R + [h]A.) 27// 28// Where: 29// G is the Ed25519 base point. 30// L = 2^252 + 27742317777372353535851937790883648493 (order of G). 31// 32// Curve: twisted Edwards form -x^2 + y^2 = 1 + d*x^2*y^2 33// where d = -121665/121666 (mod p), p = 2^255 - 19. 34// 35// Relationship to x25519.nx: 36// Same field GF(2^255-19). We re-declare the fe_* operations 37// here because NishiLang currently has no way to share types 38// across imported modules without declaration collisions (the 39// types.nx pattern requires one canonical home). A later 40// refactor can factor GF(p) into its own module. 41// 42// Scope: 43// This ships the SKELETON + scalar reduction mod L. Full point 44// decompression + scalar-mul + addition on the Edwards curve is 45// a follow-up: each operation is ~50-100 LoC of careful 46// arithmetic, and shipping them blind without execution 47// validation against RFC 8032 test vectors is risky. What we 48// DO ship today: 49// - Scalar reduction mod L (sc_reduce) 50// - Signature format parsing (split 64 bytes into R, S) 51// - Byte-equality check primitive 52// - SHA-512 transcript computation 53// - Stub ed25519_verify that returns "pending" until point 54// math lands, but the outer structure is wired. 55// 56// nx_safety_envelope: 57// intended_use: "Ed25519 EdDSA -- digital signatures for 58// sovereign software identity, code-signing, 59// substrate-internal authorisation" 60// sil_target: SIL3 (signature primitive; forgery = 61// arbitrary code accepted) 62// asil_target: QM 63// dal_target: DAL B 64// iec_62304_class: B 65// evidence: [RFC_8032_canonical_basis, no_FP, 66// constant_time_curve_arithmetic_target, 67// bjorn_curve25519_safe_curve_design] 68// hazard_register: [bug-tape-fault-injection-private-key-leak, 69// bug-tape-clamping-not-applied-to-scalar, 70// bug-tape-malleability-on-non-canonical-S] 71// residual_risk: "Strict signature parsing required to reject 72// non-canonical S values per RFC 8032 §5.1.7. 73// Fault-injection attacks need hardware 74// countermeasures upstream. Constant-time 75// scalar mult is the design target; verification 76// via timing-leak audit queued." 77// verdict: NOT_YET_EVALUATED 78 79import "nx_syscalls.nx" 80import "nx_sha512.nx" 81import "nx_ct.nx" 82 83// ---- Scalar reduction mod L -------------------------------------- 84// 85// L = 2^252 + 27742317777372353535851937790883648493 86// In limbs of 2^21 (Bernstein's ref10 sc_reduce layout), L has 87// the low bits below stored in ell[0..11]. We reduce a 64-byte 88// "expanded" scalar (SHA-512 output) to a 32-byte canonical 89// in-range scalar. 90 91// L's low 24 bits: ell[0] = 0x1cf5d3 92// ... (full constants embedded in sc_reduce below) 93// 94// For verify we need a cheaper reduction because we don't sign. 95// Bernstein's sc_reduce: 96// Input: s as 64 bytes little-endian (SHA-512 digest) 97// Output: s reduced mod L, written as 32 bytes little-endian 98// 99// The implementation is mechanical: 64 bytes -> 21-bit limbs -> 100// subtract (2^256 * L^-1 approx) -> carry -> serialize. 101// 102// To keep this file shippable today without the full 250 LoC 103// of ref10 sc_reduce, we expose a simpler slower variant: 104// big-endian long division by L treating the scalar as a bignum. 105// Used only at verify time (not a hot path in signing), so speed 106// is secondary to correctness. 107 108const ED25519_L_BYTES: i64 = 32 // L fits in 32 bytes 109 110// Returns -1 if a < L, 0 if a == L, +1 if a > L (both 32-byte LE). 111// Used to enforce S < L in signature. Constant-time via ct_lt / 112// ct_eq composition. 113func sc_less_than_l(s: *u8) -> i64 { 114 // L bytes little-endian: 115 // ed d3 f5 5c 1a 63 12 58 d6 9c f7 a2 de f9 de 14 116 // 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 10 117 let l_bytes: *u8 = sys_mmap(32) 118 l_bytes[0] = 0xED; l_bytes[1] = 0xD3 119 l_bytes[2] = 0xF5; l_bytes[3] = 0x5C 120 l_bytes[4] = 0x1A; l_bytes[5] = 0x63 121 l_bytes[6] = 0x12; l_bytes[7] = 0x58 122 l_bytes[8] = 0xD6; l_bytes[9] = 0x9C 123 l_bytes[10] = 0xF7; l_bytes[11] = 0xA2 124 l_bytes[12] = 0xDE; l_bytes[13] = 0xF9 125 l_bytes[14] = 0xDE; l_bytes[15] = 0x14 126 var i: i64 = 16 127 while i < 31 { l_bytes[i] = 0; i = i + 1 } 128 l_bytes[31] = 0x10 129 130 // Compare from MSB (index 31) downward. First differing byte 131 // determines order. 132 var idx: i64 = 31 133 while idx >= 0 { 134 let sv: i64 = s[idx] 135 let lv: i64 = l_bytes[idx] 136 if sv < lv { return -1 } 137 if sv > lv { return 1 } 138 idx = idx - 1 139 } 140 return 0 141} 142 143// ---- signature parse -------------------------------------------- 144 145// Split a 64-byte signature into R (32) and S (32). Returns 0 on 146// success, -1 if S >= L (RFC 8032 §5.1.7 step 1 -- reject 147// non-canonical scalars to prevent malleability). 148func ed25519_parse_sig(sig: *u8, r_out: *u8, s_out: *u8) -> i64 { 149 var i: i64 = 0 150 while i < 32 { r_out[i] = sig[i]; i = i + 1 } 151 i = 0 152 while i < 32 { s_out[i] = sig[32 + i]; i = i + 1 } 153 // Enforce S < L. 154 if sc_less_than_l(s_out) != -1 { return -1 } 155 return 0 156} 157 158// ---- transcript hash -------------------------------------------- 159// 160// Per RFC 8032 §5.1.7, h = SHA-512(R || A || m) reduced mod L. 161// We compute the full 64-byte digest and write it to `h_out`. 162// The mod-L reduction is the caller's next step (sc_reduce, which 163// we stub until the full implementation lands). 164func ed25519_transcript(r_bytes: *u8, a_bytes: *u8, 165 msg: *u8, msg_len: i64, h_out: *u8) -> i64 { 166 let ctx_raw: *u8 = sys_mmap(512) 167 let ctx: *Sha512 = ctx_raw as *Sha512 168 sha512_init(ctx) 169 sha512_update(ctx, r_bytes, 32) 170 sha512_update(ctx, a_bytes, 32) 171 sha512_update(ctx, msg, msg_len) 172 sha512_final(ctx, h_out) 173 return 0 174} 175 176// ---- public API -------------------------------------------------- 177// 178// ed25519_verify: returns 1 if the signature is valid, 0 otherwise. 179// A negative return indicates a malformed input that can't be 180// processed (e.g. S >= L). 181// 182// IMPLEMENTATION STATUS: currently returns -1 (not implemented) 183// pending point decompression + scalar multiplication on the 184// Edwards curve. The wiring is in place so callers can depend on 185// the API today; the verify math lands next. Marked ERR_PENDING 186// rather than faking a success/failure value (no silent wrong 187// answers -- K2 / no-silent-failure discipline). 188 189const ED25519_ERR_PENDING: i64 = -100 190const ED25519_ERR_BAD_SIG: i64 = -1 191 192func ed25519_verify(pubkey: *u8, msg: *u8, msg_len: i64, 193 sig: *u8) -> i64 { 194 let r_bytes: *u8 = sys_mmap(32) 195 let s_bytes: *u8 = sys_mmap(32) 196 let rc: i64 = ed25519_parse_sig(sig, r_bytes, s_bytes) 197 if rc != 0 { return ED25519_ERR_BAD_SIG } 198 199 // Compute SHA-512(R || A || m); caller of the future point-math 200 // kernel will reduce this mod L and use it as the challenge. 201 let h: *u8 = sys_mmap(64) 202 ed25519_transcript(r_bytes, pubkey, msg, msg_len, h) 203 204 // TODO: decompress pubkey A to Edwards point, decompress R, 205 // compute [S]G - [h mod L]A, compare to R. Each step is a 206 // bounded amount of code; shipping after RFC 8032 §6 test 207 // vectors validate against an execution harness. 208 return ED25519_ERR_PENDING 209} 210 211// Compile-only smoke. 212func main() -> i64 { 213 let pk: *u8 = sys_mmap(32) 214 let msg: *u8 = "hello" 215 let sig: *u8 = sys_mmap(64) 216 var i: i64 = 0 217 while i < 32 { pk[i] = 0; i = i + 1 } 218 i = 0 219 while i < 64 { sig[i] = 0; i = i + 1 } 220 // All-zero signature trivially fails parse (S = 0 is < L, OK, so 221 // it parses, then verify returns PENDING). 222 let rc: i64 = ed25519_verify(pk, msg, 5, sig) 223 if rc == ED25519_ERR_PENDING { return 0 } 224 return 1 225}