Skip to content

v1.0.0-beta2

Latest
Latest

Choose a tag to compare

View all tags
@mkannwischer mkannwischer released this 23 May 08:23
· 58 commits to main since this release
v1.0.0-beta2
9b0ee84

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

Full Changelog: v1.0.0-beta...v1.0.0-beta2

Contributors

flynd, mkannwischer, and 6 other contributors
Assets 2
Loading