ECDH: Add the Everest X25519 implementation

3rdparty/.gitignore

@@ -0,0 +1 @@
+/Makefile

3rdparty/CMakeLists.txt

@@ -0,0 +1,11 @@
+list (APPEND thirdparty_src)
+list (APPEND thirdparty_lib)
+list (APPEND thirdparty_inc)
+list (APPEND thirdparty_def)
+
+add_subdirectory(everest)
+
+set(thirdparty_src ${thirdparty_src} PARENT_SCOPE)
+set(thirdparty_lib ${thirdparty_lib} PARENT_SCOPE)
+set(thirdparty_inc ${thirdparty_inc} PARENT_SCOPE)
+set(thirdparty_def ${thirdparty_def} PARENT_SCOPE)

3rdparty/Makefile.inc

@@ -0,0 +1,2 @@
+include ../3rdparty/everest/Makefile.inc
+

3rdparty/everest/.gitignore

@@ -0,0 +1,2 @@
+*.o
+Makefile

3rdparty/everest/CMakeLists.txt

@@ -0,0 +1,31 @@
+list (APPEND everest_src)
+list (APPEND everest_inc)
+list (APPEND everest_def)
+
+set(everest_src
+  ${CMAKE_CURRENT_SOURCE_DIR}/library/everest.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/library/x25519.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/library/Hacl_Curve25519_joined.c
+)
+
+list(APPEND everest_inc ${CMAKE_CURRENT_SOURCE_DIR}/../../include ${CMAKE_CURRENT_SOURCE_DIR}/include ${CMAKE_CURRENT_SOURCE_DIR}/include/everest ${CMAKE_CURRENT_SOURCE_DIR}/include/everest/kremlib)
+
+execute_process(COMMAND ${PERL_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/../../scripts/config.pl -f ${CMAKE_CURRENT_SOURCE_DIR}/../../include/mbedtls/config.h get MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED RESULT_VARIABLE result)
+
+if(${result} EQUAL 0)
+
+  if(INSTALL_MBEDTLS_HEADERS)
+
+    install(DIRECTORY include/everest
+      DESTINATION include
+      FILE_PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ
+      DIRECTORY_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE
+      FILES_MATCHING PATTERN "*.h")
+
+  endif(INSTALL_MBEDTLS_HEADERS)
+
+endif()
+
+set(thirdparty_src ${thirdparty_src} ${everest_src} PARENT_SCOPE)
+set(thirdparty_inc ${thirdparty_inc} ${everest_inc} PARENT_SCOPE)
+set(thirdparty_def ${thirdparty_def} ${everest_def} PARENT_SCOPE)

3rdparty/everest/Makefile.inc

@@ -0,0 +1,6 @@
+THIRDPARTY_INCLUDES+=-I../3rdparty/everest/include -I../3rdparty/everest/include/everest -I../3rdparty/everest/include/everest/kremlib
+
+THIRDPARTY_CRYPTO_OBJECTS+= \
+	../3rdparty/everest/library/everest.o \
+	../3rdparty/everest/library/x25519.o \
+	../3rdparty/everest/library/Hacl_Curve25519_joined.o

3rdparty/everest/README.md

@@ -0,0 +1,5 @@
+The files in this directory stem from [Project Everest](https://project-everest.github.io/) and are distributed under the Apache 2.0 license.
+
+This is a formally verified implementation of Curve25519-based handshakes. The C code is automatically derived from the (verified) [original implementation](https://github.com/project-everest/hacl-star/tree/master/code/curve25519) in the [F* language](https://github.com/fstarlang/fstar) by [KreMLin](https://github.com/fstarlang/kremlin). In addition to the improved safety and security of the implementation, it is also significantly faster than the default implementation of Curve25519 in mbedTLS.
+
+The caveat is that not all platforms are supported, although the version in `everest/library/legacy` should work on most systems. The main issue is that some platforms do not provide a 128-bit integer type and KreMLin therefore has to use additional (also verified) code to simulate them, resulting in less of a performance gain overall. Explictly supported platforms are currently `x86` and `x86_64` using gcc or clang, and Visual C (2010 and later).

3rdparty/everest/include/everest/Hacl_Curve25519.h

@@ -0,0 +1,21 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+/* This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
+ * KreMLin invocation: /mnt/e/everest/verify/kremlin/krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -fbuiltin-uint128 -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -I /mnt/e/everest/verify/hacl-star/code/lib/kremlin -I /mnt/e/everest/verify/kremlin/kremlib/compat -I /mnt/e/everest/verify/hacl-star/specs -I /mnt/e/everest/verify/hacl-star/specs/old -I . -ccopt -march=native -verbose -ldopt -flto -tmpdir x25519-c -I ../bignum -bundle Hacl.Curve25519=* -minimal -add-include "kremlib.h" -skip-compilation x25519-c/out.krml -o x25519-c/Hacl_Curve25519.c
+ * F* version: 059db0c8
+ * KreMLin version: 916c37ac
+ */
+
+
+
+#ifndef __Hacl_Curve25519_H
+#define __Hacl_Curve25519_H
+
+
+#include "kremlib.h"
+
+void Hacl_Curve25519_crypto_scalarmult(uint8_t *mypublic, uint8_t *secret, uint8_t *basepoint);
+
+#define __Hacl_Curve25519_H_DEFINED
+#endif

3rdparty/everest/include/everest/everest.h

@@ -0,0 +1,234 @@
+/*
+ *  Interface to code from Project Everest
+ *
+ *  Copyright 2016-2018 INRIA and Microsoft Corporation
+ *  SPDX-License-Identifier: Apache-2.0
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License"); you may
+ *  not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+ *  WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *  This file is part of Mbed TLS (https://tls.mbed.org).
+ */
+
+#ifndef MBEDTLS_EVEREST_H
+#define MBEDTLS_EVEREST_H
+
+#include "everest/x25519.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+ * Defines the source of the imported EC key.
+ */
+typedef enum
+{
+    MBEDTLS_EVEREST_ECDH_OURS,   /**< Our key. */
+    MBEDTLS_EVEREST_ECDH_THEIRS, /**< The key of the peer. */
+} mbedtls_everest_ecdh_side;
+
+typedef struct {
+    mbedtls_x25519_context ctx;
+} mbedtls_ecdh_context_everest;
+
+
+/**
+ * \brief           This function sets up the ECDH context with the information
+ *                  given.
+ *
+ *                  This function should be called after mbedtls_ecdh_init() but
+ *                  before mbedtls_ecdh_make_params(). There is no need to call
+ *                  this function before mbedtls_ecdh_read_params().
+ *
+ *                  This is the first function used by a TLS server for ECDHE
+ *                  ciphersuites.
+ *
+ * \param ctx       The ECDH context to set up.
+ * \param grp_id    The group id of the group to set up the context for.
+ *
+ * \return          \c 0 on success.
+ */
+int mbedtls_everest_setup( mbedtls_ecdh_context_everest *ctx, int grp_id );
+
+/**
+ * \brief           This function frees a context.
+ *
+ * \param ctx       The context to free.
+ */
+void mbedtls_everest_free( mbedtls_ecdh_context_everest *ctx );
+
+/**
+ * \brief           This function generates a public key and a TLS
+ *                  ServerKeyExchange payload.
+ *
+ *                  This is the second function used by a TLS server for ECDHE
+ *                  ciphersuites. (It is called after mbedtls_ecdh_setup().)
+ *
+ * \note            This function assumes that the ECP group (grp) of the
+ *                  \p ctx context has already been properly set,
+ *                  for example, using mbedtls_ecp_group_load().
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param olen      The number of characters written.
+ * \param buf       The destination buffer.
+ * \param blen      The length of the destination buffer.
+ * \param f_rng     The RNG function.
+ * \param p_rng     The RNG context.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_make_params( mbedtls_ecdh_context_everest *ctx, size_t *olen,
+                                 unsigned char *buf, size_t blen,
+                                 int( *f_rng )( void *, unsigned char *, size_t ),
+                                 void *p_rng );
+
+/**
+ * \brief           This function parses and processes a TLS ServerKeyExhange
+ *                  payload.
+ *
+ *                  This is the first function used by a TLS client for ECDHE
+ *                  ciphersuites.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param buf       The pointer to the start of the input buffer.
+ * \param end       The address for one Byte past the end of the buffer.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ *
+ */
+int mbedtls_everest_read_params( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char **buf, const unsigned char *end );
+
+/**
+ * \brief           This function parses and processes a TLS ServerKeyExhange
+ *                  payload.
+ *
+ *                  This is the first function used by a TLS client for ECDHE
+ *                  ciphersuites.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param buf       The pointer to the start of the input buffer.
+ * \param end       The address for one Byte past the end of the buffer.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ *
+ */
+int mbedtls_everest_read_params( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char **buf, const unsigned char *end );
+
+/**
+ * \brief           This function sets up an ECDH context from an EC key.
+ *
+ *                  It is used by clients and servers in place of the
+ *                  ServerKeyEchange for static ECDH, and imports ECDH
+ *                  parameters from the EC key information of a certificate.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context to set up.
+ * \param key       The EC key to use.
+ * \param side      Defines the source of the key: 1: Our key, or
+ *                  0: The key of the peer.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ *
+ */
+int mbedtls_everest_get_params( mbedtls_ecdh_context_everest *ctx, const mbedtls_ecp_keypair *key,
+                                mbedtls_everest_ecdh_side side );
+
+/**
+ * \brief           This function generates a public key and a TLS
+ *                  ClientKeyExchange payload.
+ *
+ *                  This is the second function used by a TLS client for ECDH(E)
+ *                  ciphersuites.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param olen      The number of Bytes written.
+ * \param buf       The destination buffer.
+ * \param blen      The size of the destination buffer.
+ * \param f_rng     The RNG function.
+ * \param p_rng     The RNG context.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_make_public( mbedtls_ecdh_context_everest *ctx, size_t *olen,
+                                 unsigned char *buf, size_t blen,
+                                 int( *f_rng )( void *, unsigned char *, size_t ),
+                                 void *p_rng );
+
+/**
+ * \brief       This function parses and processes a TLS ClientKeyExchange
+ *              payload.
+ *
+ *              This is the third function used by a TLS server for ECDH(E)
+ *              ciphersuites. (It is called after mbedtls_ecdh_setup() and
+ *              mbedtls_ecdh_make_params().)
+ *
+ * \see         ecp.h
+ *
+ * \param ctx   The ECDH context.
+ * \param buf   The start of the input buffer.
+ * \param blen  The length of the input buffer.
+ *
+ * \return      \c 0 on success.
+ * \return      An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_read_public( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char *buf, size_t blen );
+
+/**
+ * \brief           This function derives and exports the shared secret.
+ *
+ *                  This is the last function used by both TLS client
+ *                  and servers.
+ *
+ * \note            If \p f_rng is not NULL, it is used to implement
+ *                  countermeasures against side-channel attacks.
+ *                  For more information, see mbedtls_ecp_mul().
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param olen      The number of Bytes written.
+ * \param buf       The destination buffer.
+ * \param blen      The length of the destination buffer.
+ * \param f_rng     The RNG function.
+ * \param p_rng     The RNG context.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_calc_secret( mbedtls_ecdh_context_everest *ctx, size_t *olen,
+                                 unsigned char *buf, size_t blen,
+                                 int( *f_rng )( void *, unsigned char *, size_t ),
+                                 void *p_rng );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* MBEDTLS_EVEREST_H */

3rdparty/everest/include/everest/kremlib.h

@@ -0,0 +1,29 @@
+/*
+ *  Copyright 2016-2018 INRIA and Microsoft Corporation
+ *
+ *  SPDX-License-Identifier: Apache-2.0
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License"); you may
+ *  not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+ *  WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *  This file is part of Mbed TLS (https://tls.mbed.org) and
+ *  originated from Project Everest (https://project-everest.github.io/)
+ */
+
+#ifndef __KREMLIB_H
+#define __KREMLIB_H
+
+#include "kremlin/internal/target.h"
+#include "kremlin/internal/types.h"
+#include "kremlin/c_endianness.h"
+
+#endif     /* __KREMLIB_H */