Skip to content

Commit afe6b75

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 b701069 commit afe6b75

35 files changed

Lines changed: 23898 additions & 649 deletions

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -222,6 +222,10 @@ jobs:
222222
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
223223
- name: keccak_f1600_x4_avx2_asm
224224
needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"]
225+
- name: rej_uniform_eta2_avx2_asm
226+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_rej_uniform_table.ml", "subroutine_signatures.ml"]
227+
- name: rej_uniform_eta4_avx2_asm
228+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_rej_uniform_table.ml", "subroutine_signatures.ml"]
225229
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
226230
runs-on: ubuntu-latest
227231
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_asm.S](dev/x86_64/src/rej_uniform_avx2_asm.S)
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_asm.S](mldsa/src/native/x86_64/src/rej_uniform_avx2_asm.S)
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)
@@ -345,6 +345,8 @@ source code and documentation.
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)
347347
- [proofs/hol_light/x86_64/mldsa/rej_uniform_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_avx2_asm.S)
348+
- [proofs/hol_light/x86_64/mldsa/rej_uniform_eta2_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_eta2_avx2_asm.S)
349+
- [proofs/hol_light/x86_64/mldsa/rej_uniform_eta4_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_eta4_avx2_asm.S)
348350

349351
### `Round3_Spec`
350352

‎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: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ 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(r, buf, mld_rej_uniform_table);
110110
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
111111
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
112112
return (int)outlen;
@@ -135,7 +135,7 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
135135
* We declassify prior the input data and mark the outputs as secret.
136136
*/
137137
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
138-
outlen = mld_rej_uniform_eta4_avx2(r, buf);
138+
outlen = mld_rej_uniform_eta4_avx2_asm(r, buf, mld_rej_uniform_table);
139139
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
140140
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
141141
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
@@ -94,15 +94,37 @@ __contract__(
9494
);
9595

9696
#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
97-
#define mld_rej_uniform_eta2_avx2 MLD_NAMESPACE(mld_rej_uniform_eta2_avx2)
98-
MLD_MUST_CHECK_RETURN_VALUE
99-
unsigned mld_rej_uniform_eta2_avx2(
100-
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN]);
97+
#define mld_rej_uniform_eta2_avx2_asm MLD_NAMESPACE(rej_uniform_eta2_avx2_asm)
98+
/* This contract must be kept in sync with the HOL-Light specification
99+
* in proofs/hol_light/x86_64/proofs/rej_uniform_eta2_avx2_asm.ml */
100+
MLD_MUST_CHECK_RETURN_VALUE MLD_SYSV_ABI
101+
unsigned mld_rej_uniform_eta2_avx2_asm(
102+
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN],
103+
const uint8_t table[256][8])
104+
__contract__(
105+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
106+
requires(memory_no_alias(buf, MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN))
107+
requires(table == mld_rej_uniform_table)
108+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
109+
ensures(return_value <= MLDSA_N)
110+
ensures(array_abs_bound(r, 0, return_value, 3))
111+
);
101112

102-
#define mld_rej_uniform_eta4_avx2 MLD_NAMESPACE(mld_rej_uniform_eta4_avx2)
103-
MLD_MUST_CHECK_RETURN_VALUE
104-
unsigned mld_rej_uniform_eta4_avx2(
105-
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN]);
113+
#define mld_rej_uniform_eta4_avx2_asm MLD_NAMESPACE(rej_uniform_eta4_avx2_asm)
114+
/* This contract must be kept in sync with the HOL-Light specification
115+
* in proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml */
116+
MLD_MUST_CHECK_RETURN_VALUE MLD_SYSV_ABI
117+
unsigned mld_rej_uniform_eta4_avx2_asm(
118+
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN],
119+
const uint8_t table[256][8])
120+
__contract__(
121+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
122+
requires(memory_no_alias(buf, MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN))
123+
requires(table == mld_rej_uniform_table)
124+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
125+
ensures(return_value <= MLDSA_N)
126+
ensures(array_abs_bound(r, 0, return_value, 5))
127+
);
106128
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
107129

108130
#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)