Bug 1783647 - Integrate Vale Curve25519 r=nss-reviewers,bbeurdouche

Differential Revision: https://phabricator.services.mozilla.com/D153944

7 files changed, 218 insertions, 2 deletions

diff --git a/automation/taskcluster/scripts/run_hacl.sh b/automation/taskcluster/scripts/run_hacl.sh
index e414b9aa5..44bdb8388 100755
--- a/automation/taskcluster/scripts/run_hacl.sh
+++ b/automation/taskcluster/scripts/run_hacl.sh
@@ -36,7 +36,7 @@ for f in "${files[@]}"; do
     diff $hacl_file $f
 done
 
-files=($(find ~/nss/lib/freebl/verified/ -type f -name '*.[ch]' -not -path "*/freebl/verified/internal/*"))
+files=($(find ~/nss/lib/freebl/verified/ -type f -name '*.[ch]' -not -path "*/freebl/verified/internal/*" -not -path "*/freebl/verified/config.h"))
 for f in "${files[@]}"; do
     file_name=$(basename "$f")
     hacl_file=($(find ~/hacl-star/dist/mozilla/ ~/hacl-star/dist/karamel/ -type f -name $file_name -not -path "*/hacl-star/dist/mozilla/internal/*"))
diff --git a/lib/freebl/Makefile b/lib/freebl/Makefile
index aa9dd95fd..74e8e6545 100644
--- a/lib/freebl/Makefile
+++ b/lib/freebl/Makefile
@@ -568,6 +568,7 @@ ifneq ($(shell $(CC) -? 2>&1 >/dev/null </dev/null | sed -e 's/:.*//;1q'),lcc)
             HAVE_INT128_SUPPORT = 1
             DEFINES += -DHAVE_INT128_SUPPORT
     else ifeq (1,$(CC_IS_GCC))
+        SUPPORTS_VALE_CURVE25519 = 1
         ifneq (,$(filter 4.6 4.7 4.8 4.9,$(word 1,$(GCC_VERSION)).$(word 2,$(GCC_VERSION))))
             HAVE_INT128_SUPPORT = 1
             DEFINES += -DHAVE_INT128_SUPPORT
@@ -592,6 +593,11 @@ ifndef HAVE_INT128_SUPPORT
     DEFINES += -DKRML_VERIFIED_UINT128
 endif
 
+ifdef SUPPORTS_VALE_CURVE25519
+    VERIFIED_SRCS += Hacl_Curve25519_64.c
+    DEFINES += -DHACL_CAN_COMPILE_INLINE_ASM
+endif
+
 ifndef NSS_DISABLE_CHACHAPOLY
     ifeq ($(CPU_ARCH),x86_64)
         ifndef NSS_DISABLE_AVX2
diff --git a/lib/freebl/ecl/curve25519_64.c b/lib/freebl/ecl/curve25519_64.c
index 7c3c67d6b..e346bdb8b 100644
--- a/lib/freebl/ecl/curve25519_64.c
+++ b/lib/freebl/ecl/curve25519_64.c
@@ -3,12 +3,22 @@
  * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
 
 #include "ecl-priv.h"
+
+#if HACL_CAN_COMPILE_INLINE_ASM
+#include "../verified/Hacl_Curve25519_64.h"
+#else
 #include "../verified/Hacl_Curve25519_51.h"
+#endif
 
 SECStatus
 ec_Curve25519_mul(uint8_t *mypublic, const uint8_t *secret, const uint8_t *basepoint)
 {
-    // Note: this cast is safe because HaCl* state has a post-condition that only "mypublic" changed.
+// Note: this cast is safe because HaCl* state has a post-condition that only "mypublic" changed.
+#if defined HACL_CAN_COMPILE_INLINE_ASM
+    Hacl_Curve25519_64_ecdh(mypublic, (uint8_t *)secret, (uint8_t *)basepoint);
+#else
     Hacl_Curve25519_51_ecdh(mypublic, (uint8_t *)secret, (uint8_t *)basepoint);
+#endif
+
     return 0;
 }
diff --git a/lib/freebl/freebl.gyp b/lib/freebl/freebl.gyp
index 23940ef77..65f9a8013 100644
--- a/lib/freebl/freebl.gyp
+++ b/lib/freebl/freebl.gyp
@@ -866,6 +866,12 @@
           }],
         ],
       }],
+      [ 'supports_vale_curve25519==1', {
+        'defines': [
+          # The Makefile does version-tests on GCC, but we're not doing that here.
+          'HACL_CAN_COMPILE_INLINE_ASM',
+        ],
+      }],
       [ 'OS=="linux" or OS=="android"', {
         'conditions': [
           [ 'target_arch=="x64"', {
@@ -928,6 +934,11 @@
   'variables': {
     'module': 'nss',
     'conditions': [
+      [ 'target_arch=="x64" and cc_is_gcc==1', {
+        'supports_vale_curve25519%': 1,
+      }, {
+        'supports_vale_curve25519%': 0,
+      }],
       [ 'target_arch=="x64" or target_arch=="arm64" or target_arch=="aarch64"', {
         'have_int128_support%': 1,
       }, {
diff --git a/lib/freebl/freebl_base.gypi b/lib/freebl/freebl_base.gypi
index 34b6b3c81..d198c442b 100644
--- a/lib/freebl/freebl_base.gypi
+++ b/lib/freebl/freebl_base.gypi
@@ -151,6 +151,11 @@
         'ecl/curve25519_32.c',
       ],
     }],
+    ['supports_vale_curve25519==1', {
+      'sources': [
+        'verified/Hacl_Curve25519_64.c',
+      ],
+    }],
     ['(target_arch!="ppc64" and target_arch!="ppc64le") or disable_altivec==1', {
       'sources': [
         # Gyp does not support per-file cflags, so working around like this.
diff --git a/lib/freebl/verified/config.h b/lib/freebl/verified/config.h
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/lib/freebl/verified/config.h
diff --git a/lib/freebl/verified/internal/Vale.h b/lib/freebl/verified/internal/Vale.h
new file mode 100644
index 000000000..400650e95
--- /dev/null
+++ b/lib/freebl/verified/internal/Vale.h
@@ -0,0 +1,184 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
+ *
+ * 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.
+ */
+
+#ifndef __internal_Vale_H
+#define __internal_Vale_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+extern uint64_t add_scalar_e(uint64_t *x0, uint64_t *x1, uint64_t x2);
+
+extern uint64_t fadd_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t sha256_update(uint32_t *x0, uint8_t *x1, uint64_t x2, uint32_t *x3);
+
+extern uint64_t x64_poly1305(uint8_t *x0, uint8_t *x1, uint64_t x2, uint64_t x3);
+
+extern uint64_t check_aesni();
+
+extern uint64_t check_sha();
+
+extern uint64_t check_adx_bmi2();
+
+extern uint64_t check_avx();
+
+extern uint64_t check_avx2();
+
+extern uint64_t check_movbe();
+
+extern uint64_t check_sse();
+
+extern uint64_t check_rdrand();
+
+extern uint64_t check_avx512();
+
+extern uint64_t check_osxsave();
+
+extern uint64_t check_avx_xcr0();
+
+extern uint64_t check_avx512_xcr0();
+
+extern uint64_t
+gcm128_decrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t
+gcm256_decrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t aes128_key_expansion(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t aes256_key_expansion(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t
+compute_iv_stdcall(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5);
+
+extern uint64_t
+gcm128_encrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t
+gcm256_encrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t aes128_keyhash_init(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t aes256_keyhash_init(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t cswap2_e(uint64_t x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t fsqr_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t fsqr2_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t fmul_e(uint64_t *x0, uint64_t *x1, uint64_t *x2, uint64_t *x3);
+
+extern uint64_t fmul2_e(uint64_t *x0, uint64_t *x1, uint64_t *x2, uint64_t *x3);
+
+extern uint64_t fmul_scalar_e(uint64_t *x0, uint64_t *x1, uint64_t x2);
+
+extern uint64_t fsub_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Vale_H_DEFINED
+#endif