Skip to content

Commit 34a0032

Browse files
jakemasjakemas
committed
x86_64 + HOL-Light: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly and HOL-Light proofs
Replaces the rej_uniform_eta2 and rej_uniform_eta4 AVX2 intrinsics with hand-written assembly, and adds HOL-Light functional-correctness and memory-safety proofs for both x86_64 routines. Both routines are variable-time, so — as for the AArch64 eta proofs — only functional correctness and memory safety are proven, not constant time. The table is passed as a parameter and all constants are built from immediates (no .rodata), following the rej_uniform approach in #1014. The proofs use the VPBROADCASTW instruction, so the s2n-bignum nix pin is temporarily moved to the fork branch of awslabs/s2n-bignum#421 until it lands on main. Signed-off-by: jake massimo <jakemas@amazon.com>
1 parent 00c5297 commit 34a0032

34 files changed

Lines changed: 26377 additions & 660 deletions

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,6 +220,10 @@ jobs:
220220
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
221221
- name: keccak_f1600_x4_avx2_asm
222222
needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"]
223+
- name: rej_uniform_eta2_avx2_asm
224+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_rej_uniform_table.ml", "subroutine_signatures.ml"]
225+
- name: rej_uniform_eta4_avx2_asm
226+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_rej_uniform_table.ml", "subroutine_signatures.ml"]
223227
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
224228
runs-on: ubuntu-latest
225229
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎BIBLIOGRAPHY.md‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -309,8 +309,8 @@ source code and documentation.
309309
- [dev/x86_64/src/polyz_unpack_17_avx2_asm.S](dev/x86_64/src/polyz_unpack_17_avx2_asm.S)
310310
- [dev/x86_64/src/polyz_unpack_19_avx2_asm.S](dev/x86_64/src/polyz_unpack_19_avx2_asm.S)
311311
- [dev/x86_64/src/rej_uniform_avx2.c](dev/x86_64/src/rej_uniform_avx2.c)
312-
- [dev/x86_64/src/rej_uniform_eta2_avx2.c](dev/x86_64/src/rej_uniform_eta2_avx2.c)
313-
- [dev/x86_64/src/rej_uniform_eta4_avx2.c](dev/x86_64/src/rej_uniform_eta4_avx2.c)
312+
- [dev/x86_64/src/rej_uniform_eta2_avx2_asm.S](dev/x86_64/src/rej_uniform_eta2_avx2_asm.S)
313+
- [dev/x86_64/src/rej_uniform_eta4_avx2_asm.S](dev/x86_64/src/rej_uniform_eta4_avx2_asm.S)
314314
- [mldsa/src/native/x86_64/src/intt_avx2_asm.S](mldsa/src/native/x86_64/src/intt_avx2_asm.S)
315315
- [mldsa/src/native/x86_64/src/ntt_avx2_asm.S](mldsa/src/native/x86_64/src/ntt_avx2_asm.S)
316316
- [mldsa/src/native/x86_64/src/nttunpack_avx2_asm.S](mldsa/src/native/x86_64/src/nttunpack_avx2_asm.S)
@@ -327,8 +327,8 @@ source code and documentation.
327327
- [mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S)
328328
- [mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S)
329329
- [mldsa/src/native/x86_64/src/rej_uniform_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_avx2.c)
330-
- [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c)
331-
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
330+
- [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2_asm.S](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2_asm.S)
331+
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2_asm.S](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2_asm.S)
332332
- [proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S)
333333
- [proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S)
334334
- [proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S](proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S)
@@ -344,6 +344,8 @@ source code and documentation.
344344
- [proofs/hol_light/x86_64/mldsa/poly_use_hint_88_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_use_hint_88_avx2_asm.S)
345345
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S)
346346
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S)
347+
- [proofs/hol_light/x86_64/mldsa/rej_uniform_eta2_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_eta2_avx2_asm.S)
348+
- [proofs/hol_light/x86_64/mldsa/rej_uniform_eta4_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_eta4_avx2_asm.S)
347349

348350
### `Round3_Spec`
349351

‎SOUNDNESS.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,19 @@ but they are not formally proved.
4545
We aim to close this gap and achieve full HOL Light coverage of the x86_64 backend
4646
prior to the first stable release of mldsa-native.
4747

48+
### Unproven secret-independent timing of rejection sampling for the secret vector
49+
50+
The `rej_uniform_eta{2,4}` kernels (AArch64 and x86_64) sample the secret vector and are
51+
proven functionally correct and memory-safe, but their secret-independent timing is not yet
52+
formally proved (see [#1160](https://github.com/pq-code-package/mldsa-native/issues/1160)).
53+
Their memory access pattern depends on which coefficients fall inside vs. outside the
54+
acceptance interval, but no other information about the secret coefficients is leaked, and the
55+
indices of in-bound vs. out-of-bound coefficients are statistically independent of the secret
56+
key; see Section 5.5 of @[Round3_Spec]. This property is validated empirically through the
57+
`valgrind`-based constant-time tests, but not formally proved. See also the
58+
[known gap](proofs/hol_light/README.md#known-gap-rejection-sampling-for-the-secret-vector-rej_uniform_eta24)
59+
in the HOL Light README.
60+
4861
<!--- bibliography --->
4962
[^mlkem_native_soundness]: pq-code-package: mlkem-native SOUNDNESS document, [https://github.com/pq-code-package/mlkem-native/blob/main/SOUNDNESS.md](https://github.com/pq-code-package/mlkem-native/blob/main/SOUNDNESS.md)
5063
[^s2n_bignum_soundness]: Amazon Web Services: s2n-bignum soundness documentation, [https://github.com/awslabs/s2n-bignum/blob/main/doc/s2n_bignum_soundness.md](https://github.com/awslabs/s2n-bignum/blob/main/doc/s2n_bignum_soundness.md)

‎dev/x86_64/meta.h‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,8 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
106106
* We declassify prior the input data and mark the outputs as secret.
107107
*/
108108
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
109-
outlen = mld_rej_uniform_eta2_avx2(r, buf);
109+
outlen = mld_rej_uniform_eta2_avx2_asm(
110+
r, buf, (const uint8_t *)mld_rej_uniform_table);
110111
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
111112
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
112113
return (int)outlen;
@@ -135,7 +136,8 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
135136
* We declassify prior the input data and mark the outputs as secret.
136137
*/
137138
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
138-
outlen = mld_rej_uniform_eta4_avx2(r, buf);
139+
outlen = mld_rej_uniform_eta4_avx2_asm(
140+
r, buf, (const uint8_t *)mld_rej_uniform_table);
139141
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
140142
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
141143
return (int)outlen;

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 30 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -83,15 +83,37 @@ unsigned mld_rej_uniform_avx2(int32_t *r,
8383
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);
8484

8585
#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
86-
#define mld_rej_uniform_eta2_avx2 MLD_NAMESPACE(mld_rej_uniform_eta2_avx2)
87-
MLD_MUST_CHECK_RETURN_VALUE
88-
unsigned mld_rej_uniform_eta2_avx2(
89-
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN]);
86+
#define mld_rej_uniform_eta2_avx2_asm MLD_NAMESPACE(rej_uniform_eta2_avx2_asm)
87+
/* This contract must be kept in sync with the HOL-Light specification
88+
* in proofs/hol_light/x86_64/proofs/rej_uniform_eta2_avx2_asm.ml */
89+
MLD_MUST_CHECK_RETURN_VALUE MLD_SYSV_ABI
90+
unsigned mld_rej_uniform_eta2_avx2_asm(
91+
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN],
92+
const uint8_t *table)
93+
__contract__(
94+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
95+
requires(memory_no_alias(buf, MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN))
96+
requires(table == mld_rej_uniform_table)
97+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
98+
ensures(return_value <= MLDSA_N)
99+
ensures(array_bound(r, 0, return_value, -2, 2))
100+
);
90101

91-
#define mld_rej_uniform_eta4_avx2 MLD_NAMESPACE(mld_rej_uniform_eta4_avx2)
92-
MLD_MUST_CHECK_RETURN_VALUE
93-
unsigned mld_rej_uniform_eta4_avx2(
94-
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN]);
102+
#define mld_rej_uniform_eta4_avx2_asm MLD_NAMESPACE(rej_uniform_eta4_avx2_asm)
103+
/* This contract must be kept in sync with the HOL-Light specification
104+
* in proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml */
105+
MLD_MUST_CHECK_RETURN_VALUE MLD_SYSV_ABI
106+
unsigned mld_rej_uniform_eta4_avx2_asm(
107+
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN],
108+
const uint8_t *table)
109+
__contract__(
110+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
111+
requires(memory_no_alias(buf, MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN))
112+
requires(table == mld_rej_uniform_table)
113+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
114+
ensures(return_value <= MLDSA_N)
115+
ensures(array_bound(r, 0, return_value, -4, 4))
116+
);
95117
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
96118

97119
#if !defined(MLD_CONFIG_NO_SIGN_API)

‎dev/x86_64/src/rej_uniform_eta2_avx2.c‎

Lines changed: 0 additions & 157 deletions
This file was deleted.

0 commit comments

Comments
 (0)