Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

use hacl-star as curve25519 backend #39

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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/
  • Loading branch information
burgerdev committed Oct 30, 2020
commit a01828aaef00219c905bfa45885dab12408d19db
1 change: 1 addition & 0 deletions rfc7748.opam
Original file line number Diff line number Diff line change
@@ -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" }
2 changes: 1 addition & 1 deletion src/dune
Original file line number Diff line number Diff line change
@@ -2,5 +2,5 @@
(name rfc7748)
(public_name rfc7748)

(libraries zarith)
(libraries zarith hacl-star)
)
92 changes: 27 additions & 65 deletions src/rfc7748.ml
Original file line number Diff line number Diff line change
@@ -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 =
22 changes: 20 additions & 2 deletions src/serde.ml
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions src/serde.mli
Original file line number Diff line number Diff line change
@@ -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

4 changes: 2 additions & 2 deletions test/test_misc.ml
Original file line number Diff line number Diff line change
@@ -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
40 changes: 28 additions & 12 deletions test/test_rfc7748.ml
Original file line number Diff line number Diff line change
@@ -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