Skip to content

Commit fe3aafc

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #391 from pq-code-package/valgrind-ct
Add valgrind-based constant-time tests
2 parents 7797682 + f0e67f0 commit fe3aafc

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)