v1.2.0

mlkem-native v1.2.0

Release notes

mlkem-native v1.2.0 adds a new PowerPC (ppc64le) assembly backend and broadens portability of the existing backends: the x86_64 backend can now be used on Windows, the RISC-V backend compiles under C90, and a new Cortex-M33 baremetal target is tested. It also fixes a signed-shift undefined behavior on 16-bit-int targets and hardens the RISC-V backend against secret-dependent timing. Finally, the CBMC proofs are extended to establish loop termination for all functions except rejection sampling.

What's New

• PowerPC (ppc64le) backend: New VSX arithmetic backend (NTT, inverse NTT, poly_reduce, poly_tomont) for POWER8 and above, with automatic fallback to C on older targets. Thanks to IBM, and in particular Danny Tsen (@dannytsen) and Basil Hess (@bhess), for this contribution! (#1677)
• Assurance: CBMC now proves loop termination for all functions except rejection sampling. Thanks to Nicky Mouha (@nmouha) for making us aware of the absence of termination proofs. (#1625)
• Verification tooling: Bump CBMC to a development build that works around a Z3 soundness issue (Z3#9550) affecting the SMT solver used by the CBMC proofs. (#1745)
• Portability: the x86_64 assembly backend can now be used on Windows with compilers that support the SysV calling convention per function (GCC and Clang, via __attribute__((sysv_abi))) (#1730), the RISC-V backend compiles under C90 (#1732), and a new Cortex-M33 baremetal target is tested (#1579).
• Correctness / CT: Fix signed-shift undefined behavior on 16-bit-int targets (#1727) and harden the RISC-V backend against secret-dependent timing (#1732).

What's Changed

• Reactor indcpa_keypair_derand() to improve its proof time. by @rod-chapman in #1621
• CBMC: Add termination proofs for all functions except rejection sampling by @mkannwischer in #1625
• Update URL for s2n-bignum's SOUNDNESS.md file by @rod-chapman in #1631
• Rename mlk_keypair_getnoise() to mlk_keypair_getnoise_eta1() by @rod-chapman in #1629
• liboqs: Set MLK_CONFIG_EXTERNAL_API_QUALIFIER in liboqs integration configs by @mkannwischer in #1635
• simpasm: Move .note.GNU-stack outside preprocessor guards by @mkannwischer in #1637
• Refactor keccak_squeezeblock_x4() to improve proof time. by @rod-chapman in #1640
• CI: lint: output errors by @L-series in #1639
• CBMC: Introduce separate proofs for Keccak XXX_c() functions by @willieyz in #1613
• CI: Update AWS-LC integration to current HEAD by @mkannwischer in #1644
• MAINTAINERS.md: Remove affiliations and chat by @mkannwischer in #1645
• CI: Add clang22 tests and constant-time tests by @mkannwischer in #1646
• CI: Skip OpenTitan integration job on forks by @mkannwischer in #1649
• CI: Add RISC-V runners to base CI (via RISE project) by @mkannwischer in #1643
• CI: Re-enable benchmarking on Mac Mini/RPi4/A55/BPi by @mkannwischer in #1641
• CBMC: Update to v6.9.0 by @hanno-becker in #1651
• Hoist noise generation in encaps into separate helper by @hanno-becker in #1630
• Make --slice-formula default for all CBMC proofs by @rod-chapman in #1652
• Wycheproof: Fix incorrect assertion for invalid encaps/decaps tests by @mkannwischer in #1636
• Armv8.1-M: Add CFI directives for stack unwinding by @mkannwischer in #1558
• Lint: Replace black with ruff by @mkannwischer in #1653
• Use heap allocation + valgrind in backend unit test by @hanno-becker in #1633
• Remove --no-array-field-sensitivity for all proofs by @rod-chapman in #1654
• Correct declaration and comments re size of rej-uniform lookup table by @rod-chapman in #1657
• Nix: Bump s2n-bignum and hol_light by @mkannwischer in #1659
• Port: Allow tables to be declared static by @mkannwischer in #1658
• HOL-Light: Remove memaccess_inbounds duplicates workaround by @mkannwischer in #1660
• check-contracts: Detect contracts separated from prototype by a comment by @mkannwischer in #1661
• Remove 2 dead instruction from AArch64 back-end poly_tomont() by @rod-chapman in #1664
• native: Unify asm backend symbol naming by @mkannwischer in #1663
• CI: Bump ACVP, liboqs, expo, and AWS-LC versions by @mkannwischer in #1662
• Port Baremetal: Add Cortex-M33 MPS3-AN524 platform support by @willieyz in #1579
• CI: Re-enable RISE RISC-V runner by @mkannwischer in #1667
• nix: Pull CBMC 6.9.0 from nixos-unstable binary cache by @mkannwischer in #1666
• Documentation: Convert to Doxygen-style function headers and lint by @mkannwischer in #1669
• Add ACVP test Windows support (C backend) by @willieyz in #1668
• CI: Add zig 0.16 compiler tests by @mkannwischer in #1670
• CI: Update Github action dependencies by @mkannwischer in #1675
• HOL-Light: Prefix imports to separate mlkem-native from s2n-bignum by @hanno-becker in #1676
• Lint: Document context parameter in public API for Doxygen by @mkannwischer in #1681
• CI: Re-enable nix compatibility tests by @mkannwischer in #1684
• README: Note other side-channel and fault attacks are currently out of scope by @mkannwischer in #1685
• nix: Anchor HOL-Light shellHook to repo root, not $PWD by @mkannwischer in #1687
• CBMC: Document and enforce 4 GiB limit of forall/exists quantifiers by @hanno-becker in #1694
• Align bench iteration macros between component and API benchmarks by @hanno-becker in #1697
• x86_64: 32-byte align Keccak x4 AVX2 stack frame by @hanno-becker in #1704
• CI: Re-Enable Cortex-A76 benchmarks by @willieyz in #1706
• CI: Migrate OpenTitan integration to Pavona by @mkannwischer in #1707
• CI: Add more legacy compiler tests and move to scheduled workflow by @mkannwischer in #1700
• CI: Add gcc16 tests by @mkannwischer in #1709
• CI: Switch HOL-Light proofs to free Github runners by @mkannwischer in #1710
• CI: Check that all HOL-Light .S files are autogenerated by @mkannwischer in #1713
• CI: Move RISC-V runner jobs into a standalone workflow by @mkannwischer in #1708
• Add ppc64le backend (supports p8 and above architectures) [full CI] by @mkannwischer in #1677
• nix: bump to nixpkgs 26.05 by @mkannwischer in #1711
• Fix minor inconsistencies by @mkannwischer in #1729
• Fix signed-shift UB on 16-bit-int targets in mlk_rej_uniform_c and mlk_poly_frombytes_c by @mkannwischer in #1727
• AVR: Prevent ACVP harness stack overflow under full UBSan by @hanno-becker in #1736
• AVR: Propagate test exit codes through simavr by @mkannwischer in #1734
• autogen: Allow --force-cross to target specific architectures by @hanno-becker in #1735
• x86_64: Use SysV calling convention for assembly on Windows by @mkannwischer in #1730
• Add clang-tidy to lint by @hanno-becker in #1737
• Nix: Remove valgrind from default shell and small clean-up by @mkannwischer in #1731
• RV64: Minor bug fix and constant-time hardening by @mkannwischer in #1732
• CI: Update dependencies and integration pins by @mkannwischer in #1718
• HOL-Light: Switch to mlk_ namespace by @hanno-becker in #1739
• CI: Improve workflow robustness by @mkannwischer in #1733
• integration/liboqs: add ppc64le backend entries by @bhess in #1740
• mlkem_native.h: Fix MLK_TOTAL_ALLOC worst-case for legacy builds by @mkannwischer in #1743
• Add kat test Windows support (C backend only) by @willieyz in #1698
• Armv8.1-M: Expand x4 XOR/extract macro comments by @mkannwischer in #1715
• nix: Bump CBMC to latest develop to work around z3 soundness issue by @mkannwischer in #1745
• RELEASE: Add release notes for v1.2.0 by @mkannwischer in #1746

Full Changelog: v1.1.0...v1.2.0