Foundation: machine-checked cryptography, in the open

Foundation: machine-checked cryptography, in the open

The National Security Agency has released Foundation as open source at https://github.com/NationalSecurityAgency/Foundation.

Foundation is a repository of formal specifications for cryptographic algorithms, written so that the specification, its mathematical properties, and the checks that keep them true all live in one place—and get re-verified on every commit.

What's in it

Foundation currently covers the symmetric and hashing core that most other constructions build on:

AES (FIPS 197)
SHA-1 (FIPS 180-4), SHA-2 (all six variants), SHA-3 (FIPS 202)
SHAKE, cSHAKE, KMAC, TupleHash, ParallelHash (SP 800-185)
HMAC (FIPS 198-1)
ECDSA over the NIST prime curves (FIPS 186-5)
AES Key Wrap (SP 800-38F)
PBKDF (SP 800-132)

Each algorithm is specified in Cryptol with its correctness properties stated alongside and discharged by an SMT solver. Where we have example implementations (AES has one in Rust today), the Software Analysis Workbench proves them equivalent to the Cryptol. GitHub Actions re-runs the whole set on every push, so a change that breaks a proof breaks the build.

These are example implementations and specifications, not a hardened cryptographic library. Use them to understand an algorithm, to test another implementation against, or as a starting point for your own assured code.

How the method works
  1. Start from the standard.
  2. Transcribe it into Cryptol—a bit-precise, executable domain-specific language for cryptography. Because Cryptol specs run, you can load one at the REPL, feed it inputs, and watch the algorithm compute step by step; then check any other implementation by running the same inputs through both.
  3. State the algorithm's properties (test vectors pass, decrypt inverts encrypt, and so on) as Cryptol property declarations and prove them.
  4. When there is a separate implementation in Rust or C, use SAW to prove it computes the same function as the Cryptol. Cryptol's foreign declarations then let the spec call that implementation directly through the C ABI—so the same Rust code that SAW just proved correct is what runs when you evaluate the spec at the REPL. AES in this repository is wired that way.
  5. Wire steps 3 and 4 into CI.

Foundation is a worked corpus of that loop, plus the CI plumbing to run it yourself.

What's next

The near-term roadmap fills out the Commercial National Security Algorithm Suite 2.0:

ML-KEM (FIPS 203), ML-DSA (FIPS 204), and XMSS (SP 800-208). Cryptol specifications for all three already exist in GaloisInc/cryptol-specs.
LMS (SP 800-208). LMS and XMSS are the stateful hash-based signature schemes; both sit on top of Merkle trees, so a reusable, formally validated Merkle-tree specification is part of that work.

Contributing

Feel free to contribute—issues and pull requests are open. Some places to start:

  • Cryptol specs for algorithms on the roadmap—CNSA 2.0 primitives, current FIPS and NIST SP 800-series standards, and their approved modes. (Foundation is scoped to algorithms in current use; historical or toy ciphers belong elsewhere.)
  • Example implementations in Rust (or C) for algorithms that currently have only a spec, along with the SAW script that ties them together.
  • Sharper properties, or proofs for properties that are currently only tested.
  • CI and tooling—anything that makes the assurance loop faster or easier to reproduce.

CONTRIBUTING.md in the repo has the mechanics.

Getting started

git clone https://github.com/NationalSecurityAgency/Foundation 
cd Foundation

The repository ships two dev-container configurations (one Cryptol-focused, one SAW-focused) that work with GitHub Codespaces or VS Code's Dev Containers extension, so you can be proving properties without installing a toolchain locally. The README has the links.

Foundation is released under the Apache License 2.0. Portions authored by U.S. Government employees in the course of their duties are in the public domain in the United States; see NOTICE.md in the repository for the full statement. Cryptol and SAW are developed by Galois, Inc.

Submitted by Regan Williams on