Prepare moving verify.c functions to backend

Currently, mlkem-native has the `verify`, `cmov`, and `cmov_int16`
functions in the verify.c function similar as the reference implementation.
By putting them in a separate compilation unit, we stop the compiler
from turning this code into variable time code.

While being portable, this has various downside:
- If LTO were to be used, this can lead to timing side-channels.
  We stop that by not using LTO for verify.c in our own build, but
  we have no control over how other people compile our code -
  this feels dangerous.
- If these functions are in a separte compilation unit, the compiler
  cannot inline them. This is very expensive particularly for `cmov_int16`.
  By writing that gadget in inline assembly, we can allow the compiler to
  inline these calls, but still guarantee that they execute in constant-time.

This commit prepares the switch to a native implementation of the
verify.c functions in a architecture-specific header file.
For now these are not implemented in inline assembly as I wanted to
gather feedback on this first.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mlkem/native/aarch64/profiles/clean.h

@@ -19,6 +19,7 @@
 #define MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED
 #define MLKEM_USE_NATIVE_POLY_TOBYTES
 #define MLKEM_USE_NATIVE_REJ_UNIFORM
+#define MLKEM_USE_NATIVE_VERIFY
 
 #define NTT_BOUND_NATIVE (6 * MLKEM_Q)
 static inline void ntt_native(poly *data)

mlkem/native/aarch64/profiles/opt.h

@@ -19,6 +19,7 @@
 #define MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED
 #define MLKEM_USE_NATIVE_POLY_TOBYTES
 #define MLKEM_USE_NATIVE_REJ_UNIFORM
+#define MLKEM_USE_NATIVE_VERIFY
 
 #define NTT_BOUND_NATIVE (6 * MLKEM_Q)
 static inline void ntt_native(poly *data)

mlkem/native/aarch64/verify-aarch64.h

@@ -0,0 +1,57 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0
+#ifndef VERIFY_AARCH64_H
+#define VERIFY_AARCH64_H
+
+#include <stddef.h>
+#include <stdint.h>
+
+static inline int verify_native(const uint8_t *a, const uint8_t *b,
+                                const size_t len)
+{
+  // TODO: replace this with inline asm
+  uint8_t r = 0;
+  uint64_t u;
+
+  // Switch to a _signed_ ilen value, so that our loop counter
+  // can also be signed, and thus (i - 1) in the loop invariant
+  // can yield -1 as required.
+  const int ilen = (int)len;
+
+  for (int i = 0; i < ilen; i++)
+  {
+    r |= a[i] ^ b[i];
+  }
+
+  u = (-(uint64_t)r) >> 63;
+  return (int)u;
+}
+
+static inline void cmov_native(uint8_t *r, const uint8_t *x, size_t len,
+                               uint8_t b)
+{
+  // TODO: replace this with inline asm
+  size_t i;
+
+  b = (-b) & 0xFF;
+  for (i = 0; i < len; i++)
+  {
+    r[i] ^= b & (r[i] ^ x[i]);
+  }
+}
+
+
+static inline void cmov_int16_native(int16_t *r, const int16_t v,
+                                     const uint16_t b)
+{
+  // TODO: replace this with inline asm
+  // b == 0 => mask = 0x0000
+  // b == 1 => mask = 0xFFFF
+  const uint16_t mask = -b;
+
+  // mask == 0x0000 => *r == (*r ^ 0x0000) == *r
+  // mask == 0xFFFF => *r == (*r ^ (*r ^ v)) == (*r ^ *r) ^ v == 0 ^ v == v
+  *r ^= mask & ((*r) ^ v);
+}
+
+#endif /* VERIFY_AARCH64_H */

mlkem/native/x86_64/profiles/default.h

@@ -27,6 +27,7 @@
 #define MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE
 #define MLKEM_USE_NATIVE_POLY_TOBYTES
 #define MLKEM_USE_NATIVE_POLY_FROMBYTES
+#define MLKEM_USE_NATIVE_VERIFY
 
 #define INVNTT_BOUND_NATIVE \
   (14870 + 1)  // Bound from the official Kyber repository

mlkem/native/x86_64/verify-x86_64.h

@@ -0,0 +1,57 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0
+#ifndef VERIFY_X86_64_H
+#define VERIFY_X86_64_H
+
+#include <stddef.h>
+#include <stdint.h>
+
+static inline int verify_native(const uint8_t *a, const uint8_t *b,
+                                const size_t len)
+{
+  // TODO: replace this with inline asm
+  uint8_t r = 0;
+  uint64_t u;
+
+  // Switch to a _signed_ ilen value, so that our loop counter
+  // can also be signed, and thus (i - 1) in the loop invariant
+  // can yield -1 as required.
+  const int ilen = (int)len;
+
+  for (int i = 0; i < ilen; i++)
+  {
+    r |= a[i] ^ b[i];
+  }
+
+  u = (-(uint64_t)r) >> 63;
+  return (int)u;
+}
+
+static inline void cmov_native(uint8_t *r, const uint8_t *x, size_t len,
+                               uint8_t b)
+{
+  // TODO: replace this with inline asm
+  size_t i;
+
+  b = (-b) & 0xFF;
+  for (i = 0; i < len; i++)
+  {
+    r[i] ^= b & (r[i] ^ x[i]);
+  }
+}
+
+
+static inline void cmov_int16_native(int16_t *r, const int16_t v,
+                                     const uint16_t b)
+{
+  // TODO: replace this with inline asm
+  // b == 0 => mask = 0x0000
+  // b == 1 => mask = 0xFFFF
+  const uint16_t mask = -b;
+
+  // mask == 0x0000 => *r == (*r ^ 0x0000) == *r
+  // mask == 0xFFFF => *r == (*r ^ (*r ^ v)) == (*r ^ *r) ^ v == 0 ^ v == v
+  *r ^= mask & ((*r) ^ v);
+}
+
+#endif /* VERIFY_X86_64_H */

mlkem/verify.c

@@ -4,6 +4,7 @@
 #include <stddef.h>
 #include <stdint.h>
 
+#if !defined(MLKEM_USE_NATIVE_VERIFY)
 //
 // WARNING:
 //
@@ -79,3 +80,11 @@ void cmov_int16(int16_t *r, const int16_t v, const uint16_t b)
   *r ^= mask & ((*r) ^ v);
 #pragma CPROVER check pop
 }
+
+
+#else /* MLKEM_USE_NATIVE_VERIFY */
+
+// Dummy constant to keep compiler happy despite empty CU
+int empty_cu_c_verify;
+
+#endif /* MLKEM_USE_NATIVE_VERIFY */

mlkem/verify.h

@@ -6,9 +6,28 @@
 #include <limits.h>
 #include <stddef.h>
 #include <stdint.h>
+#include "arith_native.h"
 #include "cbmc.h"
 #include "params.h"
 
+// If a native backend is used, we include the native implementations from the
+// backend as those are using inline assembly. This guarantees that these
+// gadgets are constant-time, but also allows the compiler to inline them.
+// Otherwise, we use the reference code (verify.c) in a separate compilation
+// unit.
+#if defined(MLKEM_USE_NATIVE_VERIFY)
+#include "cpucap.h"
+
+#if defined(SYS_AARCH64)
+#include "verify-aarch64.h"
+#endif /* SYS_AARCH64 */
+
+#if defined(SYS_X86_64)
+#include "verify-x86_64.h"
+#endif /* SYS_X86_64 */
+#endif
+
+
 #define verify MLKEM_NAMESPACE(verify)
 /*************************************************
  * Name:        verify
@@ -21,13 +40,20 @@
  *
  * Returns 0 if the byte arrays are equal, 1 otherwise
  **************************************************/
+#if !defined(MLKEM_USE_NATIVE_VERIFY)
 int verify(const uint8_t *a, const uint8_t *b, const size_t len)
 __contract__(
   requires(memory_no_alias(a, len))
   requires(memory_no_alias(b, len))
   requires(len <= INT_MAX)
   ensures(return_value == (1 - forall(int, i, 0, ((int)len - 1), (a[i] == b[i]))))
 );
+#else  /* MLKEM_USE_NATIVE_VERIFY */
+static inline int verify(const uint8_t *a, const uint8_t *b, const size_t len)
+{
+  return verify_native(a, b, len);
+}
+#endif /* MLKEM_USE_NATIVE_VERIFY */
 
 #define cmov MLKEM_NAMESPACE(cmov)
 /*************************************************
@@ -43,13 +69,20 @@ __contract__(
  *              size_t len:       Amount of bytes to be copied
  *              uint8_t b:        Condition bit; has to be in {0,1}
  **************************************************/
+#if !defined(MLKEM_USE_NATIVE_VERIFY)
 void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b)
 __contract__(
   requires(memory_no_alias(r, len))
   requires(memory_no_alias(x, len))
   requires(b == 0 || b == 1)
   assigns(memory_slice(r, len))
 );
+#else  /* MLKEM_USE_NATIVE_VERIFY */
+static inline void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b)
+{
+  cmov_native(r, x, len, b);
+}
+#endif /* MLKEM_USE_NATIVE_VERIFY */
 
 #define cmov_int16 MLKEM_NAMESPACE(cmov_int16)
 /*************************************************
@@ -63,12 +96,19 @@ __contract__(
  *              int16_t v:        input int16_t. Must not be NULL
  *              uint16_t b:       Condition bit; has to be in {0,1}
  **************************************************/
+#if !defined(MLKEM_USE_NATIVE_VERIFY)
 void cmov_int16(int16_t *r, const int16_t v, const uint16_t b)
 __contract__(
   requires(b == 0 || b == 1)
   requires(memory_no_alias(r, sizeof(int16_t)))
   assigns(memory_slice(r, sizeof(int16_t)))
   ensures(*r == (b ? v : old(*r)))
 );
+#else  /* MLKEM_USE_NATIVE_VERIFY */
+static inline void cmov_int16(int16_t *r, const int16_t v, const uint16_t b)
+{
+  cmov_int16_native(r, v, b);
+}
+#endif /* MLKEM_USE_NATIVE_VERIFY */
 
 #endif