Skip to content

SOUNDNESS.md

Latest commit

 

History

History
53 lines (39 loc) · 3.18 KB

SOUNDNESS.md

File metadata and controls

53 lines (39 loc) · 3.18 KB

Formal Verification in mldsa-native: Scope, Assumptions, Risks

This document describes the scope, assumptions and risks of the formal verification efforts around mldsa-native.

We see this as a living document. If you have suggestions for improvements, such as soundness risks missing from or insufficiently covered in this document, please reach out to us or open an issue. However, if you find a potential security vulnerability in mldsa-native, do not open a public GitHub issue, but instead use private vulnerability reporting.

Shared analysis with mlkem-native

mldsa-native uses the same verification methodology as its sister project mlkem-native: CBMC for the C code (memory safety, type safety, and absence of undefined behavior), and HOL Light together with the s2n-bignum verification infrastructure for the AArch64 and x86_64 assembly backends (functional correctness, memory safety, and secret-independent execution).

The detailed analysis of the methods, formal models, trusted computing base, gaps and risks of these verification stacks is given in mlkem-native's SOUNDNESS document1 and the underlying s2n-bignum soundness document2. Except for the FIPS 203 vs. FIPS 204 specifications and the differing modular arithmetic constants, the analysis applies to mldsa-native unchanged: the same proof tools, the same ISA models, the same TCB, and therefore the same shared mitigations and residual risks.

Additional risks specific to mldsa-native

Incomplete HOL Light proof coverage

Unlike mlkem-native, where all AArch64 and x86_64 assembly routines have HOL Light specifications, mldsa-native's HOL Light proof coverage is not yet complete. The full list of functions that are covered today is maintained in proofs/hol_light/README.md.

The remaining HOL Light proof work is tracked in two umbrella issues:

  • AArch64 backend: #918
  • x86_64 backend: #912

For the routines without HOL Light specifications, functional correctness, memory safety, and constant-time properties are validated empirically through the full test suite (functional tests, KAT, ACVP, unit tests, and valgrind-based constant-time tests on AArch64 and x86_64), but they are not formally proved.

We aim to close this gap and achieve full HOL Light coverage of the AArch64 and x86_64 backends prior to the first stable release of mldsa-native.

Footnotes

  1. pq-code-package: mlkem-native SOUNDNESS document, https://github.com/pq-code-package/mlkem-native/blob/main/SOUNDNESS.md ↩

  2. Amazon Web Services: s2n-bignum soundness documentation, https://github.com/awslabs/s2n-bignum/blob/main/doc/s2n_bignum_soundness.md ↩