v1.0.0-beta2

mldsa-native v1.0.0-beta2

We are pleased to announce the v1.0.0-beta2 release of mldsa-native, the second beta release.

As in the previous release, the C backend of mldsa-native is production-ready: it is formally verified with CBMC for memory safety, type safety, and the absence of (certain types of) undefined behavior. On the AArch64 and x86_64 backends, a growing set of assembly routines carries HOL Light proofs of functional correctness, memory safety, and secret-independent execution. The "beta" designation does not reflect project maturity: it will be dropped once HOL-Light proof coverage of the AArch64 and x86_64 backends is complete. See SOUNDNESS.md for the full verification scope, and the AArch64 and x86_64 coverage trackers for the remaining work.

Memory optimizations

The MLD_CONFIG_REDUCE_RAM build mode introduced as experimental in v1.0.0-beta is no longer experimental: it is now fully covered by CBMC, and substantial further reductions have landed on top of it. The MLD_TOTAL_ALLOC_{44,65,87}_{KEYPAIR,SIGN,VERIFY} constants exposed in mldsa_native.h report the maximum cumulative MLD_ALLOC size for each parameter set and operation (note that on top of that a small amount of stack memory is needed); the figures for v1.0.0-beta2 are:

Parameter set	Operation	Default (bytes)	MLD_CONFIG_REDUCE_RAM (bytes)
ML-DSA-44	keypair	26,912	11,584
ML-DSA-44	sign	44,704	13,120
ML-DSA-44	verify	24,448	9,120
ML-DSA-65	keypair	44,320	14,656
ML-DSA-65	sign	69,312	17,248
ML-DSA-65	verify	39,872	10,208
ML-DSA-87	keypair	75,040	18,752
ML-DSA-87	sign	108,224	21,344
ML-DSA-87	verify	68,800	12,512

New configuration options

• MLD_CONFIG_NO_KEYPAIR_API - excludes crypto_sign_keypair, crypto_sign_keypair_internal, crypto_sign_pk_from_sk, and all internal APIs only needed by keypair generation.
• MLD_CONFIG_NO_SIGN_API - excludes crypto_sign, crypto_sign_signature{,_extmu,_internal,_pre_hash_internal,_pre_hash_shake256} and the internal APIs only they need.
• MLD_CONFIG_NO_VERIFY_API - excludes crypto_sign_open, crypto_sign_verify{,_extmu,_internal,_pre_hash_internal,_pre_hash_shake256} and the internal APIs only they need.
• MLD_CONFIG_MAX_SIGNING_ATTEMPTS - upper bound on the rejection-sampling iterations performed by signing (FIPS 204 Algorithm 7). When exhausted, signing returns the new MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED error code.

SOUNDNESS.md

This release introduces SOUNDNESS.md (#1112), a written account of the scope, assumptions, trusted computing base, and residual risks of mldsa-native's formal-verification effort. It covers the shared methodology with mlkem-native (CBMC for the C code and HOL Light + s2n-bignum for the AArch64 and x86_64 assembly), points at the underlying mlkem-native and s2n-bignum soundness documents for the shared analysis, and enumerates the gaps specific to mldsa-native, in particular the assembly routines that do not yet have HOL Light specifications. It is intended as a living document; feedback is welcome via GitHub issues or, for potential vulnerabilities, private vulnerability reporting.

Other noteworthy changes

• Wycheproof test vectors are now exercised against ML-DSA in CI (#1063).
• The AArch64 backend is now CI-tested on a baremetal AArch64 target where any unaligned data access raises an Alignment fault (#1094). The same trap would fire under an OS that sets SCTLR_ELn.A, but in typical configurations that bit is cleared and unaligned accesses to Normal memory silently succeed. Several assembly routines that had relied on unaligned memory accesses were updated to use alignment-safe accesses.
• CI gains RISC-V runners provided by the RISE project (#1034).

What's Changed

• CI: lint: output errors by @L-series in #1004
• Refactor keccak_squeezeblocks_x4() to simplify proof by @rod-chapman in #1012
• Sign: Unpack s1, s2, and t0 on the fly in REDUCE_RAM mode by @mkannwischer in #1002
• x86_64: Eliminate caddq intrinsics by @willieyz in #905
• MAINTAINERS.md: Remove affiliations by @mkannwischer in #1017
• simpasm: Move .note.GNU-stack outside preprocessor guards by @mkannwischer in #1021
• nix: Bump cbmc-viewer from 3.11 to 3.12 by @mkannwischer in #1020
• HOL-Light/AArch64: Port proofs from mlkem-native by @willieyz in #965
• CI: Add clang22 tests and constant-time tests by @mkannwischer in #1024
• Add HOL Light pointwise multiplication proofs for AArch64 and x86_64 by @jakemas in #1006
• lowram: Compute h incrementally in signing by @mkannwischer in #1015
• aarch64/src/polyz_unpack_table.c: Disable unused tables by @flynd in #1029
• Add HOL Light pointwise-acc multiplication proofs for AArch64 and x86_64 by @jakemas in #1010
• CT: Update comment on valgrind issue by @hanno-becker in #1035
• FIPS202/x86_64: Don't use native x4 backend on x86_64 when not needed by @flynd in #1032
• Add README to mldsa/ by @hanno-becker in #1036
• Fix context-length validation in ACVP test binary by @hanno-becker in #1038
• CI: Sync with mlkem-native (RISC-V runners, fork guards, examples, benchmarking) by @mkannwischer in #1034
• CBMC: Restore polyvecl_pointwise_acc_montgomery_c proof flags by @hanno-becker in #1039
• CBMC: Update to v6.9.0 by @hanno-becker in #1041
• poly_ntt_c add --slice-formula to stabilize proof by @rod-chapman in #1042
• Add configs to disable unused APIs [full CI] by @mkannwischer in #1000
• Sign: Set smlen to 0 in case of failure by @mkannwischer in #959
• CBMC: Remove MLD_UNION_OR_STRUCT by @hanno-becker in #1044
• Lowram: Share buffers with non-overlapping lifetimes in keygen by @mkannwischer in #1011
• native: Allow tables to be declared static by @flynd in #1043
• Update s2n-bignum and HOL Light pins by @jakemas in #1045
• Lint: Replace black with ruff by @mkannwischer in #1047
• Armv8.1-M: Add CFI directives for stack unwinding by @mkannwischer in #1048
• lowram: Stream matrix A element-by-element to reduce memory by @mkannwischer in #1019
• Remove --slice-formula from all Makefiles and set in Makefile.common by @rod-chapman in #1049
• check-contracts: Detect contracts separated from prototype by a comment by @mkannwischer in #1051
• Port: Format: Don't allow tabs by @mkannwischer in #1022
• CBMC: Run proofs with MLD_CONFIG_REDUCE_RAM in CI by @mkannwischer in #1050
• CI: Bump ACVP, liboqs, expo, and AWS-LC versions by @mkannwischer in #1057
• HOL-Light: Add x86 AVX2 nttunpack proof by @jakemas in #955
• nix: Pull CBMC 6.9.0 from nixos-unstable binary cache by @mkannwischer in #1062
• CI: Re-enable RISE RISC-V runner by @mkannwischer in #1061
• CBMC: Cover MLD_CONFIG_REDUCE_RAM mode by @mkannw...

v1.0.0-beta

We are pleased to announce the v1.0.0-beta release of mldsa-native. This release is not yet considered stable - there are numerous improvements we would like to make before reaching that milestone, including the completion of HOL Light correctness proofs for at least one full backend. For details on the current state of the project, refer to the README and the set of changes below. Starting with this release, we intend to make more regular releases, targeting a new release every 2-3 months. As a result, individual releases may not correspond to the completion of a well-defined set of features.

What's Changed

• sys.h: Detect little endian when compiling with MSVC by @mkannwischer in #704
• Align common.h with mlkem-native by @mkannwischer in #702
• ACVP: Update to v1.1.0.41 by @mkannwischer in #705
• Examples: Add monolithic_build_native by @mkannwischer in #709
• Examples: Add monolithic_build_multilevel_native by @mkannwischer in #711
• Hoist domain separation logic into helper function by @hanno-becker in #710
• HOL-Light: ML-DSA NTT Platform independent code by @jakemas in #695
• Replace FIPS202_NAMESPACE with MLD_NAMESPACE by @willieyz in #717
• CI: Enable examples in compiler tests by @mkannwischer in #727
• Use consistent syntax for macro definitions and invocations by @hanno-becker in #726
• Add missing zeroization to crypto_sign_verify_internal by @mkannwischer in #731
• Add Runtime dispatch based on custom CPU capabilities function by @willieyz in #607
• SLOTHY: Superoptimize AArch64 NTT by @mkannwischer in #715
• Port: porting check-namespace from mlkem-native by @willieyz in #718
• CI: Port ec2_compatibilitytests by @willieyz in #665
• CI: Align build_kat functional tests with mlkem-native by @mkannwischer in #728
• CBMC: Allow specification of per-proof timeouts by @hanno-becker in #734
• CBMC: Replace object_whole with memory_slice in non-top-level contracts by @mkannwischer in #730
• CI: Switch from pqcp-arm64 to Github Arm runners by @mkannwischer in #749
• Add crypto_sign_pk_from_sk to top-level API by @jakemas in #714
• Strengthen preconditions on polyveck_add() and polyvecl_add() by @rod-chapman in #724
• Port: Copyright linting extension by @willieyz in #744
• Switch mld_polymat to struct wrapper by @hanno-becker in #741
• SLOTHY: Superoptimize AArch64 INTT by @mkannwischer in #748
• Example: Add custom_backend by @willieyz in #699
• Examples: multilevel build by @willieyz in #746
• Examples: multilevel_build_native by @willieyz in #747
• config.h: Align mldsa-native and mlkem-native config.h by @willieyz in #745
• Port: Hoist default C backend into separate functions by @willieyz in #735
• ASM: Add marker for non-executable stack by @hanno-becker in #769
• Port: Use a single configuration file for internal and external headers by @mkannwischer in #782
• Avoid overread in polyz_unpack (AArch64 + x86_64) by @mkannwischer in #784
• CBMC: Add proofs for native backend functions by @willieyz in #768
• Inline ntt.c by @willieyz in #787
• Backend unit tests by @willieyz in #777
• Port: Speed up make by @willieyz in #788
• Namespace all macros by @willieyz in #786
• decompose: Remove separate input argument by @mkannwischer in #798
• Port: Minor autogen and CI improvements by @willieyz in #794
• CI: Fix markdown-link-check and fix various broken links by @mkannwischer in #808
• tests: Allow specification of parameter set via -kl switch by @hanno-becker in #809
• HOL-Light: Speed up NTT proof by @mkannwischer in #811
• Make allocation of large structures/buffers configurable by @hanno-becker in #801
• x86_64 Backend: Remove <immintrin.h> dependency from arith_native_x86_64.h by @willieyz in #805
• BUILDING.md: add build instructions by @L-series in #780
• refactor: align the tests scripts with mlkem-native by @willieyz in #797
• x86_64: Autogenerate the entire constant array qdata for NTT/INTT by @mkannwischer in #812
• autogen: Port check_asm_* by @willieyz in #813
• Add test for failing dynamic allocation by @hanno-becker in #810
• Remove broken symlink auto.mk and check for broken symlinks in CI by @mkannwischer in #771
• sign stack usage: Re-use y/h buffer by @mkannwischer in #818
• CBMC: Prove x86_64 NTT adheres to native API contract in api.h by @willieyz in #806
• CI: Do not use npx in lint-markdown-link by @mkannwischer in #823
• Introduce mld_polymat_get_row() helper function by @hanno-becker in #742
• Make value barrier volatile by @hanno-becker in #772
• Namespace STACK_SIZE by @willieyz in #796
• Dependencies update by @willieyz in #832
• CI: Enable gcc15 tests on MacOS by @mkannwischer in #834
• Align mld_ct_memcmp with mlkem-native by @hanno-becker in #837
• verify: Switch to constant-time memcmp by @hanno-becker in #838
• CI: Benchmark stack consumption with MLD_CONFIG_REDUCE_RAM by @mkannwischer in #836
• Replace (near-)copies of notrandombytes.[ch] by symlinks by @hanno-becker in #839
• pk_from_sk: Add validation of s1 and s2 by @mkannwischer in #841
• CBMC: Prove mld_polymat_permute_bitrev_to_custom on top of native API by @willieyz in #820
• CBMC: Increase OBJECT_BITS for polyvecl_pointwise_acc_montgomery_c by @mkannwischer in #848
• API: add failure mode support for randombytes() by @L-series in #689
• Port: Move configuration files and configs.yml into tests/configs/ by @willieyz in #843
• Port: move basic test source into test/src/ by @willieyz in #844
• Port: move acvp test source and data into test/acvp/ by @willieyz in #845
• Port: move benchmarking sources to test/bench/ by @willieyz in #846
• AArch64: Align return type of rejection sampling functions by @mkannwischer in #860
• Consolidate MLD_CONFIG_CUSTOM_ZEROIZE with mlkem-native by @willieyz in #852
• sign stack usage: compute z incrementally by @mkannwischer in #825
• CI: Move container tests to mldsa-native AWS account by @mkannwischer in #862
• mldsa_native.h: Introduce MLD_TOTAL_ALLOC constants by @mkannwischer in #850
• autogen: fix print issue with narrow terminals by @l-...

v1.0.0-alpha

mldsa-native v1.0.0-alpha

mldsa-native is a C90 library that allows developers to support the ML-DSA / FIPS 204 post-quantum cryptography standard with minimal performance and maintenance cost.

Why mldsa-native?

Minimal Dependencies: mldsa-native is written in portable C90 with minimal and configurable dependencies on the standard library.

Maintainability and Safety: Memory safety, type safety and absence of various classes of timing leakage are automatically checked on every change, using a combination of static model checking (using CBMC) and dynamic instrumentation (using valgrind). This reduces review and maintenance burden and accelerates safe code delivery.

Architecture Support: Native backends are added under a unified interface, minimizing duplicated code and reasoning. mldsa-native comes with backends for AArch64 and x86-64.

Governance: mldsa-native is supported by the Linux Foundation and Post-Quantum Cryptography Alliance.

See the README for more details.

Status

This is a production ready alpha release. External APIs are expected but not guaranteed to be stable. Feedback welcome! If you have any questions, please reach out to us or open an issue on https://github.com/pq-code-package/mldsa-native.

Development plan

• Assurance: Prove functional correctness of x86_64 and AArch64 assembly backends using HOL-Light and s2n-bignum verification infrastructure.

• Performance: Super-optimize AArch64 backend using SLOTHY; further improve performance of x86_64 backend.

• Maintainability: Improve requirements traceability by documenting relation between source and FIPS 204 standard.