Skip to content

Commit 7429b71

Browse files
jakemasjakemas
committed
HOL-Light: Add AArch64 rej_uniform_eta_{2,4} correctness, memory-safety proofs
Add functional correctness, subroutine correctness, memory-safety and subroutine-safety proofs for the AArch64 assembly implementations of rej_uniform_eta for both eta variants: - rej_uniform_eta2 (eta=2, used in ML-DSA-44) - rej_uniform_eta4 (eta=4, used in ML-DSA-65/87) Memory safety follows the mlkem_rej_uniform_VARIABLE_TIME pattern in s2n-bignum because the loop count is data-dependent (which nibbles pass the < 9 / < 15 filter). Written with the assistance of Claude Opus 4.7. Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent cbc80f6 commit 7429b71

18 files changed

Lines changed: 7462 additions & 10 deletions

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,10 @@ jobs:
103103
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
104104
- name: poly_use_hint_88_aarch64_asm
105105
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
106+
- name: rej_uniform_eta2_aarch64_asm
107+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_eta_table.ml", "subroutine_signatures.ml"]
108+
- name: rej_uniform_eta4_aarch64_asm
109+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_eta_table.ml", "subroutine_signatures.ml"]
106110
- name: keccak_f1600_x1_scalar_aarch64_asm
107111
needs: ["keccak_spec.ml", "keccak_constants.ml", "subroutine_signatures.ml"]
108112
- name: keccak_f1600_x1_v84a_aarch64_asm

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 26 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -113,15 +113,37 @@ __contract__(
113113
MLD_NAMESPACE(rej_uniform_eta2_aarch64_asm)
114114
MLD_MUST_CHECK_RETURN_VALUE
115115
uint64_t mld_rej_uniform_eta2_aarch64_asm(int32_t *r, const uint8_t *buf,
116-
unsigned buflen,
117-
const uint8_t *table);
116+
unsigned buflen, const uint8_t *table)
117+
/* This must be kept in sync with the HOL-Light specification
118+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2.ml */
119+
__contract__(
120+
requires(buflen % 8 == 0)
121+
requires(buflen >= 8)
122+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
123+
requires(memory_no_alias(buf, buflen))
124+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
125+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
126+
ensures(return_value <= MLDSA_N)
127+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
128+
);
118129

119130
#define mld_rej_uniform_eta4_aarch64_asm \
120131
MLD_NAMESPACE(rej_uniform_eta4_aarch64_asm)
121132
MLD_MUST_CHECK_RETURN_VALUE
122133
uint64_t mld_rej_uniform_eta4_aarch64_asm(int32_t *r, const uint8_t *buf,
123-
unsigned buflen,
124-
const uint8_t *table);
134+
unsigned buflen, const uint8_t *table)
135+
/* This must be kept in sync with the HOL-Light specification
136+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4.ml */
137+
__contract__(
138+
requires(buflen % 8 == 0)
139+
requires(buflen >= 8)
140+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
141+
requires(memory_no_alias(buf, buflen))
142+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
143+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
144+
ensures(return_value <= MLDSA_N)
145+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
146+
);
125147
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
126148

127149
#if !defined(MLD_CONFIG_NO_SIGN_API)

‎mldsa/src/native/aarch64/src/arith_native_aarch64.h‎

Lines changed: 26 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -113,15 +113,37 @@ __contract__(
113113
MLD_NAMESPACE(rej_uniform_eta2_aarch64_asm)
114114
MLD_MUST_CHECK_RETURN_VALUE
115115
uint64_t mld_rej_uniform_eta2_aarch64_asm(int32_t *r, const uint8_t *buf,
116-
unsigned buflen,
117-
const uint8_t *table);
116+
unsigned buflen, const uint8_t *table)
117+
/* This must be kept in sync with the HOL-Light specification
118+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2.ml */
119+
__contract__(
120+
requires(buflen % 8 == 0)
121+
requires(buflen >= 8)
122+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
123+
requires(memory_no_alias(buf, buflen))
124+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
125+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
126+
ensures(return_value <= MLDSA_N)
127+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
128+
);
118129

119130
#define mld_rej_uniform_eta4_aarch64_asm \
120131
MLD_NAMESPACE(rej_uniform_eta4_aarch64_asm)
121132
MLD_MUST_CHECK_RETURN_VALUE
122133
uint64_t mld_rej_uniform_eta4_aarch64_asm(int32_t *r, const uint8_t *buf,
123-
unsigned buflen,
124-
const uint8_t *table);
134+
unsigned buflen, const uint8_t *table)
135+
/* This must be kept in sync with the HOL-Light specification
136+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4.ml */
137+
__contract__(
138+
requires(buflen % 8 == 0)
139+
requires(buflen >= 8)
140+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
141+
requires(memory_no_alias(buf, buflen))
142+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
143+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
144+
ensures(return_value <= MLDSA_N)
145+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
146+
);
125147
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
126148

127149
#if !defined(MLD_CONFIG_NO_SIGN_API)

‎nix/s2n_bignum/default.nix‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@
44
{ stdenv, fetchFromGitHub, writeText, ... }:
55
stdenv.mkDerivation rec {
66
pname = "s2n_bignum";
7-
version = "f3c5acff6948d559194245237f6aaa7ebf7fcae8";
7+
version = "ccef24569ed5c41f4e7fcb19965bf48eff3fdaa0";
88
src = fetchFromGitHub {
99
owner = "awslabs";
1010
repo = "s2n-bignum";
1111
rev = "${version}";
12-
hash = "sha256-kfc8X2e+voefttshSUdifDc3Qn+dx0Gq5ENNLhWIdw0=";
12+
hash = "sha256-1KHAmHtBKMO+8Ea+1TTF6adKW3XKRmfcJC1vNZ/guRA=";
1313
};
1414
setupHook = writeText "setup-hook.sh" ''
1515
export S2N_BIGNUM_DIR="$1"

‎proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = rej_uniform_eta_native_aarch64_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = rej_uniform_eta_native_aarch64
12+
13+
# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
14+
# included, which contains the CBMC specifications.
15+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
23+
24+
# ML-DSA-44 and ML-DSA-87 use eta=2; ML-DSA-65 uses eta=4.
25+
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
26+
CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_native
27+
USE_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_aarch64_asm
28+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
29+
CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta4_native
30+
USE_FUNCTION_CONTRACTS=mld_rej_uniform_eta4_aarch64_asm
31+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
32+
CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_native
33+
USE_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_aarch64_asm
34+
endif
35+
USE_FUNCTION_CONTRACTS += mld_sys_check_capability
36+
APPLY_LOOP_CONTRACTS=on
37+
USE_DYNAMIC_FRAMES=1
38+
39+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
40+
EXTERNAL_SAT_SOLVER=
41+
CBMCFLAGS=--bitwuzla
42+
43+
FUNCTION_NAME = rej_uniform_eta_native_aarch64
44+
45+
# If this proof is found to consume huge amounts of RAM, you can set the
46+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
47+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
48+
# documentation in Makefile.common under the "Job Pools" heading for details.
49+
# EXPENSIVE = true
50+
51+
# This function is large enough to need...
52+
CBMC_OBJECT_BITS = 8
53+
54+
include ../Makefile.common

‎proofs/cbmc/rej_uniform_eta_native_aarch64/rej_uniform_eta_native_aarch64_harness.c‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include <stdint.h>
5+
#include "cbmc.h"
6+
#include "params.h"
7+
8+
#if MLDSA_ETA == 2
9+
int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, const uint8_t *buf,
10+
unsigned buflen);
11+
#elif MLDSA_ETA == 4
12+
int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, const uint8_t *buf,
13+
unsigned buflen);
14+
#endif
15+
16+
void harness(void)
17+
{
18+
int32_t *r;
19+
unsigned len;
20+
const uint8_t *buf;
21+
unsigned buflen;
22+
int t;
23+
24+
#if MLDSA_ETA == 2
25+
t = mld_rej_uniform_eta2_native(r, len, buf, buflen);
26+
#elif MLDSA_ETA == 4
27+
t = mld_rej_uniform_eta4_native(r, len, buf, buflen);
28+
#endif
29+
}

‎proofs/hol_light/README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -126,6 +126,8 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
126126
* AArch64 pointwise multiplication-accumulation (l=5): [mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S)
127127
* AArch64 pointwise multiplication-accumulation (l=7): [mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S)
128128
* AArch64 rejection sampling: [rej_uniform_aarch64_asm.S](aarch64/mldsa/rej_uniform_aarch64_asm.S)
129+
* AArch64 rejection sampling (eta=2): [rej_uniform_eta2_aarch64_asm.S](aarch64/mldsa/rej_uniform_eta2_aarch64_asm.S)
130+
* AArch64 rejection sampling (eta=4): [rej_uniform_eta4_aarch64_asm.S](aarch64/mldsa/rej_uniform_eta4_aarch64_asm.S)
129131
- FIPS202:
130132
* Keccak-F1600 using lazy rotations[^HYBRID]: [keccak_f1600_x1_scalar_aarch64_asm.S](aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S)
131133
* Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a_aarch64_asm.S](aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,8 @@ OBJ = mldsa/intt_aarch64_asm.o \
6363
mldsa/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.o \
6464
mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.o \
6565
mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.o \
66+
mldsa/rej_uniform_eta2_aarch64_asm.o \
67+
mldsa/rej_uniform_eta4_aarch64_asm.o \
6668
mldsa/keccak_f1600_x1_scalar_aarch64_asm.o \
6769
mldsa/keccak_f1600_x1_v84a_aarch64_asm.o \
6870
mldsa/keccak_f1600_x2_v84a_aarch64_asm.o \

‎proofs/hol_light/aarch64/mldsa/rej_uniform_eta2_aarch64_asm.S‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* Copyright (c) The mlkem-native project authors
4+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
5+
*/
6+
7+
/*
8+
* Standalone assembly for mld_rej_uniform_eta2_asm for HOL Light proofs.
9+
* This file is assembled to produce the object file that
10+
* define_assert_from_elf reads to extract the bytecodes being verified.
11+
*
12+
* Source: dev/aarch64_opt/src/rej_uniform_eta2_asm.S
13+
*/
14+
15+
#define MLDSA_N 256
16+
17+
.text
18+
.balign 4
19+
20+
// uint64_t mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf,
21+
// unsigned buflen, const uint8_t *table);
22+
.global mld_rej_uniform_eta2_asm
23+
mld_rej_uniform_eta2_asm:
24+
sub sp, sp, #0x240
25+
mov x7, #0x1
26+
movk x7, #0x2, lsl #16
27+
movk x7, #0x4, lsl #32
28+
movk x7, #0x8, lsl #48
29+
mov v31.d[0], x7
30+
mov x7, #0x10
31+
movk x7, #0x20, lsl #16
32+
movk x7, #0x40, lsl #32
33+
movk x7, #0x80, lsl #48
34+
mov v31.d[1], x7
35+
movi v30.8h, #15
36+
mov x8, sp
37+
mov x7, x8
38+
mov x11, #0
39+
eor v16.16b, v16.16b, v16.16b
40+
.Lzero:
41+
str q16, [x7], #64
42+
str q16, [x7, #-48]
43+
str q16, [x7, #-32]
44+
str q16, [x7, #-16]
45+
add x11, x11, #32
46+
cmp x11, #MLDSA_N
47+
b.lt .Lzero
48+
mov x7, x8
49+
mov x9, #0
50+
mov x4, #MLDSA_N
51+
.Lloop:
52+
cmp x9, x4
53+
b.hs .Lcopy
54+
sub x2, x2, #8
55+
ld1 {v0.8b}, [x1], #8
56+
movi v26.8b, #0x0F
57+
and v27.8b, v0.8b, v26.8b
58+
ushr v28.8b, v0.8b, #4
59+
zip1 v26.8b, v27.8b, v28.8b
60+
zip2 v29.8b, v27.8b, v28.8b
61+
ushll v16.8h, v26.8b, #0
62+
ushll v17.8h, v29.8b, #0
63+
cmhi v4.8h, v30.8h, v16.8h
64+
cmhi v5.8h, v30.8h, v17.8h
65+
and v4.16b, v4.16b, v31.16b
66+
and v5.16b, v5.16b, v31.16b
67+
uaddlv s20, v4.8h
68+
uaddlv s21, v5.8h
69+
fmov w12, s20
70+
fmov w13, s21
71+
ldr q24, [x3, x12, lsl #4]
72+
ldr q25, [x3, x13, lsl #4]
73+
cnt v4.16b, v4.16b
74+
cnt v5.16b, v5.16b
75+
uaddlv s20, v4.8h
76+
uaddlv s21, v5.8h
77+
fmov w12, s20
78+
fmov w13, s21
79+
tbl v16.16b, {v16.16b}, v24.16b
80+
tbl v17.16b, {v17.16b}, v25.16b
81+
st1 {v16.8h}, [x7]
82+
add x7, x7, x12, lsl #1
83+
st1 {v17.8h}, [x7]
84+
add x7, x7, x13, lsl #1
85+
add x12, x12, x13
86+
add x9, x9, x12
87+
cmp x2, #8
88+
b.hs .Lloop
89+
.Lcopy:
90+
cmp x9, x4
91+
csel x9, x9, x4, lo
92+
// Barrett reduction constants for mod 5
93+
movz w7, #6554
94+
dup v26.8h, w7
95+
movi v27.8h, #5
96+
movi v7.8h, #2
97+
mov x11, #0
98+
mov x7, x8
99+
.Lcopy_loop:
100+
ldr q16, [x7], #32
101+
ldr q18, [x7, #-16]
102+
// Barrett reduction: val mod 5
103+
sqdmulh v28.8h, v16.8h, v26.8h
104+
mls v16.8h, v28.8h, v27.8h
105+
sqdmulh v28.8h, v18.8h, v26.8h
106+
mls v18.8h, v28.8h, v27.8h
107+
// eta - (val mod 5) = 2 - (val mod 5)
108+
sub v16.8h, v7.8h, v16.8h
109+
sub v18.8h, v7.8h, v18.8h
110+
// Sign-extend 16->32 bit
111+
sshll2 v17.4s, v16.8h, #0
112+
sshll v16.4s, v16.4h, #0
113+
sshll2 v19.4s, v18.8h, #0
114+
sshll v18.4s, v18.4h, #0
115+
str q16, [x0], #64
116+
str q17, [x0, #-48]
117+
str q18, [x0, #-32]
118+
str q19, [x0, #-16]
119+
add x11, x11, #16
120+
cmp x11, #MLDSA_N
121+
b.lt .Lcopy_loop
122+
mov x0, x9
123+
add sp, sp, #0x240
124+
ret

0 commit comments

Comments
 (0)