Skip to content

Commit 2fbc340

Browse files
hanno-beckerhanno-becker
committed
Add ABI checker for AArch64, x86_64 (SysV), Armv8.1-M+MVE
Verify that each assembly kernel preserves the callee-saved registers its platform calling convention requires: - AArch64 (AAPCS64): x19-x28, x29/FP, lower 64 bits of d8-d15. - x86_64 (System V): rbx, rbp, r12-r15. No SIMD register callee-saved. - Armv8.1-M (AAPCS32): r4-r11 plus MVE Q4-Q7 (= D8-D15). A per-arch assembly call stub loads a random register state, calls the kernel, and captures the result; a checker then confirms the callee-saved set is intact. Pointer arguments are backed by correctly-sized buffers whose layout comes from a per-kernel YAML block; scripts/autogen turns that YAML into the per-kernel checks. A self-test of hand-written corrupters confirms the checker actually fires before kernel verdicts are trusted. Run via `make run_abicheck OPT=1` or `scripts/tests abicheck`. It needs no library build, so `scripts/tests all` runs it by default. Ported from mlkem-native, with the following deviations: - No PowerPC64/ELFv2 backend, which mldsa-native does not ship. - Fresh ABI YAML for the ML-DSA kernel set and signatures. - Fixed the FIPS202 Keccak YAML Name fields to match the exported symbols (e.g. keccak_f1600_x1_scalar_aarch64_asm, not keccak_f1600_x1_scalar_asm), which the generator maps to mld_<Name>. - The build force-undefines MLD_CONFIG_NO_{KEYPAIR,SIGN,VERIFY}_API so every kernel is present; many ML-DSA kernels are otherwise gated out by reduced-API configs, unlike any mlkem kernel. - Adds MLD_SYS_CAP_MVE to sys.h (mlkem already has MLK_SYS_CAP_MVE), as the Armv8.1-M check needs it for its runtime capability gate. AArch64 ABI YAML lives in dev/aarch64_clean/src/, not dev/aarch64_opt/src/, which scripts/autogen regenerates from clean. See test/abicheck/README.md for details. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 22a70aa commit 2fbc340

189 files changed

Lines changed: 7888 additions & 31 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/mlc_config.json‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,10 @@
2121
},
2222
{
2323
"pattern": "^https://eprint\\.iacr\\.org"
24+
},
25+
{
26+
"_comment": "Armv8-M Architecture Reference Manual; the Arm developer site rate-limits / 403s automated link-checks.",
27+
"pattern": "^https://developer\\.arm\\.com"
2428
}
2529
]
2630
}

‎BIBLIOGRAPHY.md‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,26 @@
77
This file lists the citations made throughout the mldsa-native
88
source code and documentation.
99

10+
### `AAPCS32`
11+
12+
* Procedure Call Standard for the Arm Architecture (AAPCS32)
13+
* Author(s):
14+
- Arm Limited
15+
* URL: https://github.com/ARM-software/abi-aa/blob/main/aapcs32/aapcs32.rst
16+
* Referenced from:
17+
- [test/abicheck/README.md](test/abicheck/README.md)
18+
- [test/abicheck/armv81m/abicheck_armv81m.c](test/abicheck/armv81m/abicheck_armv81m.c)
19+
20+
### `AAPCS64`
21+
22+
* Procedure Call Standard for the Arm 64-bit Architecture (AAPCS64)
23+
* Author(s):
24+
- Arm Limited
25+
* URL: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst
26+
* Referenced from:
27+
- [test/abicheck/README.md](test/abicheck/README.md)
28+
- [test/abicheck/aarch64/abicheck_aarch64.c](test/abicheck/aarch64/abicheck_aarch64.c)
29+
1030
### `ACVP`
1131

1232
* Automated Cryptographic Validation Protocol (ACVP) Server
@@ -16,6 +36,16 @@ source code and documentation.
1636
* Referenced from:
1737
- [README.md](README.md)
1838

39+
### `ArmARMv8M`
40+
41+
* Armv8-M Architecture Reference Manual (DDI 0553)
42+
* Author(s):
43+
- Arm Limited
44+
* URL: https://developer.arm.com/documentation/ddi0553/latest/
45+
* Referenced from:
46+
- [test/abicheck/README.md](test/abicheck/README.md)
47+
- [test/abicheck/armv81m/abicheck_armv81m.c](test/abicheck/armv81m/abicheck_armv81m.c)
48+
1949
### `AutoCorrode`
2050

2151
* AutoCorrode software verification framework for Isabelle/HOL
@@ -347,6 +377,19 @@ source code and documentation.
347377
- [proofs/hol_light/aarch64/mldsa/intt_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/intt_aarch64_asm.S)
348378
- [proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S)
349379

380+
### `SysVAMD64`
381+
382+
* System V Application Binary Interface — AMD64 Architecture Processor Supplement
383+
* Author(s):
384+
- Michael Matz
385+
- Jan Hubička
386+
- Andreas Jaeger
387+
- Mark Mitchell
388+
* URL: https://gitlab.com/x86-psABIs/x86-64-ABI
389+
* Referenced from:
390+
- [test/abicheck/README.md](test/abicheck/README.md)
391+
- [test/abicheck/x86_64/abicheck_x86_64.c](test/abicheck/x86_64/abicheck_x86_64.c)
392+
350393
### `libmceliece`
351394

352395
* libmceliece implementation of Classic McEliece

‎BIBLIOGRAPHY.yml‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,3 +204,31 @@
204204
name: Project Wycheproof
205205
author: Community Cryptography Specification Project
206206
url: https://github.com/C2SP/wycheproof
207+
208+
- id: AAPCS64
209+
short: AAPCS64
210+
name: "Procedure Call Standard for the Arm 64-bit Architecture (AAPCS64)"
211+
author: Arm Limited
212+
url: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst
213+
214+
- id: AAPCS32
215+
short: AAPCS32
216+
name: "Procedure Call Standard for the Arm Architecture (AAPCS32)"
217+
author: Arm Limited
218+
url: https://github.com/ARM-software/abi-aa/blob/main/aapcs32/aapcs32.rst
219+
220+
- id: SysVAMD64
221+
short: System V AMD64 psABI
222+
name: "System V Application Binary Interface — AMD64 Architecture Processor Supplement"
223+
author:
224+
- Matz, Michael
225+
- Hubička, Jan
226+
- Jaeger, Andreas
227+
- Mitchell, Mark
228+
url: https://gitlab.com/x86-psABIs/x86-64-ABI
229+
230+
- id: ArmARMv8M
231+
short: Armv8-M ARM
232+
name: "Armv8-M Architecture Reference Manual (DDI 0553)"
233+
author: Arm Limited
234+
url: https://developer.arm.com/documentation/ddi0553/latest/

‎Makefile‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
clean quickcheck check-defined-CYCLES \
1919
size_44 size_65 size_87 size \
2020
run_size_44 run_size_65 run_size_87 run_size \
21-
host_info
21+
host_info abicheck run_abicheck
2222

2323
SHELL := /usr/bin/env bash
2424
.DEFAULT_GOAL := build
@@ -47,7 +47,7 @@ quickcheck: test
4747
build: func kat acvp wycheproof
4848
$(Q)echo " Everything builds fine!"
4949

50-
test: run_kat run_func run_acvp run_wycheproof run_unit run_alloc run_rng_fail
50+
test: run_kat run_func run_acvp run_wycheproof run_unit run_alloc run_rng_fail run_abicheck
5151
$(Q)echo " Everything checks fine!"
5252

5353
run_kat_44: kat_44
@@ -247,6 +247,22 @@ run_size: \
247247
run_size_65 \
248248
run_size_87
249249

250+
# ABI checker: verifies each assembly kernel preserves the callee-saved
251+
# registers its platform calling convention requires. Needs OPT=1 (the native
252+
# .S kernels are only assembled then), and on x86_64 also relies on
253+
# MLD_SYSV_ABI_SUPPORTED because the call stub is hand-written SysV asm.
254+
# Unsupported targets get an empty registry and exit success, so this builds
255+
# and runs cleanly on every arch (e.g. riscv64) with no explicit allowlist.
256+
ifeq ($(OPT),1)
257+
abicheck: $(ABICHECK_DIR)/bin/abicheck
258+
259+
run_abicheck: abicheck
260+
$(W) $(ABICHECK_DIR)/bin/abicheck
261+
else
262+
abicheck:
263+
run_abicheck:
264+
endif
265+
250266
# Display host and compiler feature detection information
251267
# Shows which architectural features are supported by both the compiler and host CPU
252268
# Usage: make host_info [AUTO=0|1] [CROSS_PREFIX=...]

‎dev/aarch64_clean/src/intt_aarch64_asm.S‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,33 @@
2727

2828
/* AArch64 ML-DSA inverse NTT following @[NeonNTT], @[SLOTHY_Paper], and @[NeonNTT_Autoformalised] */
2929

30+
/*yaml
31+
Name: intt_aarch64_asm
32+
Description: AArch64 ML-DSA inverse NTT
33+
Signature: void mld_intt_aarch64_asm(int32_t *r, const int32_t *zetas_l78, const int32_t *zetas_l123456)
34+
ABI:
35+
Architecture: aarch64
36+
CallingConvention: AAPCS64
37+
x0:
38+
type: buffer
39+
size_bytes: 1024
40+
permissions: read/write
41+
c_parameter: int32_t *r
42+
description: Input/output polynomial (256 x int32_t)
43+
x1:
44+
type: buffer
45+
size_bytes: 1536
46+
permissions: read-only
47+
c_parameter: const int32_t *zetas_l78
48+
description: Twiddle factors for layers 7-8 (384 x int32_t)
49+
x2:
50+
type: buffer
51+
size_bytes: 640
52+
permissions: read-only
53+
c_parameter: const int32_t *zetas_l123456
54+
description: Twiddle factors for layers 1-6 (160 x int32_t)
55+
*/
56+
3057
#include "../../../common.h"
3158
#if defined(MLD_ARITH_BACKEND_AARCH64) && \
3259
!defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)

‎dev/aarch64_clean/src/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.S‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,33 @@
22
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
33
*/
44

5+
/*yaml
6+
Name: polyvecl_pointwise_acc_montgomery_l4_aarch64_asm
7+
Description: AArch64 pointwise multiply-accumulate of length-4 polynomial vectors
8+
Signature: void mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm(int32_t *r, const int32_t a[4][256], const int32_t b[4][256])
9+
ABI:
10+
Architecture: aarch64
11+
CallingConvention: AAPCS64
12+
x0:
13+
type: buffer
14+
size_bytes: 1024
15+
permissions: write-only
16+
c_parameter: int32_t *r
17+
description: Output polynomial (256 x int32_t)
18+
x1:
19+
type: buffer
20+
size_bytes: 4096
21+
permissions: read-only
22+
c_parameter: const int32_t a[4][256]
23+
description: Input polynomial vector a (4 x 256 x int32_t)
24+
x2:
25+
type: buffer
26+
size_bytes: 4096
27+
permissions: read-only
28+
c_parameter: const int32_t b[4][256]
29+
description: Input polynomial vector b (4 x 256 x int32_t)
30+
*/
31+
532
#include "../../../common.h"
633
#if defined(MLD_ARITH_BACKEND_AARCH64) && !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) && \
734
(defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLDSA_L == 4)

‎dev/aarch64_clean/src/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,33 @@
22
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
33
*/
44

5+
/*yaml
6+
Name: polyvecl_pointwise_acc_montgomery_l5_aarch64_asm
7+
Description: AArch64 pointwise multiply-accumulate of length-5 polynomial vectors
8+
Signature: void mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm(int32_t *r, const int32_t a[5][256], const int32_t b[5][256])
9+
ABI:
10+
Architecture: aarch64
11+
CallingConvention: AAPCS64
12+
x0:
13+
type: buffer
14+
size_bytes: 1024
15+
permissions: write-only
16+
c_parameter: int32_t *r
17+
description: Output polynomial (256 x int32_t)
18+
x1:
19+
type: buffer
20+
size_bytes: 5120
21+
permissions: read-only
22+
c_parameter: const int32_t a[5][256]
23+
description: Input polynomial vector a (5 x 256 x int32_t)
24+
x2:
25+
type: buffer
26+
size_bytes: 5120
27+
permissions: read-only
28+
c_parameter: const int32_t b[5][256]
29+
description: Input polynomial vector b (5 x 256 x int32_t)
30+
*/
31+
532
#include "../../../common.h"
633
#if defined(MLD_ARITH_BACKEND_AARCH64) && !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) && \
734
(defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLDSA_L == 5)

‎dev/aarch64_clean/src/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,33 @@
22
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
33
*/
44

5+
/*yaml
6+
Name: polyvecl_pointwise_acc_montgomery_l7_aarch64_asm
7+
Description: AArch64 pointwise multiply-accumulate of length-7 polynomial vectors
8+
Signature: void mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm(int32_t *r, const int32_t a[7][256], const int32_t b[7][256])
9+
ABI:
10+
Architecture: aarch64
11+
CallingConvention: AAPCS64
12+
x0:
13+
type: buffer
14+
size_bytes: 1024
15+
permissions: write-only
16+
c_parameter: int32_t *r
17+
description: Output polynomial (256 x int32_t)
18+
x1:
19+
type: buffer
20+
size_bytes: 7168
21+
permissions: read-only
22+
c_parameter: const int32_t a[7][256]
23+
description: Input polynomial vector a (7 x 256 x int32_t)
24+
x2:
25+
type: buffer
26+
size_bytes: 7168
27+
permissions: read-only
28+
c_parameter: const int32_t b[7][256]
29+
description: Input polynomial vector b (7 x 256 x int32_t)
30+
*/
31+
532
#include "../../../common.h"
633
#if defined(MLD_ARITH_BACKEND_AARCH64) && !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) && \
734
(defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLDSA_L == 7)

‎dev/aarch64_clean/src/ntt_aarch64_asm.S‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,33 @@
2727

2828
/* AArch64 ML-DSA forward NTT following @[NeonNTT], @[SLOTHY_Paper], and @[NeonNTT_Autoformalised] */
2929

30+
/*yaml
31+
Name: ntt_aarch64_asm
32+
Description: AArch64 ML-DSA forward NTT
33+
Signature: void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456, const int32_t *zetas_l78)
34+
ABI:
35+
Architecture: aarch64
36+
CallingConvention: AAPCS64
37+
x0:
38+
type: buffer
39+
size_bytes: 1024
40+
permissions: read/write
41+
c_parameter: int32_t *r
42+
description: Input/output polynomial (256 x int32_t)
43+
x1:
44+
type: buffer
45+
size_bytes: 576
46+
permissions: read-only
47+
c_parameter: const int32_t *zetas_l123456
48+
description: Twiddle factors for layers 1-6 (144 x int32_t)
49+
x2:
50+
type: buffer
51+
size_bytes: 1536
52+
permissions: read-only
53+
c_parameter: const int32_t *zetas_l78
54+
description: Twiddle factors for layers 7-8 (384 x int32_t)
55+
*/
56+
3057
#include "../../../common.h"
3158
#if defined(MLD_ARITH_BACKEND_AARCH64) && \
3259
!defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)

‎dev/aarch64_clean/src/pointwise_montgomery_aarch64_asm.S‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,27 @@
22
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
33
*/
44

5+
/*yaml
6+
Name: poly_pointwise_montgomery_aarch64_asm
7+
Description: AArch64 pointwise Montgomery multiplication of two polynomials
8+
Signature: void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b)
9+
ABI:
10+
Architecture: aarch64
11+
CallingConvention: AAPCS64
12+
x0:
13+
type: buffer
14+
size_bytes: 1024
15+
permissions: read/write
16+
c_parameter: int32_t *a
17+
description: Input/output polynomial (256 x int32_t)
18+
x1:
19+
type: buffer
20+
size_bytes: 1024
21+
permissions: read-only
22+
c_parameter: const int32_t *b
23+
description: Input polynomial (256 x int32_t)
24+
*/
25+
526
#include "../../../common.h"
627
#if defined(MLD_ARITH_BACKEND_AARCH64) && \
728
(!defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \

0 commit comments

Comments
 (0)