[TEST] Valgrind constant-time tests

.github/actions/ct-test/action.yml

@@ -0,0 +1,44 @@
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: CT Test
+description: Builds the library with given flags and runs Valgrind-based constant-time tests
+
+inputs:
+  cflags:
+    description: CFLAGS to pass to compilation
+    default: ""
+  valgrind_flags:
+    description: Extra flags to pass to valgrind
+    default: ""
+
+runs:
+  using: composite
+  steps:
+      - name: System info
+        shell: ${{ env.SHELL }}
+        run: |
+          ARCH=$(uname -m)
+          echo <<-EOF
+            ## Setup
+            Architecture: $ARCH
+            - $(uname -a)
+            - $(nix --version || echo 'nix not present')
+            - $(bash --version | grep -m1 "")
+            - $(python3 --version)
+            - $(${{ inputs.cross_prefix }}${CC} --version | grep -m1 "")
+          EOF
+          cat >> $GITHUB_STEP_SUMMARY <<-EOF
+            ## Setup
+            Architecture: $ARCH
+            - $(uname -a)
+            - $(nix --version || echo 'nix not present')
+            - $(bash --version | grep -m1 "")
+            - $(python3 --version)
+            - $(${{ inputs.cross_prefix }}${CC} --version | grep -m1 "")
+          EOF
+      - shell: ${{ env.SHELL }}
+        run: |
+          make clean
+          tests func --exec-wrapper="valgrind --error-exitcode=1 ${{ inputs.valgrind_flags }}" --cflags="-DMLD_CONFIG_CT_TESTING_ENABLED -DNTESTS=5 ${{ inputs.cflags }} -flto"

.github/workflows/all.yml

@@ -43,3 +43,11 @@ jobs:
     needs: [ base, nix ]
     uses: ./.github/workflows/cbmc.yml
     secrets: inherit
+  ct-test:
+    name: Constant-time
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    needs: [ base, nix ]
+    uses: ./.github/workflows/ct-tests.yml
+    secrets: inherit

.github/workflows/ct-tests.yml

@@ -0,0 +1,90 @@
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: Constant-time tests
+permissions:
+  contents: read
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  check-ct-varlat:
+    # Using the patched Valgrind from the KyberSlash paper to detect divisions
+    # In case the patch no longer applies after an update, we may want to switch back
+    # to stock valgrind added in https://github.com/pq-code-package/mlkem-native/pull/687
+    name: CT test ${{ matrix.nix-shell }} ${{ matrix.system }}
+    strategy:
+      fail-fast: false
+      max-parallel: 10
+      matrix:
+        system: [ubuntu-latest, pqcp-arm64]
+        nix-shell:
+          - ci_valgrind-varlat_clang14
+          - ci_valgrind-varlat_clang15
+          - ci_valgrind-varlat_clang16
+          - ci_valgrind-varlat_clang17
+          - ci_valgrind-varlat_clang18
+          - ci_valgrind-varlat_clang19
+          - ci_valgrind-varlat_clang20
+          - ci_valgrind-varlat_gcc48
+          - ci_valgrind-varlat_gcc49
+          - ci_valgrind-varlat_gcc7
+          - ci_valgrind-varlat_gcc11
+          - ci_valgrind-varlat_gcc12
+          - ci_valgrind-varlat_gcc13
+          - ci_valgrind-varlat_gcc14
+    runs-on: ${{ matrix.system }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: Setup nix
+        uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: ${{ matrix.nix-shell }}
+          nix-cache: true
+      - name:  Build and run test (-Oz)
+        # -Oz got introduced in gcc12
+        if: ${{ matrix.nix-shell !=  'ci_valgrind-varlat_gcc48' && matrix.nix-shell !=  'ci_valgrind-varlat_gcc49' && matrix.nix-shell !=  'ci_valgrind-varlat_gcc7' && matrix.nix-shell !=  'ci_valgrind-varlat_gcc11'}}
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -Oz -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-Os)
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -Os -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-O3)
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -O3 -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-Ofast)
+        # -Ofast got deprecated in clang19; -O3 -ffast-math should be used instead
+        if: ${{ matrix.nix-shell != 'ci_valgrind-varlat_clang19' &&  matrix.nix-shell !=  'ci_valgrind-varlat_clang20' }}
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -Ofast -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-O3 -ffast-math)
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -O3 -ffast-math -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-O2)
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -O2 -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-O1)
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -O1 -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes
+      - name:  Build and run test (-O0)
+        uses: ./.github/actions/ct-test
+        with:
+          cflags: -O0 -DMLD_CONFIG_KEYGEN_PCT
+          valgrind_flags: --variable-latency-errors=yes

mldsa/config.h

@@ -156,6 +156,18 @@
    #endif
 */
 
+/******************************************************************************
+ * Name:        MLD_CONFIG_CT_TESTING_ENABLED
+ *
+ * Description: If set, mldsa-native annotates data as secret / public using
+ *              valgrind's annotations VALGRIND_MAKE_MEM_UNDEFINED and
+ *              VALGRIND_MAKE_MEM_DEFINED, enabling various checks for secret-
+ *              dependent control flow of variable time execution (depending
+ *              on the exact version of valgrind installed).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CT_TESTING_ENABLED */
+
 /******************************************************************************
  * Name:        MLD_CONFIG_NO_ASM
  *

mldsa/native/aarch64/meta.h

@@ -49,28 +49,48 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
+  int outlen;
   /* AArch64 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
   {
     return -1;
   }
-
-  return (int)mld_rej_uniform_eta2_asm(r, buf, buflen,
-                                       mld_rej_uniform_eta_table);
+  /* Constant time: Inputs and outputs to this function are secret.
+   * It is safe to leak which coefficients are accepted/rejected.
+   * The assembly implementation must not leak any other information about the
+   * accepted coefficients. Constant-time testing cannot cover this, and we
+   * hence have to manually verify the assembly.
+   * We declassify prior the input data and mark the outputs as secret.
+   */
+  MLD_CT_TESTING_DECLASSIFY(buf, buflen);
+  outlen =
+      (int)mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
+  MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
+  return outlen;
 }
 
 static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
+  int outlen;
   /* AArch64 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
   {
     return -1;
   }
-
-  return (int)mld_rej_uniform_eta4_asm(r, buf, buflen,
-                                       mld_rej_uniform_eta_table);
+  /* Constant time: Inputs and outputs to this function are secret.
+   * It is safe to leak which coefficients are accepted/rejected.
+   * The assembly implementation must not leak any other information about the
+   * accepted coefficients. Constant-time testing cannot cover this, and we
+   * hence have to manually verify the assembly.
+   * We declassify prior the input data and mark the outputs as secret.
+   */
+  MLD_CT_TESTING_DECLASSIFY(buf, buflen);
+  outlen =
+      (int)mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
+  MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
+  return outlen;
 }
 
 #endif /* !__ASSEMBLER__ */

mldsa/native/x86_64/meta.h

@@ -54,26 +54,48 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
+  int outlen;
   /* AVX2 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
   {
     return -1;
   }
 
-  return (int)mld_rej_uniform_eta2_avx2(r, buf);
+  /* Constant time: Inputs and outputs to this function are secret.
+   * It is safe to leak which coefficients are accepted/rejected.
+   * The assembly implementation must not leak any other information about the
+   * accepted coefficients. Constant-time testing cannot cover this, and we
+   * hence have to manually verify the assembly.
+   * We declassify prior the input data and mark the outputs as secret.
+   */
+  MLD_CT_TESTING_DECLASSIFY(buf, buflen);
+  outlen = (int)mld_rej_uniform_eta2_avx2(r, buf);
+  MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
+  return outlen;
 }
 
 static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
+  int outlen;
   /* AVX2 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
   {
     return -1;
   }
 
-  return (int)mld_rej_uniform_eta4_avx2(r, buf);
+  /* Constant time: Inputs and outputs to this function are secret.
+   * It is safe to leak which coefficients are accepted/rejected.
+   * The assembly implementation must not leak any other information about the
+   * accepted coefficients. Constant-time testing cannot cover this, and we
+   * hence have to manually verify the assembly.
+   * We declassify prior the input data and mark the outputs as secret.
+   */
+  MLD_CT_TESTING_DECLASSIFY(buf, buflen);
+  outlen = (int)mld_rej_uniform_eta4_avx2(r, buf);
+  MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
+  return outlen;
 }
 
 #endif /* !__ASSEMBLER__ */

mldsa/poly.c

@@ -494,6 +494,7 @@ __contract__(
 )
 {
   unsigned int ctr, pos;
+  int t_valid;
   uint32_t t0, t1;
 
 /* TODO: CBMC proof based on mld_rej_uniform_eta2_native */
@@ -534,23 +535,36 @@ __contract__(
     t0 = buf[pos] & 0x0F;
     t1 = buf[pos++] >> 4;
 
+    /* Constant time: The inputs and outputs to the rejection sampling are
+     * secret. However, it is fine to leak which coefficients have been
+     * rejected. For constant-time testing, we declassify the result of
+     * the comparison.
+     */
 #if MLDSA_ETA == 2
-    if (t0 < 15)
+    t_valid = t0 < 15;
+    MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
+    if (t_valid) /* t0 < 15 */
     {
       t0 = t0 - (205 * t0 >> 10) * 5;
       a[ctr++] = 2 - (int32_t)t0;
     }
-    if (t1 < 15 && ctr < target)
+    t_valid = t1 < 15;
+    MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
+    if (t_valid && ctr < target) /* t1 < 15 */
     {
       t1 = t1 - (205 * t1 >> 10) * 5;
       a[ctr++] = 2 - (int32_t)t1;
     }
 #elif MLDSA_ETA == 4
-    if (t0 < 9)
+    t_valid = t0 < 9;
+    MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
+    if (t_valid) /* t0 < 9 */
     {
       a[ctr++] = 4 - (int32_t)t0;
     }
-    if (t1 < 9 && ctr < target)
+    t_valid = t1 < 9; /* t1 < 9 */
+    MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
+    if (t_valid && ctr < target)
     {
       a[ctr++] = 4 - (int32_t)t1;
     }

mldsa/rounding.c

@@ -24,7 +24,7 @@ void mld_decompose(int32_t *a0, int32_t *a1, int32_t a)
   *a1 = (*a1 * 11275 + (1 << 23)) >> 24;
   cassert(*a1 >= 0 && *a1 <= 44);
 
-  *a1 = mld_ct_sel_int32(0, *a1, mld_ct_cmask_neg_i32(43 - *a1));
+  *a1 ^= ((43 - *a1) >> 31) & *a1;
   cassert(*a1 >= 0 && *a1 <= 43);
 #else /* MLDSA_MODE == 2 */
   *a1 = (*a1 * 1025 + (1 << 21)) >> 22;
@@ -36,8 +36,7 @@ void mld_decompose(int32_t *a0, int32_t *a1, int32_t a)
 #endif /* MLDSA_MODE != 2 */
 
   *a0 = a - *a1 * 2 * MLDSA_GAMMA2;
-  *a0 = mld_ct_sel_int32(*a0 - MLDSA_Q, *a0,
-                         mld_ct_cmask_neg_i32((MLDSA_Q - 1) / 2 - *a0));
+  *a0 -= (((MLDSA_Q - 1) / 2 - *a0) >> 31) & MLDSA_Q;
 }
 
 unsigned int mld_make_hint(int32_t a0, int32_t a1)