Skip to content

Commit

Permalink
25519: scalarmult in C
Browse files Browse the repository at this point in the history
  • Loading branch information
@hannesm
hannesm committed Mar 15, 2021
1 parent 8d73de2 commit 7cc310b
Show file tree
Hide file tree
Showing 2 changed files with 131 additions and 89 deletions.
89 changes: 2 additions & 87 deletions ec/mirage_crypto_ec.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -781,98 +781,13 @@ module P521 : Dh_dsa = struct
end

module Curve25519 = struct
external sub : field_element -> field_element -> field_element -> unit = "mc_25519_sub" [@@noalloc]
external add : field_element -> field_element -> field_element -> unit = "mc_25519_add" [@@noalloc]
external mul : field_element -> field_element -> field_element -> unit = "mc_25519_mul" [@@noalloc]
external square : field_element -> field_element -> unit = "mc_25519_square" [@@noalloc]
external mul_121666 : field_element -> field_element -> unit = "mc_25519_mul_121666" [@@noalloc]
external from_bytes : field_element -> Cstruct.buffer -> unit = "mc_25519_from_bytes" [@@noalloc]
external to_bytes : Cstruct.buffer -> field_element -> unit = "mc_25519_to_bytes" [@@noalloc]
external select_c : field_element -> bool -> field_element -> field_element -> unit = "mc_25519_select" [@@noalloc]

(* 32 bit: 10 limbs, 64 bit: 5 limbs *)
let create () =
Cstruct.(to_bigarray (create 40))

let key_len = 32

let one =
let buf = Cstruct.create key_len in
Cstruct.set_uint8 buf 0 1;
buf

let bit_at s i =
let byte_num = i / 8 in
let bit_num = i mod 8 in
let byte = Cstruct.get_uint8 s byte_num in
byte land (1 lsl bit_num) <> 0

let swap bit a b =
let out0 = create ()
and out1 = create ()
in
select_c out0 bit b a;
select_c out1 bit a b;
Bigarray.Array1.blit out0 a;
Bigarray.Array1.blit out1 b

external invert : field_element -> field_element -> unit = "mc_25519_invert" [@@noalloc]
external scalarmult : Cstruct.buffer -> Cstruct.buffer -> Cstruct.buffer -> unit = "mc_x25519_scalarmult" [@@noalloc]

let scalar_mult in_ base =
let out = Cstruct.create key_len in
let e = Cstruct.create key_len in
Cstruct.blit base 0 e 0 key_len;
let x1 = create ()
and x2 = create ()
and z2 = create ()
and x3 = create ()
and z3 = create ()
and tmp0 = create ()
and tmp1 = create ()
in
Cstruct.set_uint8 e 31 (Cstruct.get_uint8 e 31 land 0x7f);
from_bytes x1 e.Cstruct.buffer;
from_bytes x2 one.Cstruct.buffer;
from_bytes x3 e.Cstruct.buffer;
from_bytes z3 one.Cstruct.buffer;
Cstruct.blit in_ 0 e 0 key_len;
Cstruct.set_uint8 e 0 (Cstruct.get_uint8 e 0 land 248);
Cstruct.set_uint8 e 31 (Cstruct.get_uint8 e 31 land 127);
Cstruct.set_uint8 e 31 (Cstruct.get_uint8 e 31 lor 64);
let to_swap = ref false in
for pos = 254 downto 0 do
let b = bit_at e pos in
to_swap :=
(match !to_swap, b with
| false, false | true, true-> false
| false, true | true, false -> true);
swap !to_swap x2 x3;
swap !to_swap z2 z3;
to_swap := b;
sub tmp0 x3 z3;
sub tmp1 x2 z2;
add x2 x2 z2;
add z2 x3 z3;
mul z3 tmp0 x2;
mul z2 z2 tmp1;
square tmp0 tmp1;
square tmp1 x2;
add x3 z3 z2;
sub z2 z3 z2;
mul x2 tmp1 tmp0;
sub tmp1 tmp1 tmp0;
square z2 z2;
mul_121666 z3 tmp1;
square x3 x3;
add tmp0 tmp0 z3;
mul z3 x1 z2;
mul z2 tmp1 tmp0;
done;
swap !to_swap x2 x3;
swap !to_swap z2 z3;
invert z2 z2;
mul x2 x2 z2;
to_bytes out.Cstruct.buffer x2;
scalarmult out.Cstruct.buffer in_.Cstruct.buffer base.Cstruct.buffer;
out

type secret = Cstruct.t
Expand Down
131 changes: 129 additions & 2 deletions ec/native/curve25519_stubs.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ typedef WORD fe[LIMBS];
#define fe_mul_ttt fiat_25519_carry_mul

/* from BoringSSL source (curve25519.c, fe_loose_invert, with all & removed) */
static void invert (fe out, const fe z) {
static void fe_invert (fe out, const fe z) {
fe t0;
fe t1;
fe t2;
Expand Down Expand Up @@ -76,6 +76,126 @@ static void invert (fe out, const fe z) {
fe_mul_ttt(out, t1, t0);
}

static void fe_frombytes(fe h, const uint8_t s[32]) {
uint8_t s_copy[32];
memcpy(s_copy, s, 32);
s_copy[31] &= 0x7f;
fiat_25519_from_bytes(h, s_copy);
}

#define fe_tobytes fiat_25519_to_bytes
#define fe_mul_tll fiat_25519_carry_mul
#define fe_add fiat_25519_add
#define fe_sub fiat_25519_sub
#define fe_mul121666 fiat_25519_carry_scmul_121666

static void fe_1(fe h) {
memset(h, 0, sizeof(fe));
h[0] = 1;
}

static void fe_0(fe h) {
memset(h, 0, sizeof(fe));
}

static void fe_copy(fe h, const fe f) {
memmove(h, f, sizeof(fe));
}

static void fe_cswap(fe f, fe g, WORD b) {
b = 0-b;
for (unsigned i = 0; i < LIMBS; i++) {
WORD x = f[i] ^ g[i];
x &= b;
f[i] ^= x;
g[i] ^= x;
}
}


static void x25519_scalar_mult_generic(uint8_t out[32],
const uint8_t scalar[32],
const uint8_t point[32]) {
fe x1, x2, z2, x3, z3, tmp0, tmp1;
fe x2l, z2l, x3l, tmp0l, tmp1l;

uint8_t e[32];
memcpy(e, scalar, 32);
e[0] &= 248;
e[31] &= 127;
e[31] |= 64;

// The following implementation was transcribed to Coq and proven to
// correspond to unary scalar multiplication in affine coordinates given that
// x1 != 0 is the x coordinate of some point on the curve. It was also checked
// in Coq that doing a ladderstep with x1 = x3 = 0 gives z2' = z3' = 0, and z2
// = z3 = 0 gives z2' = z3' = 0. The statement was quantified over the
// underlying field, so it applies to Curve25519 itself and the quadratic
// twist of Curve25519. It was not proven in Coq that prime-field arithmetic
// correctly simulates extension-field arithmetic on prime-field values.
// The decoding of the byte array representation of e was not considered.
// Specification of Montgomery curves in affine coordinates:
// <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Spec/MontgomeryCurve.v#L27>
// Proof that these form a group that is isomorphic to a Weierstrass curve:
// <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/AffineProofs.v#L35>
// Coq transcription and correctness proof of the loop (where scalarbits=255):
// <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L118>
// <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L278>
// preconditions: 0 <= e < 2^255 (not necessarily e < order), fe_invert(0) = 0
fe_frombytes(x1, point);
fe_1(x2);
fe_0(z2);
fe_copy(x3, x1);
fe_1(z3);

unsigned swap = 0;
int pos;
for (pos = 254; pos >= 0; --pos) {
// loop invariant as of right before the test, for the case where x1 != 0:
// pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3 is nonzero
// let r := e >> (pos+1) in the following equalities of projective points:
// to_xz (r*P) === if swap then (x3, z3) else (x2, z2)
// to_xz ((r+1)*P) === if swap then (x2, z2) else (x3, z3)
// x1 is the nonzero x coordinate of the nonzero point (r*P-(r+1)*P)
unsigned b = 1 & (e[pos / 8] >> (pos & 7));
swap ^= b;
fe_cswap(x2, x3, swap);
fe_cswap(z2, z3, swap);
swap = b;
// Coq transcription of ladderstep formula (called from transcribed loop):
// <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L89>
// <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L131>
// x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L217>
// x1 = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L147>
fe_sub(tmp0l, x3, z3);
fe_sub(tmp1l, x2, z2);
fe_add(x2l, x2, z2);
fe_add(z2l, x3, z3);
fe_mul_tll(z3, tmp0l, x2l);
fe_mul_tll(z2, z2l, tmp1l);
fe_sq_tl(tmp0, tmp1l);
fe_sq_tl(tmp1, x2l);
fe_add(x3l, z3, z2);
fe_sub(z2l, z3, z2);
fe_mul_ttt(x2, tmp1, tmp0);
fe_sub(tmp1l, tmp1, tmp0);
fe_sq_tl(z2, z2l);
fe_mul121666(z3, tmp1l);
fe_sq_tl(x3, x3l);
fe_add(tmp0l, tmp0, z3);
fe_mul_ttt(z3, x1, z2);
fe_mul_tll(z2, tmp1l, tmp0l);
}
// here pos=-1, so r=e, so to_xz (e*P) === if swap then (x3, z3) else (x2, z2)
fe_cswap(x2, x3, swap);
fe_cswap(z2, z3, swap);

fe_invert(z2, z2);
fe_mul_ttt(x2, x2, z2);
fe_tobytes(out, x2);
}


#include <caml/memory.h>

CAMLprim value mc_25519_sub(value out, value a, value b)
Expand Down Expand Up @@ -152,6 +272,13 @@ CAMLprim value mc_25519_select(value out, value bit, value t, value f)
CAMLprim value mc_25519_invert(value out, value in)
{
CAMLparam2(out, in);
invert(Caml_ba_data_val(out), Caml_ba_data_val(in));
fe_invert(Caml_ba_data_val(out), Caml_ba_data_val(in));
CAMLreturn(Val_unit);
}

CAMLprim value mc_x25519_scalarmult(value out, value scalar, value point)
{
CAMLparam3(out, scalar, point);
x25519_scalar_mult_generic(Caml_ba_data_val(out), Caml_ba_data_val(scalar), Caml_ba_data_val(point));
CAMLreturn(Val_unit);
}

0 comments on commit 7cc310b

Please sign in to comment.