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/
burgerdev · Oct 30, 2020 · a01828a · a01828a
1 parent ed03421
commit a01828a
Show file tree

Hide file tree

Showing 7 changed files with 82 additions and 82 deletions.
diff --git a/rfc7748.opam b/rfc7748.opam
@@ -13,6 +13,7 @@ build: [
 ]
 depends: [
   "ocaml" { >= "4.03" }
+  "hacl-star" { >= "0.2.2" }
   "zarith" { >= "1.5" }
   "dune" { build & >= "1.2.1" }
   "ounit" { with-test & >= "2.0.5" }

diff --git a/src/dune b/src/dune
@@ -2,5 +2,5 @@
  (name rfc7748)
  (public_name rfc7748)
 
- (libraries zarith)
+ (libraries zarith hacl-star)
 )
diff --git a/src/rfc7748.ml b/src/rfc7748.ml
@@ -23,81 +23,43 @@ module type DH = sig
 end
 
 module X25519: DH = struct
-  type private_key = Private_key of Z.t
-  type public_key = Public_key of Z.t
-
-  let key_size = 32
-
-  module A = struct
-    type element = Z.t
-    type integral = Z.t
-
-    let p = Z.(one lsl 255 - ~$19)
-
-    let bits = 255
-
-    let a24 = Z.of_int 121665
-
-    let two = Z.(~$2)
+  open Hacl_star
 
-    let constant_time_conditional_swap cond a b =
-      let c = Z.(rem cond two) in
-      let c' = Z.(one - c) in
-      let a' = Z.(c'*a + c*b) in
-      let b' = Z.(c'*b + c*a) in
-      a', b'
-  end
-
-  module C = Curve.Make(Zfield.Zp(A))(Z)(A)
-
-  (* Quoth the RFC:
-     set the three least significant bits of the first byte and the most significant bit
-     of the last to zero, set the second most significant bit of the last byte to 1
-  *)
-  let sanitize_scalar =
-    let unset_this = Z.logor Z.(~$7) (Z.shift_left Z.(~$128) (8*31)) in
-    let set_that = Z.shift_left Z.(~$64) (8*31) in
-    fun z ->
-      Z.(z - (logand z unset_this))
-      |> Z.logor set_that
+  type public_key = Public_key of Hacl.C.t
+  type private_key = Private_key of Hacl.C.t
 
-  let public_key_of_string: string -> public_key = fun s ->
-    let p = Serde.z_of_hex s in
-    let high = Z.(logand p (~$128 lsl 248)) in
-    Public_key Z.(p - high)
+  let key_size = 32
 
-  let public_key_of_bytes: Bytes.t -> public_key = fun buf ->
+  let public_key_of_string s = Public_key (Serde.bytes_of_hex s)
+  let public_key_of_bytes buf =
     assert (Bytes.length buf = key_size);
-    let p = Serde.z_of_bytes buf in
-    let high = Z.(logand p (~$128 lsl 248)) in
-    Public_key Z.(p - high)
-
-  let string_of_public_key: public_key -> string = function Public_key pk ->
-    Serde.hex_of_z key_size pk
-
-  let bytes_of_public_key: public_key -> Bytes.t = function Public_key pk ->
-    Serde.bytes_of_z key_size pk
-
-  let private_key_of_string: string -> private_key = fun s ->
-    let z = Serde.z_of_hex s |> sanitize_scalar in
-    Private_key z
-
-  let private_key_of_bytes: Bytes.t -> private_key = fun buf ->
+    Public_key (buf)
+  let private_key_of_string s = Private_key (Serde.bytes_of_hex s)
+  let private_key_of_bytes buf =
     assert (Bytes.length buf = key_size);
-    let z = Serde.z_of_bytes buf |> sanitize_scalar in
-    Private_key z
+    Private_key (buf)
 
-  let string_of_private_key: private_key -> string = function Private_key pk ->
-    Serde.hex_of_z key_size pk
+  let base = public_key_of_string "0900000000000000000000000000000000000000000000000000000000000000"
 
-  let bytes_of_private_key: private_key -> Bytes.t = function Private_key pk ->
-    Serde.bytes_of_z key_size pk
+  let string_of_public_key (Public_key k) =
+    Serde.hex_of_bytes k
+  let string_of_private_key (Private_key k) =
+    Serde.hex_of_bytes k
+  let bytes_of_public_key (Public_key k) = k
+  let bytes_of_private_key (Private_key k) = k
 
-  let scale (Private_key priv) (Public_key pub) = Public_key (C.scale priv pub)
 
-  let base = Public_key (Z.of_int 9)
+  let scale (Private_key priv) (Public_key pub) =
+    let out = Bytes.make 32 '\x00' in 
+    if EverCrypt.Curve25519.ecdh out priv pub then
+      Public_key out
+    else
+      failwith "arrg"
+  let public_key_of_private_key (Private_key priv) =
+    let out = Bytes.make 32 '\x00' in 
+    EverCrypt.Curve25519.secret_to_public out priv;
+    Public_key out
 
-  let public_key_of_private_key priv = scale priv base
 end
 
 let x25519 ~priv ~pub =

diff --git a/src/serde.ml b/src/serde.ml
@@ -1,21 +1,39 @@
 
 let z_of_bytes buf = Bytes.unsafe_to_string buf |> Z.of_bits
 
-let z_of_hex hex =
+let bytes_of_hex hex =
   let n = String.length hex / 2 in
   let buf = Bytes.create n in
   let ic = Scanf.Scanning.from_string hex in
   for i = 0 to (n - 1) do
     Bytes.set buf i @@ Scanf.bscanf ic "%02x" char_of_int
   done;
-  z_of_bytes buf
+  buf
+
+let z_of_hex hex = bytes_of_hex hex |> z_of_bytes
 
 let bytes_of_z n z =
   let buf = Bytes.create n in
   let zbuf = Z.to_bits z in
   Bytes.blit_string zbuf 0 buf 0 String.(length zbuf);
   buf
 
+let hex = function
+  | n when n >= 0 && n < 10 -> char_of_int (int_of_char '0' + n)
+  | n when n >= 10 && n < 16 -> char_of_int (int_of_char 'a' + n - 10)
+  | _ -> assert false
+
+let hex_of_bytes buf = 
+  let n = Bytes.length buf in
+  let dst = Bytes.create (2*n) in
+  for i = 0 to (n - 1) do
+    let c = Bytes.get buf i |> int_of_char in
+    Bytes.set dst (2*i) @@ hex (c / 16);
+    Bytes.set dst (2*i + 1) @@ hex (c mod 16)
+  done;
+  Bytes.unsafe_to_string dst
+
+
 let hex_of_z n z =
   let num_hex = 2 * n in
   let upper_bound = n - 1 in

diff --git a/src/serde.mli b/src/serde.mli
@@ -1,4 +1,7 @@
 
+val bytes_of_hex: string -> Bytes.t
+val hex_of_bytes: Bytes.t -> string
+
 val z_of_hex: string -> Z.t
 val hex_of_z: int -> Z.t -> string
 

diff --git a/test/test_misc.ml b/test/test_misc.ml
@@ -20,7 +20,7 @@ let module_suite: (module DH) -> test list = fun m ->
   ; "base_point" >:: check_base_point]
 
 let x25519_dh _ =
-  let base = "09" in
+  let base = X25519.(string_of_public_key base) in
   let alice = "77076d0a7318a57d3c16c17251b26645df4c2f87ebc0992ab177fba51db92c2a" in
   let bob = "5dab087e624a8a4b79e17f8b83800ee66f3bb1292618b6fd1c2f8b27ff88e0eb" in
   let shared_secret_alice = x25519 ~priv:alice ~pub:(x25519 ~priv:bob ~pub:base) in
@@ -42,7 +42,7 @@ let x448_dh _ =
     shared_secret_alice
 
 let _ =
-  "Library_Suite" >::: [ "x25519" >::: module_suite (module X25519)
+  "MiscXYZ_Suite" >::: [ "x25519" >::: module_suite (module X25519)
                        ; "x25519_dh" >:: x25519_dh
                        ; "x448" >::: module_suite (module X448)
                        ; "x448_dh" >:: x448_dh

diff --git a/test/test_rfc7748.ml b/test/test_rfc7748.ml
@@ -12,6 +12,15 @@ type case = {priv: string; pub: string; exp: string}
 let to_bytes hex =
   Hex.to_string (`Hex hex) |> Bytes.of_string
 
+(* We want to execute the slow tests only when running on CI, which is determined by the presence of the [CI] env var. *)
+let all_tests () =
+  try
+    ignore @@ Sys.getenv "CI";
+    true
+  with
+  | Not_found -> false
+
+
 let black_box_test: (module DH) -> case -> test_fun = fun m {priv; pub; exp} _ ->
   let module M = (val m) in
   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}
   assert_equal exp out
 
 let x25519_rep =
-  [ { start="0900000000000000000000000000000000000000000000000000000000000000"
-    ; iter=1
-    ; exp="422c8e7a6227d7bca1350b3e2bb7279f7897b87bb6854b783c60e80311ae3079"}
-  ; { start="0900000000000000000000000000000000000000000000000000000000000000"
-    ; iter=1000
-    ; exp="684cf59ba83309552800ef566f2f4d3c1c3887c49360e3875f2eb94d99532c51"}
-    (* implementation is too slow to run this within a reasonable time frame
-       ; { start="0900000000000000000000000000000000000000000000000000000000000000"
-       ; iter=1000000
-       ; exp="7c3911e0ab2586fd864497297e575e6f3bc601c0883c30df5f4dd2d24f665424"}
-    *)
-  ]
+  let cases =
+    [ { start="0900000000000000000000000000000000000000000000000000000000000000"
+      ; iter=1
+      ; exp="422c8e7a6227d7bca1350b3e2bb7279f7897b87bb6854b783c60e80311ae3079"}
+    ; { start="0900000000000000000000000000000000000000000000000000000000000000"
+      ; iter=1000
+      ; exp="684cf59ba83309552800ef566f2f4d3c1c3887c49360e3875f2eb94d99532c51"}
+    ]
+  in
+  let cases =
+    if all_tests () then
+      { start="0900000000000000000000000000000000000000000000000000000000000000"
+      ; iter=1000000
+      ; exp="7c3911e0ab2586fd864497297e575e6f3bc601c0883c30df5f4dd2d24f665424"}
+      :: cases
+    else
+      cases
+  in
+  cases
   |> List.map @@ black_box_test (module X25519)
   |> List.map @@ fun f -> "repeated" >:: f