ed25519.nx source

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