Skip to content

Commit 237e387

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, plus the CBMC proof for the native wrapper. 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 31300ad commit 237e387

36 files changed

Lines changed: 26473 additions & 650 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: 14 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -28,22 +28,20 @@ same TCB, and therefore the same shared mitigations and residual risks.
2828

2929
## Additional risks specific to mldsa-native
3030

31-
### Incomplete HOL Light proof coverage
32-
33-
The AArch64 backend is fully covered, but the x86_64 backend is not yet complete.
34-
The full list of functions that are covered today is
35-
maintained in [proofs/hol_light/README.md](proofs/hol_light/README.md).
36-
37-
The remaining HOL Light proof work for the x86_64 backend is tracked in
38-
[#912](https://github.com/pq-code-package/mldsa-native/issues/912).
39-
40-
For the routines without HOL Light specifications, functional correctness, memory safety,
41-
and constant-time properties are validated empirically through the full test suite (functional
42-
tests, KAT, ACVP, unit tests, and `valgrind`-based constant-time tests on AArch64 and x86_64),
43-
but they are not formally proved.
44-
45-
We aim to close this gap and achieve full HOL Light coverage of the x86_64 backend
46-
prior to the first stable release of mldsa-native.
31+
### Rejection sampling for the secret vector (`rej_uniform_eta{2,4}`)
32+
33+
Both the AArch64 and x86_64 backends are fully covered by HOL Light proofs; the full list of
34+
functions is maintained in [proofs/hol_light/README.md](proofs/hol_light/README.md).
35+
36+
The one exception to the three target properties is the rejection-sampling kernels for the
37+
secret vector, `rej_uniform_eta{2,4}`, on both backends: these are proven functionally correct
38+
and memory-safe, but their secret-independent timing is not yet formally proved (see
39+
[#1160](https://github.com/pq-code-package/mldsa-native/issues/1160)). Their memory access
40+
pattern depends on which coefficients fall inside vs. outside the acceptance interval, but no
41+
other information about the secret coefficients is leaked, and the indices of in-bound vs.
42+
out-of-bound coefficients are statistically independent of the secret key; see Section 5.5 of
43+
@[Round3_Spec]. This property is validated empirically through the `valgrind`-based
44+
constant-time tests, but not formally proved.
4745

4846
<!--- bibliography --->
4947
[^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)

‎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)