Skip to content

Commit f0e67f0

Browse files
mkannwischermkannwischer
committed
Add valgrind-based constant-time tests
This commit adds extensive constant-time tests for a large set of compilers and compilation flags. It also makes use of the KyberSlash valgrind patch allowing detection of secret-dependent divisions (none were found in our code). The approach works as follows: We mark all output of randombytes as undefined and let valgrind trace through the program where values are derived from it. It will produce an error if any branches, memory accesses, or divisions depend on these undefined (secret) values. Note that ALL secret values are derived from randomness in one way or another. In places, where variable time code is detected we carefully check whether that leakage is safe or not and add appropriate declassifications (through MLD_CT_TESTING_DECLASSIFY). Comments are added explaining the rationale for the declassification. Note that compared to the mlkem-native tests, we omit the --track-origins=yes valgrind flag as it resulted in valgrind errors on AArch64 platforms for some compiler/flag combinations: vex: priv/host_arm64_defs.c:2832 (genSpill_ARM64): Assertion `offsetB < 4096' failed. Removing the flag works around this. This has no impact on the soundness of the tests - the flag merely helps tracking down were secret values originate from. Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 7797682 commit f0e67f0

File tree

9 files changed

+301
-13
lines changed

9 files changed

+301
-13
lines changed

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

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The mldsa-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: CT Test
6+
description: Builds the library with given flags and runs Valgrind-based constant-time tests
7+
8+
inputs:
9+
cflags:
10+
description: CFLAGS to pass to compilation
11+
default: ""
12+
valgrind_flags:
13+
description: Extra flags to pass to valgrind
14+
default: ""
15+
16+
runs:
17+
using: composite
18+
steps:
19+
- name: System info
20+
shell: ${{ env.SHELL }}
21+
run: |
22+
ARCH=$(uname -m)
23+
echo <<-EOF
24+
## Setup
25+
Architecture: $ARCH
26+
- $(uname -a)
27+
- $(nix --version || echo 'nix not present')
28+
- $(bash --version | grep -m1 "")
29+
- $(python3 --version)
30+
- $(${{ inputs.cross_prefix }}${CC} --version | grep -m1 "")
31+
EOF
32+
cat >> $GITHUB_STEP_SUMMARY <<-EOF
33+
## Setup
34+
Architecture: $ARCH
35+
- $(uname -a)
36+
- $(nix --version || echo 'nix not present')
37+
- $(bash --version | grep -m1 "")
38+
- $(python3 --version)
39+
- $(${{ inputs.cross_prefix }}${CC} --version | grep -m1 "")
40+
EOF
41+
- shell: ${{ env.SHELL }}
42+
run: |
43+
make clean
44+
tests func --exec-wrapper="valgrind --error-exitcode=1 ${{ inputs.valgrind_flags }}" --cflags="-DMLD_CONFIG_CT_TESTING_ENABLED -DNTESTS=5 ${{ inputs.cflags }}"

‎.github/workflows/all.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,3 +43,11 @@ jobs:
4343
needs: [ base, nix ]
4444
uses: ./.github/workflows/cbmc.yml
4545
secrets: inherit
46+
ct-test:
47+
name: Constant-time
48+
permissions:
49+
contents: 'read'
50+
id-token: 'write'
51+
needs: [ base, nix ]
52+
uses: ./.github/workflows/ct-tests.yml
53+
secrets: inherit

‎.github/workflows/ct-tests.yml‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The mldsa-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: Constant-time tests
6+
permissions:
7+
contents: read
8+
on:
9+
workflow_call:
10+
workflow_dispatch:
11+
12+
jobs:
13+
check-ct-varlat:
14+
# Using the patched Valgrind from the KyberSlash paper to detect divisions
15+
# In case the patch no longer applies after an update, we may want to switch back
16+
# to stock valgrind added in https://github.com/pq-code-package/mlkem-native/pull/687
17+
name: CT test ${{ matrix.nix-shell }} ${{ matrix.system }}
18+
strategy:
19+
fail-fast: false
20+
max-parallel: 10
21+
matrix:
22+
system: [ubuntu-latest, pqcp-arm64]
23+
nix-shell:
24+
- ci_valgrind-varlat_clang14
25+
- ci_valgrind-varlat_clang15
26+
- ci_valgrind-varlat_clang16
27+
- ci_valgrind-varlat_clang17
28+
- ci_valgrind-varlat_clang18
29+
- ci_valgrind-varlat_clang19
30+
- ci_valgrind-varlat_clang20
31+
- ci_valgrind-varlat_gcc48
32+
- ci_valgrind-varlat_gcc49
33+
- ci_valgrind-varlat_gcc7
34+
- ci_valgrind-varlat_gcc11
35+
- ci_valgrind-varlat_gcc12
36+
- ci_valgrind-varlat_gcc13
37+
- ci_valgrind-varlat_gcc14
38+
runs-on: ${{ matrix.system }}
39+
steps:
40+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
41+
- name: Setup nix
42+
uses: ./.github/actions/setup-shell
43+
with:
44+
gh_token: ${{ secrets.GITHUB_TOKEN }}
45+
nix-shell: ${{ matrix.nix-shell }}
46+
nix-cache: true
47+
- name: Build and run test (-Oz)
48+
# -Oz got introduced in gcc12
49+
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'}}
50+
uses: ./.github/actions/ct-test
51+
with:
52+
cflags: -Oz -DMLD_CONFIG_KEYGEN_PCT
53+
valgrind_flags: --variable-latency-errors=yes
54+
- name: Build and run test (-Os)
55+
uses: ./.github/actions/ct-test
56+
with:
57+
cflags: -Os -DMLD_CONFIG_KEYGEN_PCT
58+
valgrind_flags: --variable-latency-errors=yes
59+
- name: Build and run test (-O3)
60+
uses: ./.github/actions/ct-test
61+
with:
62+
cflags: -O3 -DMLD_CONFIG_KEYGEN_PCT
63+
valgrind_flags: --variable-latency-errors=yes
64+
- name: Build and run test (-Ofast)
65+
# -Ofast got deprecated in clang19; -O3 -ffast-math should be used instead
66+
if: ${{ matrix.nix-shell != 'ci_valgrind-varlat_clang19' && matrix.nix-shell != 'ci_valgrind-varlat_clang20' }}
67+
uses: ./.github/actions/ct-test
68+
with:
69+
cflags: -Ofast -DMLD_CONFIG_KEYGEN_PCT
70+
valgrind_flags: --variable-latency-errors=yes
71+
- name: Build and run test (-O3 -ffast-math)
72+
uses: ./.github/actions/ct-test
73+
with:
74+
cflags: -O3 -ffast-math -DMLD_CONFIG_KEYGEN_PCT
75+
valgrind_flags: --variable-latency-errors=yes
76+
- name: Build and run test (-O2)
77+
uses: ./.github/actions/ct-test
78+
with:
79+
cflags: -O2 -DMLD_CONFIG_KEYGEN_PCT
80+
valgrind_flags: --variable-latency-errors=yes
81+
- name: Build and run test (-O1)
82+
uses: ./.github/actions/ct-test
83+
with:
84+
cflags: -O1 -DMLD_CONFIG_KEYGEN_PCT
85+
valgrind_flags: --variable-latency-errors=yes
86+
- name: Build and run test (-O0)
87+
uses: ./.github/actions/ct-test
88+
with:
89+
cflags: -O0 -DMLD_CONFIG_KEYGEN_PCT
90+
valgrind_flags: --variable-latency-errors=yes

‎mldsa/config.h‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,18 @@
156156
#endif
157157
*/
158158

159+
/******************************************************************************
160+
* Name: MLD_CONFIG_CT_TESTING_ENABLED
161+
*
162+
* Description: If set, mldsa-native annotates data as secret / public using
163+
* valgrind's annotations VALGRIND_MAKE_MEM_UNDEFINED and
164+
* VALGRIND_MAKE_MEM_DEFINED, enabling various checks for secret-
165+
* dependent control flow of variable time execution (depending
166+
* on the exact version of valgrind installed).
167+
*
168+
*****************************************************************************/
169+
/* #define MLD_CONFIG_CT_TESTING_ENABLED */
170+
159171
/******************************************************************************
160172
* Name: MLD_CONFIG_NO_ASM
161173
*

‎mldsa/native/aarch64/meta.h‎

Lines changed: 26 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -49,28 +49,48 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
4949
const uint8_t *buf,
5050
unsigned buflen)
5151
{
52+
int outlen;
5253
/* AArch64 implementation assumes specific buffer lengths */
5354
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
5455
{
5556
return -1;
5657
}
57-
58-
return (int)mld_rej_uniform_eta2_asm(r, buf, buflen,
59-
mld_rej_uniform_eta_table);
58+
/* Constant time: Inputs and outputs to this function are secret.
59+
* It is safe to leak which coefficients are accepted/rejected.
60+
* The assembly implementation must not leak any other information about the
61+
* accepted coefficients. Constant-time testing cannot cover this, and we
62+
* hence have to manually verify the assembly.
63+
* We declassify prior the input data and mark the outputs as secret.
64+
*/
65+
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
66+
outlen =
67+
(int)mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
68+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
69+
return outlen;
6070
}
6171

6272
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
6373
const uint8_t *buf,
6474
unsigned buflen)
6575
{
76+
int outlen;
6677
/* AArch64 implementation assumes specific buffer lengths */
6778
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
6879
{
6980
return -1;
7081
}
71-
72-
return (int)mld_rej_uniform_eta4_asm(r, buf, buflen,
73-
mld_rej_uniform_eta_table);
82+
/* Constant time: Inputs and outputs to this function are secret.
83+
* It is safe to leak which coefficients are accepted/rejected.
84+
* The assembly implementation must not leak any other information about the
85+
* accepted coefficients. Constant-time testing cannot cover this, and we
86+
* hence have to manually verify the assembly.
87+
* We declassify prior the input data and mark the outputs as secret.
88+
*/
89+
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
90+
outlen =
91+
(int)mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
92+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
93+
return outlen;
7494
}
7595

7696
#endif /* !__ASSEMBLER__ */

‎mldsa/native/x86_64/meta.h‎

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,26 +54,48 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
5454
const uint8_t *buf,
5555
unsigned buflen)
5656
{
57+
int outlen;
5758
/* AVX2 implementation assumes specific buffer lengths */
5859
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
5960
{
6061
return -1;
6162
}
6263

63-
return (int)mld_rej_uniform_eta2_avx2(r, buf);
64+
/* Constant time: Inputs and outputs to this function are secret.
65+
* It is safe to leak which coefficients are accepted/rejected.
66+
* The assembly implementation must not leak any other information about the
67+
* accepted coefficients. Constant-time testing cannot cover this, and we
68+
* hence have to manually verify the assembly.
69+
* We declassify prior the input data and mark the outputs as secret.
70+
*/
71+
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
72+
outlen = (int)mld_rej_uniform_eta2_avx2(r, buf);
73+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
74+
return outlen;
6475
}
6576

6677
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
6778
const uint8_t *buf,
6879
unsigned buflen)
6980
{
81+
int outlen;
7082
/* AVX2 implementation assumes specific buffer lengths */
7183
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
7284
{
7385
return -1;
7486
}
7587

76-
return (int)mld_rej_uniform_eta4_avx2(r, buf);
88+
/* Constant time: Inputs and outputs to this function are secret.
89+
* It is safe to leak which coefficients are accepted/rejected.
90+
* The assembly implementation must not leak any other information about the
91+
* accepted coefficients. Constant-time testing cannot cover this, and we
92+
* hence have to manually verify the assembly.
93+
* We declassify prior the input data and mark the outputs as secret.
94+
*/
95+
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
96+
outlen = (int)mld_rej_uniform_eta4_avx2(r, buf);
97+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
98+
return outlen;
7799
}
78100

79101
#endif /* !__ASSEMBLER__ */

‎mldsa/poly.c‎

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -494,6 +494,7 @@ __contract__(
494494
)
495495
{
496496
unsigned int ctr, pos;
497+
int t_valid;
497498
uint32_t t0, t1;
498499

499500
/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */
@@ -534,23 +535,36 @@ __contract__(
534535
t0 = buf[pos] & 0x0F;
535536
t1 = buf[pos++] >> 4;
536537

538+
/* Constant time: The inputs and outputs to the rejection sampling are
539+
* secret. However, it is fine to leak which coefficients have been
540+
* rejected. For constant-time testing, we declassify the result of
541+
* the comparison.
542+
*/
537543
#if MLDSA_ETA == 2
538-
if (t0 < 15)
544+
t_valid = t0 < 15;
545+
MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
546+
if (t_valid) /* t0 < 15 */
539547
{
540548
t0 = t0 - (205 * t0 >> 10) * 5;
541549
a[ctr++] = 2 - (int32_t)t0;
542550
}
543-
if (t1 < 15 && ctr < target)
551+
t_valid = t1 < 15;
552+
MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
553+
if (t_valid && ctr < target) /* t1 < 15 */
544554
{
545555
t1 = t1 - (205 * t1 >> 10) * 5;
546556
a[ctr++] = 2 - (int32_t)t1;
547557
}
548558
#elif MLDSA_ETA == 4
549-
if (t0 < 9)
559+
t_valid = t0 < 9;
560+
MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
561+
if (t_valid) /* t0 < 9 */
550562
{
551563
a[ctr++] = 4 - (int32_t)t0;
552564
}
553-
if (t1 < 9 && ctr < target)
565+
t_valid = t1 < 9; /* t1 < 9 */
566+
MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int));
567+
if (t_valid && ctr < target)
554568
{
555569
a[ctr++] = 4 - (int32_t)t1;
556570
}

0 commit comments

Comments
 (0)