Merge pull request #101 from hannesm/ec

NIST elliptic curves via mirage-crypto-ec

.github/workflows/test.yml

@@ -9,7 +9,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: ["4.11.1", "4.10.1", "4.09.0", "4.08.1"]
+        ocaml-version: ["4.12.0", "4.11.2", "4.10.2", "4.09.1", "4.08.1"]
         operating-system: [macos-latest, ubuntu-latest]
 
     runs-on: ${{ matrix.operating-system }}
@@ -30,7 +30,8 @@ jobs:
           opam pin add -n mirage-crypto-rng-mirage.dev .
           opam pin add -n mirage-crypto-rng-async.dev .
           opam pin add -n mirage-crypto-pk.dev .
-          opam depext -y mirage-crypto mirage-crypto-rng mirage-crypto-rng-mirage mirage-crypto-pk
+          opam pin add -n mirage-crypto-ec.dev .
+          opam depext -y mirage-crypto mirage-crypto-rng mirage-crypto-rng-mirage mirage-crypto-pk mirage-crypto-ec
           opam install -t --deps-only .
 
       - name: Build

.github/workflows/windows.yml

@@ -9,7 +9,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: ["4.11.1", "4.10.1", "4.09.0", "4.08.1"]
+        ocaml-version: ["4.12.0", "4.11.2", "4.10.2", "4.09.1", "4.08.1"]
         operating-system: [windows-latest]
 
     runs-on: ${{ matrix.operating-system }}
@@ -29,11 +29,12 @@ jobs:
           opam pin add -n mirage-crypto-rng.dev .
           opam pin add -n mirage-crypto-rng-mirage.dev .
           opam pin add -n mirage-crypto-pk.dev .
-          opam depext -y mirage-crypto mirage-crypto-rng mirage-crypto-rng-mirage mirage-crypto-pk
-          opam install -t --deps-only mirage-crypto mirage-crypto-rng mirage-crypto-rng-mirage mirage-crypto-pk
+          opam pin add -n mirage-crypto-ec.dev .
+          opam depext -y mirage-crypto mirage-crypto-rng mirage-crypto-rng-mirage mirage-crypto-pk mirage-crypto-ec
+          opam install -t --deps-only mirage-crypto mirage-crypto-rng mirage-crypto-rng-mirage mirage-crypto-pk mirage-crypto-ec
 
       - name: Build
-        run: opam exec -- dune build -p mirage-crypto,mirage-crypto-rng,mirage-crypto-rng-mirage,mirage-crypto-pk
+        run: opam exec -- dune build -p mirage-crypto,mirage-crypto-rng,mirage-crypto-rng-mirage,mirage-crypto-pk,mirage-crypto-ec
 
       - name: Test
-        run: opam exec -- dune runtest -p mirage-crypto,mirage-crypto-rng,mirage-crypto-rng-mirage,mirage-crypto-pk
+        run: opam exec -- dune runtest -p mirage-crypto,mirage-crypto-rng,mirage-crypto-rng-mirage,mirage-crypto-pk,mirage-crypto-ec

.travis.yml

@@ -6,7 +6,7 @@ services:
 os: linux
 env:
   global:
-    - PINS="mirage-crypto:. mirage-crypto-rng:. mirage-crypto-rng-mirage:. mirage-crypto-pk:. mirage-crypto-rng-async:."
+    - PINS="mirage-crypto:. mirage-crypto-rng:. mirage-crypto-rng-mirage:. mirage-crypto-pk:. mirage-crypto-rng-async:. mirage-crypto-ec:."
     - PACKAGE="mirage-crypto-pk"
     - TESTS=true
     - DISTRO=alpine

META.mirage-crypto-ec.template

@@ -0,0 +1,3 @@
+# DUNE_GEN
+
+freestanding_linkopts = "-l:libmirage_crypto_ec_freestanding_stubs.a"

dune-project

@@ -1,2 +1,3 @@
 (lang dune 2.6)
 (name mirage-crypto)
+(formatting disabled)

ec-freestanding/Makefile

@@ -0,0 +1,24 @@
+PKG_CONFIG_PATH := $(shell opam config var prefix)/lib/pkgconfig
+
+EXISTS := $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) pkg-config --exists ocaml-freestanding; echo $$?)
+
+.PHONY: all clean
+all: libmirage_crypto_ec_freestanding_stubs.a
+
+ifeq ($(EXISTS), 1)
+libmirage_crypto_ec_freestanding_stubs.a:
+	touch $@
+else
+CC ?= cc
+FREESTANDING_CFLAGS := $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) pkg-config --cflags ocaml-freestanding)
+DISCOVER_CFLAGS := $(shell sed 's/^(\(.*\))$$/\1/' ../ec/cflags_optimized.sexp | tr -d '"')
+CFLAGS := -O3 -I../ec/native -I../src/native $(DISCOVER_CFLAGS) $(FREESTANDING_CFLAGS)
+
+OBJS=p224_stubs.o np224_stubs.o p256_stubs.o np256_stubs.o p384_stubs.o np384_stubs.o p521_stubs.o np521_stubs.o
+
+libmirage_crypto_ec_freestanding_stubs.a: $(OBJS)
+	$(AR) r $@ $^
+endif
+
+clean:
+	$(RM) $(OBJS) libmirage_crypto_ec_freestanding_stubs.a

ec-freestanding/dune

@@ -0,0 +1,16 @@
+(copy_files# ../ec/native/*.c)
+
+(rule
+ (deps ../ec/cflags_optimized.sexp ../src/native/mirage_crypto.h
+   ../src/native/bitfn.h Makefile p224_stubs.c np224_stubs.c p256_stubs.c
+   np256_stubs.c p384_stubs.c np384_stubs.c p521_stubs.c np521_stubs.c)
+ (targets libmirage_crypto_ec_freestanding_stubs.a)
+ (action
+  (no-infer
+   (progn
+    (run %{make})))))
+
+(install
+ (package mirage-crypto-ec)
+ (section lib)
+ (files libmirage_crypto_ec_freestanding_stubs.a))

ec/LICENSE.md

@@ -0,0 +1,31 @@
+The MIT License
+
+Copyright (c) 2019 Etienne Millon
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+
+
+C stubs in `p256_32.h`, `p256_64.h` and `p256_stubs.c` were generated using
+Fiat (https://github.com/mit-plv/fiat-crypto) and thus these files are
+licensed under the MIT license with the following copyright :
+----------------------------
+Copyright (c) 2015-2016 Andres Erbsen <[email protected]>
+                        Google Inc.
+                        Jade Philipoom <[email protected]> <[email protected]>
+                        Massachusetts Institute of Technology

ec/dune

@@ -0,0 +1,22 @@
+(library
+ (name mirage_crypto_ec)
+ (public_name mirage-crypto-ec)
+ (libraries cstruct eqaf.cstruct mirage-crypto mirage-crypto-rng)
+ (foreign_stubs
+  (language c)
+  (names p224_stubs np224_stubs p256_stubs np256_stubs p384_stubs np384_stubs
+    p521_stubs np521_stubs)
+  (flags
+   (:standard -I../src/native)
+   (:include cflags_optimized.sexp))))
+
+(env
+ (dev
+  (c_flags (-Werror))))
+
+(include_subdirs unqualified)
+
+(rule
+ (targets cflags_optimized.sexp)
+ (action
+  (run ../config/cfg.exe)))

ec/implementation.mld

@@ -0,0 +1,72 @@
+{1 Implementation }
+
+The goal of this document is to describe how the library is implemented.
+
+{2 Field operations}
+
+These are implemented in [Field_element], which is a binding over
+[p256_{32,64}.h]. These are files extracted from Coq code in
+{{:https://github.com/mit-plv/fiat-crypto}this repository}.
+
+This module uses
+{{:https://en.wikipedia.org/wiki/Montgomery_modular_multiplication} Montgomery
+Modular Multiplication}. Instead of storing a number [a], operations are done
+on [aR] where R = 2{^256}.
+
+It is possible to check that these files correspond to the extracted ones in
+the upstream repository by running [dune build @check_vendors].
+
+These files are part of the trusted computing base. That is, using this package
+relies on the fact that they implemented the correct algorithms. To go further,
+one can re-run the extraction process from Coq sources, see
+{{:https://github.com/mirage/fiat/issues/41}#41}.
+
+{2 Point operations}
+
+Points (see the [Point] module) are stored using projective coordinates (X : Y
+: Z):
+
+- Z=0 corresponds to the point at infinity
+- for Z≠0, this corresponds to a point with affine coordinates (X/Z{^2},
+  Y/Z{^3})
+
+Doubling and addition are implemented as C stubs in [p256_stubs.c] using code
+that comes from BoringSSL, Google's fork of OpenSSL. Fiat code has been design
+in part to be included in BoringSSL, so this does not require any particular
+glue code.
+
+Some operations are implemented manually, in particular:
+
+- conversion to affine coordinates, as described above. This relies on a field
+  inversion primitive from BoringSSL, that is exposed in [Field_element].
+- point verification (bound checking and making sure that the equation is
+  satisfied).
+
+There is no automated way to check that the BoringSSL part is identical to that
+in the upstream repository (nor to update it).
+
+{2 Scalar multiplication}
+
+Implemented by hand using the
+{{:https://cr.yp.to/bib/2003/joye-ladder.pdf}Montgomery Powering Ladder}.
+
+Instead of branching based on key bits, constant-time selection (as defined in
+fiat code) is used.
+
+The following references discuss this algorithm:
+
+- {{:https://cryptojedi.org/peter/data/eccss-20130911b.pdf}Scalar-multiplication algorithms, Peter Schwabe, ECC 2013 Summer School}
+- {{:https://eprint.iacr.org/2017/293.pdf}Montgomery curves and the Montgomery
+ladder, Daniel J. Bernstein and Tanja Lange}
+
+{2 Key exchange}
+
+Key exchange consists in
+
+- validating the public key as described in
+  {{:https://tools.ietf.org/html/rfc8446#section-4.2.8.2}RFC 8446 §4.2.8.2};
+- computing scalar multiplication;
+- returning the encoded x coordinate of the result.
+
+This is implemented by hand and checked against common errors using test
+vectors from {{:https://github.com/google/wycheproof}project Wycheproof}.