Skip to content

Commit 9d59d00

Browse files
committed
use hacl-star as curve25519 backend
The hacl-star project [1] provides verified C code for Curve25519 together with shallow OCaml bindings. Using them as a backend for the Rfc7748.X25519 module gives a nice 15x speed-up, and arguably improves the security posture. Fixes #29. [1]: https://hacl-star.github.io/
1 parent ed03421 commit 9d59d00

File tree

6 files changed

+81
-82
lines changed

6 files changed

+81
-82
lines changed

src/dune

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
(name rfc7748)
33
(public_name rfc7748)
44

5-
(libraries zarith)
5+
(libraries zarith hacl-star)
66
)

src/rfc7748.ml

Lines changed: 27 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -23,81 +23,43 @@ module type DH = sig
2323
end
2424

2525
module X25519: DH = struct
26-
type private_key = Private_key of Z.t
27-
type public_key = Public_key of Z.t
28-
29-
let key_size = 32
30-
31-
module A = struct
32-
type element = Z.t
33-
type integral = Z.t
34-
35-
let p = Z.(one lsl 255 - ~$19)
36-
37-
let bits = 255
38-
39-
let a24 = Z.of_int 121665
40-
41-
let two = Z.(~$2)
26+
open Hacl_star
4227

43-
let constant_time_conditional_swap cond a b =
44-
let c = Z.(rem cond two) in
45-
let c' = Z.(one - c) in
46-
let a' = Z.(c'*a + c*b) in
47-
let b' = Z.(c'*b + c*a) in
48-
a', b'
49-
end
50-
51-
module C = Curve.Make(Zfield.Zp(A))(Z)(A)
52-
53-
(* Quoth the RFC:
54-
set the three least significant bits of the first byte and the most significant bit
55-
of the last to zero, set the second most significant bit of the last byte to 1
56-
*)
57-
let sanitize_scalar =
58-
let unset_this = Z.logor Z.(~$7) (Z.shift_left Z.(~$128) (8*31)) in
59-
let set_that = Z.shift_left Z.(~$64) (8*31) in
60-
fun z ->
61-
Z.(z - (logand z unset_this))
62-
|> Z.logor set_that
28+
type public_key = Public_key of Hacl.C.t
29+
type private_key = Private_key of Hacl.C.t
6330

64-
let public_key_of_string: string -> public_key = fun s ->
65-
let p = Serde.z_of_hex s in
66-
let high = Z.(logand p (~$128 lsl 248)) in
67-
Public_key Z.(p - high)
31+
let key_size = 32
6832

69-
let public_key_of_bytes: Bytes.t -> public_key = fun buf ->
33+
let public_key_of_string s = Public_key (Serde.bytes_of_hex s)
34+
let public_key_of_bytes buf =
7035
assert (Bytes.length buf = key_size);
71-
let p = Serde.z_of_bytes buf in
72-
let high = Z.(logand p (~$128 lsl 248)) in
73-
Public_key Z.(p - high)
74-
75-
let string_of_public_key: public_key -> string = function Public_key pk ->
76-
Serde.hex_of_z key_size pk
77-
78-
let bytes_of_public_key: public_key -> Bytes.t = function Public_key pk ->
79-
Serde.bytes_of_z key_size pk
80-
81-
let private_key_of_string: string -> private_key = fun s ->
82-
let z = Serde.z_of_hex s |> sanitize_scalar in
83-
Private_key z
84-
85-
let private_key_of_bytes: Bytes.t -> private_key = fun buf ->
36+
Public_key (buf)
37+
let private_key_of_string s = Private_key (Serde.bytes_of_hex s)
38+
let private_key_of_bytes buf =
8639
assert (Bytes.length buf = key_size);
87-
let z = Serde.z_of_bytes buf |> sanitize_scalar in
88-
Private_key z
40+
Private_key (buf)
8941

90-
let string_of_private_key: private_key -> string = function Private_key pk ->
91-
Serde.hex_of_z key_size pk
42+
let base = public_key_of_string "0900000000000000000000000000000000000000000000000000000000000000"
9243

93-
let bytes_of_private_key: private_key -> Bytes.t = function Private_key pk ->
94-
Serde.bytes_of_z key_size pk
44+
let string_of_public_key (Public_key k) =
45+
Serde.hex_of_bytes k
46+
let string_of_private_key (Private_key k) =
47+
Serde.hex_of_bytes k
48+
let bytes_of_public_key (Public_key k) = k
49+
let bytes_of_private_key (Private_key k) = k
9550

96-
let scale (Private_key priv) (Public_key pub) = Public_key (C.scale priv pub)
9751

98-
let base = Public_key (Z.of_int 9)
52+
let scale (Private_key priv) (Public_key pub) =
53+
let out = Bytes.make 32 '\x00' in
54+
if EverCrypt.Curve25519.ecdh out priv pub then
55+
Public_key out
56+
else
57+
failwith "arrg"
58+
let public_key_of_private_key (Private_key priv) =
59+
let out = Bytes.make 32 '\x00' in
60+
EverCrypt.Curve25519.secret_to_public out priv;
61+
Public_key out
9962

100-
let public_key_of_private_key priv = scale priv base
10163
end
10264

10365
let x25519 ~priv ~pub =

src/serde.ml

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,39 @@
11

22
let z_of_bytes buf = Bytes.unsafe_to_string buf |> Z.of_bits
33

4-
let z_of_hex hex =
4+
let bytes_of_hex hex =
55
let n = String.length hex / 2 in
66
let buf = Bytes.create n in
77
let ic = Scanf.Scanning.from_string hex in
88
for i = 0 to (n - 1) do
99
Bytes.set buf i @@ Scanf.bscanf ic "%02x" char_of_int
1010
done;
11-
z_of_bytes buf
11+
buf
12+
13+
let z_of_hex hex = bytes_of_hex hex |> z_of_bytes
1214

1315
let bytes_of_z n z =
1416
let buf = Bytes.create n in
1517
let zbuf = Z.to_bits z in
1618
Bytes.blit_string zbuf 0 buf 0 String.(length zbuf);
1719
buf
1820

21+
let hex = function
22+
| n when n >= 0 && n < 10 -> char_of_int (int_of_char '0' + n)
23+
| n when n >= 10 && n < 16 -> char_of_int (int_of_char 'a' + n - 10)
24+
| _ -> assert false
25+
26+
let hex_of_bytes buf =
27+
let n = Bytes.length buf in
28+
let dst = Bytes.create (2*n) in
29+
for i = 0 to (n - 1) do
30+
let c = Bytes.get buf i |> int_of_char in
31+
Bytes.set dst (2*i) @@ hex (c / 16);
32+
Bytes.set dst (2*i + 1) @@ hex (c mod 16)
33+
done;
34+
Bytes.unsafe_to_string dst
35+
36+
1937
let hex_of_z n z =
2038
let num_hex = 2 * n in
2139
let upper_bound = n - 1 in

src/serde.mli

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11

2+
val bytes_of_hex: string -> Bytes.t
3+
val hex_of_bytes: Bytes.t -> string
4+
25
val z_of_hex: string -> Z.t
36
val hex_of_z: int -> Z.t -> string
47

test/test_misc.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ let module_suite: (module DH) -> test list = fun m ->
2020
; "base_point" >:: check_base_point]
2121

2222
let x25519_dh _ =
23-
let base = "09" in
23+
let base = X25519.(string_of_public_key base) in
2424
let alice = "77076d0a7318a57d3c16c17251b26645df4c2f87ebc0992ab177fba51db92c2a" in
2525
let bob = "5dab087e624a8a4b79e17f8b83800ee66f3bb1292618b6fd1c2f8b27ff88e0eb" in
2626
let shared_secret_alice = x25519 ~priv:alice ~pub:(x25519 ~priv:bob ~pub:base) in
@@ -42,7 +42,7 @@ let x448_dh _ =
4242
shared_secret_alice
4343

4444
let _ =
45-
"Library_Suite" >::: [ "x25519" >::: module_suite (module X25519)
45+
"MiscXYZ_Suite" >::: [ "x25519" >::: module_suite (module X25519)
4646
; "x25519_dh" >:: x25519_dh
4747
; "x448" >::: module_suite (module X448)
4848
; "x448_dh" >:: x448_dh

test/test_rfc7748.ml

Lines changed: 28 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,15 @@ type case = {priv: string; pub: string; exp: string}
1212
let to_bytes hex =
1313
Hex.to_string (`Hex hex) |> Bytes.of_string
1414

15+
(* We want to execute the slow tests only when running on CI, which is determined by the presence of the [CI] env var. *)
16+
let all_tests () =
17+
try
18+
ignore @@ Sys.getenv "CI";
19+
true
20+
with
21+
| Not_found -> false
22+
23+
1524
let black_box_test: (module DH) -> case -> test_fun = fun m {priv; pub; exp} _ ->
1625
let module M = (val m) in
1726
let out = M.scale (M.private_key_of_string priv) (M.public_key_of_string pub)
@@ -63,18 +72,25 @@ let black_box_test: (module DH) -> case2 -> test_fun = fun m {start; iter; exp}
6372
assert_equal exp out
6473

6574
let x25519_rep =
66-
[ { start="0900000000000000000000000000000000000000000000000000000000000000"
67-
; iter=1
68-
; exp="422c8e7a6227d7bca1350b3e2bb7279f7897b87bb6854b783c60e80311ae3079"}
69-
; { start="0900000000000000000000000000000000000000000000000000000000000000"
70-
; iter=1000
71-
; exp="684cf59ba83309552800ef566f2f4d3c1c3887c49360e3875f2eb94d99532c51"}
72-
(* implementation is too slow to run this within a reasonable time frame
73-
; { start="0900000000000000000000000000000000000000000000000000000000000000"
74-
; iter=1000000
75-
; exp="7c3911e0ab2586fd864497297e575e6f3bc601c0883c30df5f4dd2d24f665424"}
76-
*)
77-
]
75+
let cases =
76+
[ { start="0900000000000000000000000000000000000000000000000000000000000000"
77+
; iter=1
78+
; exp="422c8e7a6227d7bca1350b3e2bb7279f7897b87bb6854b783c60e80311ae3079"}
79+
; { start="0900000000000000000000000000000000000000000000000000000000000000"
80+
; iter=1000
81+
; exp="684cf59ba83309552800ef566f2f4d3c1c3887c49360e3875f2eb94d99532c51"}
82+
]
83+
in
84+
let cases =
85+
if all_tests () then
86+
{ start="0900000000000000000000000000000000000000000000000000000000000000"
87+
; iter=1000000
88+
; exp="7c3911e0ab2586fd864497297e575e6f3bc601c0883c30df5f4dd2d24f665424"}
89+
:: cases
90+
else
91+
cases
92+
in
93+
cases
7894
|> List.map @@ black_box_test (module X25519)
7995
|> List.map @@ fun f -> "repeated" >:: f
8096

0 commit comments

Comments
 (0)