Milestone 6 (ACL/PKI): Ed25519 verify + SHA-512, built from scratch
New freestanding, verify-only Ed25519 (RFC 8032) implementation:
include/starkernel/{sha512,fe25519,scalar25519,ed25519}.h +
src/starkernel/crypto/{sha512,fe25519,scalar25519,ed25519}.c, wired into
Makefile.starkernel. Kernel never signs or generates keys -- only
ed25519_verify() is needed; signing happens in the host-side mkcapsule
build tool via libsodium/OpenSSL.
Confirmed __int128 multiply/add/shift-by-constant compile with zero
undefined symbols on all three target toolchains (only division needs
libgcc's __udivti3, per timer.c's existing documented finding -- that
file's comment updated to narrow the claim, since it had been read as
"avoid __int128 entirely"). This enabled the standard 5-limb radix-2^51
field arithmetic representation.
An abandoned first attempt (10-limb radix-2^26, avoiding __int128 out of
premature caution) hit two real bugs, both invisible on inspection and
found only by property-based testing against Python's own bignum
arithmetic: a non-uniform-radix limb misalignment in multiplication, and
a double-counted carry. Verification chain: SHA-512 against known +
boundary vectors (7/7); field arithmetic property-tested 25,045 cases;
scalar-mod-L arithmetic 300 cases (L confirmed prime via Miller-Rabin
first); full verify() end-to-end against 110 real signatures from
Python's cryptography library, including tampered inputs and the RFC
8032 S>=L malleability attack -- all correctly accepted/rejected.
Compiles clean (zero warnings) and links on all three architectures,
confirmed via the mandatory three-arch QEMU boot. The code is linked but
not yet called from anywhere -- wiring into capsule_birth.c needs a
from-scratch X.509/DER parser first (Captain Bob chose real X.509 over a
raw-blob cert format this session), which is the next open item.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZ8kNoTuP63pbQtro4qvrm
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
2b7743027c
commit
2e7e957680
@@ -0,0 +1,235 @@
|
||||
/* ed25519.c -- see ed25519.h. Twisted Edwards curve point arithmetic
|
||||
* (projective X:Y:Z coordinates, unified addition law -- correctness
|
||||
* over speed, this is a verify-only, non-hot-path library) plus the
|
||||
* RFC 8032 EdDSA verify algorithm.
|
||||
*
|
||||
* All constants below were generated by direct Python computation
|
||||
* (arbitrary-precision arithmetic) and pasted in, not hand-derived or
|
||||
* recalled from memory -- see FABRIC-2.md's Ed25519 milestone writeup
|
||||
* for the derivation. Cross-checked: the curve equation
|
||||
* -x^2+y^2 = 1+d*x^2*y^2 holds for (BX,BY) under this D; the base point
|
||||
* encoding (0x58, then 0x66 repeating) matches the well-known published
|
||||
* Ed25519 base point; L (scalar25519.c) independently confirmed prime.
|
||||
*/
|
||||
#include "starkernel/ed25519.h"
|
||||
#include "starkernel/fe25519.h"
|
||||
#include "starkernel/scalar25519.h"
|
||||
#include "starkernel/sha512.h"
|
||||
#include <string.h>
|
||||
|
||||
static const uint8_t D_BYTES[32] = {
|
||||
0xa3, 0x78, 0x59, 0x13, 0xca, 0x4d, 0xeb, 0x75,
|
||||
0xab, 0xd8, 0x41, 0x41, 0x4d, 0x0a, 0x70, 0x00,
|
||||
0x98, 0xe8, 0x79, 0x77, 0x79, 0x40, 0xc7, 0x8c,
|
||||
0x73, 0xfe, 0x6f, 0x2b, 0xee, 0x6c, 0x03, 0x52,
|
||||
};
|
||||
static const uint8_t BX_BYTES[32] = {
|
||||
0x1a, 0xd5, 0x25, 0x8f, 0x60, 0x2d, 0x56, 0xc9,
|
||||
0xb2, 0xa7, 0x25, 0x95, 0x60, 0xc7, 0x2c, 0x69,
|
||||
0x5c, 0xdc, 0xd6, 0xfd, 0x31, 0xe2, 0xa4, 0xc0,
|
||||
0xfe, 0x53, 0x6e, 0xcd, 0xd3, 0x36, 0x69, 0x21,
|
||||
};
|
||||
static const uint8_t BY_BYTES[32] = {
|
||||
0x58, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66,
|
||||
0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66,
|
||||
0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66,
|
||||
0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66, 0x66,
|
||||
};
|
||||
static const uint8_t SQRTM1_BYTES[32] = {
|
||||
0xb0, 0xa0, 0x0e, 0x4a, 0x27, 0x1b, 0xee, 0xc4,
|
||||
0x78, 0xe4, 0x2f, 0xad, 0x06, 0x18, 0x43, 0x2f,
|
||||
0xa7, 0xd7, 0xfb, 0x3d, 0x99, 0x00, 0x4d, 0x2b,
|
||||
0x0b, 0xdf, 0xc1, 0x4f, 0x80, 0x24, 0x83, 0x2b,
|
||||
};
|
||||
static const uint8_t POW_2252M2_EXP[32] = {
|
||||
0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff,
|
||||
0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff,
|
||||
0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff,
|
||||
0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x0f,
|
||||
};
|
||||
|
||||
typedef struct { fe25519 x, y, z; } ed_point_t;
|
||||
|
||||
static void fe25519_pow(fe25519 *r, const fe25519 *a, const uint8_t exp[32])
|
||||
{
|
||||
fe25519 result; fe25519_1(&result);
|
||||
for (int i = 255; i >= 0; i--) {
|
||||
fe25519_sq(&result, &result);
|
||||
if ((exp[i/8] >> (i%8)) & 1) {
|
||||
fe25519_mul(&result, &result, a);
|
||||
}
|
||||
}
|
||||
*r = result;
|
||||
}
|
||||
|
||||
static void point_identity(ed_point_t *p)
|
||||
{
|
||||
fe25519_0(&p->x);
|
||||
fe25519_1(&p->y);
|
||||
fe25519_1(&p->z);
|
||||
}
|
||||
|
||||
/* Unified addition law for twisted Edwards curves with a=-1 (Ed25519's
|
||||
* curve), projective coordinates -- works for both general addition and
|
||||
* doubling (p1==p2), avoiding a separate doubling formula and its own
|
||||
* chance of transcription error. Standard "add-2008-bbjlp"-family
|
||||
* formula (add_bbjlp_readdition in EFD terminology), not invented here. */
|
||||
static void point_add(ed_point_t *r, const ed_point_t *p1, const ed_point_t *p2)
|
||||
{
|
||||
fe25519 d; fe25519_unpack(&d, D_BYTES);
|
||||
|
||||
fe25519 A, B, C, Dd, E, F, G, t1, t2;
|
||||
fe25519_mul(&A, &p1->z, &p2->z);
|
||||
fe25519_sq(&B, &A);
|
||||
fe25519_mul(&C, &p1->x, &p2->x);
|
||||
fe25519_mul(&Dd, &p1->y, &p2->y);
|
||||
fe25519_mul(&E, &d, &C);
|
||||
fe25519_mul(&E, &E, &Dd);
|
||||
fe25519_sub(&F, &B, &E);
|
||||
fe25519_add(&G, &B, &E);
|
||||
|
||||
fe25519_add(&t1, &p1->x, &p1->y);
|
||||
fe25519_add(&t2, &p2->x, &p2->y);
|
||||
fe25519_mul(&t1, &t1, &t2);
|
||||
fe25519_sub(&t1, &t1, &C);
|
||||
fe25519_sub(&t1, &t1, &Dd);
|
||||
fe25519_mul(&t1, &t1, &F);
|
||||
fe25519_mul(&r->x, &A, &t1);
|
||||
|
||||
fe25519_add(&t2, &Dd, &C);
|
||||
fe25519_mul(&t2, &t2, &G);
|
||||
fe25519_mul(&r->y, &A, &t2);
|
||||
|
||||
fe25519_mul(&r->z, &F, &G);
|
||||
}
|
||||
|
||||
/* Non-constant-time double-and-add: fine here -- verify's scalars (a
|
||||
* message hash and the signature's S component) are public data, not
|
||||
* secrets, so there is no timing side channel to defend against (see
|
||||
* ed25519.h's own doc comment). scalar is 32 bytes little-endian. */
|
||||
static void scalar_mult(ed_point_t *r, const uint8_t scalar[32], const ed_point_t *p)
|
||||
{
|
||||
ed_point_t result;
|
||||
point_identity(&result);
|
||||
for (int i = 255; i >= 0; i--) {
|
||||
point_add(&result, &result, &result);
|
||||
if ((scalar[i/8] >> (i%8)) & 1) {
|
||||
point_add(&result, &result, p);
|
||||
}
|
||||
}
|
||||
*r = result;
|
||||
}
|
||||
|
||||
/* Decompress a 32-byte encoded point: byte 31's top bit is x's sign;
|
||||
* the rest (255 bits) is y. Recovers x via the curve equation and a
|
||||
* modular square root (p = 5 mod 8, so a candidate root is
|
||||
* u^((p+3)/8) mod p, corrected by sqrt(-1) if the first candidate's
|
||||
* square doesn't match -- the standard technique for this prime shape).
|
||||
* Returns 0 on success, -1 if the encoded value has no valid x (not a
|
||||
* point on the curve) -- a malformed/malicious input, must be rejected,
|
||||
* not faulted on. */
|
||||
static int point_decompress(ed_point_t *p, const uint8_t in[32])
|
||||
{
|
||||
int sign = (in[31] >> 7) & 1;
|
||||
uint8_t ybytes[32];
|
||||
memcpy(ybytes, in, 32);
|
||||
ybytes[31] &= 0x7F;
|
||||
|
||||
fe25519 y, d, one, y2, u, v, x2, x, cand, sqrt_m1, check;
|
||||
fe25519_unpack(&y, ybytes);
|
||||
fe25519_unpack(&d, D_BYTES);
|
||||
fe25519_1(&one);
|
||||
|
||||
fe25519_sq(&y2, &y);
|
||||
fe25519_sub(&u, &y2, &one);
|
||||
fe25519_mul(&v, &d, &y2);
|
||||
fe25519_add(&v, &v, &one);
|
||||
|
||||
fe25519 vinv;
|
||||
fe25519_invert(&vinv, &v);
|
||||
fe25519_mul(&x2, &u, &vinv);
|
||||
|
||||
fe25519_pow(&cand, &x2, POW_2252M2_EXP);
|
||||
fe25519_sq(&check, &cand);
|
||||
if (!fe25519_eq(&check, &x2)) {
|
||||
fe25519_unpack(&sqrt_m1, SQRTM1_BYTES);
|
||||
fe25519_mul(&cand, &cand, &sqrt_m1);
|
||||
fe25519_sq(&check, &cand);
|
||||
if (!fe25519_eq(&check, &x2)) {
|
||||
return -1; /* x2 is not a square mod p -- not a valid point */
|
||||
}
|
||||
}
|
||||
x = cand;
|
||||
if (fe25519_parity(&x) != sign) {
|
||||
fe25519_neg(&x, &x);
|
||||
}
|
||||
/* Reject the one remaining edge case RFC 8032 calls out: x == 0
|
||||
* with sign bit set to 1 has no valid representative. */
|
||||
fe25519 zero; fe25519_0(&zero);
|
||||
if (fe25519_eq(&x, &zero) && sign) {
|
||||
return -1;
|
||||
}
|
||||
|
||||
p->x = x;
|
||||
p->y = y;
|
||||
fe25519_1(&p->z);
|
||||
return 0;
|
||||
}
|
||||
|
||||
static void point_compress(uint8_t out[32], const ed_point_t *p)
|
||||
{
|
||||
fe25519 zinv, x, y;
|
||||
fe25519_invert(&zinv, &p->z);
|
||||
fe25519_mul(&x, &p->x, &zinv);
|
||||
fe25519_mul(&y, &p->y, &zinv);
|
||||
fe25519_pack(out, &y);
|
||||
if (fe25519_parity(&x)) {
|
||||
out[31] |= 0x80;
|
||||
}
|
||||
}
|
||||
|
||||
int ed25519_verify(const uint8_t pubkey[32], const uint8_t *msg, size_t msg_len,
|
||||
const uint8_t sig[64])
|
||||
{
|
||||
const uint8_t *R_bytes = sig;
|
||||
const uint8_t *S_bytes = sig + 32;
|
||||
|
||||
/* RFC 8032 malleability requirement: reject S >= L outright, not
|
||||
* just S >= 2^256 -- this is exactly the check a naive
|
||||
* "treat S as a 256-bit number" implementation would skip. */
|
||||
if (!scalar_lt_L(S_bytes)) return 0;
|
||||
|
||||
ed_point_t A, R;
|
||||
if (point_decompress(&A, pubkey) != 0) return 0;
|
||||
if (point_decompress(&R, R_bytes) != 0) return 0;
|
||||
|
||||
/* k = SHA512(R || A || M) mod L */
|
||||
sha512_ctx_t ctx;
|
||||
sha512_init(&ctx);
|
||||
sha512_update(&ctx, R_bytes, 32);
|
||||
sha512_update(&ctx, pubkey, 32);
|
||||
sha512_update(&ctx, msg, msg_len);
|
||||
uint8_t hash[64];
|
||||
sha512_final(&ctx, hash);
|
||||
uint8_t k[32];
|
||||
scalar_reduce512(k, hash);
|
||||
|
||||
/* Check [S]B == R + [k]A by comparing compressed encodings of both
|
||||
* sides -- simpler and just as correct as an in-projective-
|
||||
* coordinates equality check for a verify-only, non-hot-path
|
||||
* library. */
|
||||
ed_point_t B, sB, kA, rhs;
|
||||
fe25519_unpack(&B.x, BX_BYTES);
|
||||
fe25519_unpack(&B.y, BY_BYTES);
|
||||
fe25519_1(&B.z);
|
||||
|
||||
scalar_mult(&sB, S_bytes, &B);
|
||||
scalar_mult(&kA, k, &A);
|
||||
point_add(&rhs, &R, &kA);
|
||||
|
||||
uint8_t lhs_enc[32], rhs_enc[32];
|
||||
point_compress(lhs_enc, &sB);
|
||||
point_compress(rhs_enc, &rhs);
|
||||
|
||||
return memcmp(lhs_enc, rhs_enc, 32) == 0;
|
||||
}
|
||||
Reference in New Issue
Block a user