Skip to content

README.md

Latest commit

 

History

History
344 lines (235 loc) · 15.8 KB

README.md

File metadata and controls

344 lines (235 loc) · 15.8 KB
Raw

Overview

These directories contain files for proving the functional correctness of the corecrypto ML-KEM and ML-DSA implementations. We use SAW to prove that each C function satisfies its Cryptol functional specification and its SAW precondition/postcondition contract. We also use SAW to check that our C functions are memory-safe and have no undefined C behaviors.

We then use Isabelle and the cryptol-to-isabelle translator to prove that each Cryptol spec is a behavioral refinement of its corresponding FIPS spec, given appropriate input constraints.

We also use Isabelle to prove under the same input constraints that our ARM64 subroutines are functionally equivalent to their corresponding C functions. For this purpose, we use the C functions themselves as formal specifications.

Assurance

soundness.md discusses the scope of our proofs and important considerations to keep in mind when reviewing the files.

Formal verification for Apple corecrypto: ML-KEM and ML-DSA in 2026 discusses our formal verification process, tools, and proofs.

SAW proofs

Note that you don't need to run the SAW proofs if you are only interested in running the Isabelle proofs. However, you will need to perform the steps for installing SAW itself as some of our Isabelle proof commands call out to SAW and its associated SMT solvers.

Prerequisites:

  • macOS 26.5
  • Xcode 26.5 (with command-line tools)

Installing SAW

  • Download the file saw-1.5.1-macos-15-ARM64-with-solvers.tar.gz from https://github.com/GaloisInc/saw-script/releases/tag/v1.5.1

  • tar xfz saw-1.5.1-macos-15-ARM64-with-solvers.tar.gz

  • Add saw-1.5.1-macos-15-ARM64-with-solvers/bin/ to your PATH

  • chmod u+x /path/to/saw-1.5.1-macos-15-ARM64-with-solvers/bin/*

  • saw --version to confirm your SAW version

Performing all proofs

  • Install the Python3 lmdb module if you haven't already: pip3 install lmdb
  • cd corecrypto
  • scripts/run-saw-verify.py

Note that the proofs will run in parallel. A full run can take 20+ hours to complete on an M4 MacBook Pro, depending on how much memory you have.

Pass -n to disable the solver cache (which will be populated on the first run and used subsequently) and -s to force running proofs sequentially.

Pass --dev to run symbolic execution only, i.e., generate proof obligations and discharge them by admission.

Performing only specific proofs

To run a single proof, pass its name as an argument to the script:

  • scripts/run-saw-verify.py ccmlkem/sample

To run multiple proofs, simply pass all names:

  • scripts/run-saw-verify.py ccmlkem/sample ccmldsa/sample

Isabelle proofs

The following steps demonstrate how we prove that our Cryptol spec for each C function is a behavioral refinement of its corresponding FIPS spec, given appropriate input constraints. Some of the terminology we use in our proofs is listed at the bottom of this README file.

Our refinement framework is based on the concept of logical relations that is also used by Isabelle's transfer package. Many of our logical relations are actually partial functions since our Cryptol and FIPS specifications are deterministic.

We also prove that our ML-KEM ARM64 assembly subroutines are behaviorally equivalent to their corresponding C subroutines. Together, these theorems establish the desired correctness properties of our implementation.

Although we use SAW and the cryptol-to-isabelle translator, currently there is no translator from SAW's outer-level specification language into Isabelle. So the last step in our assurance argument, namely composing the Isabelle C and ARM64 refinement proofs, remains informal.

Open-source Isabelle libraries

The default license for the corecrypto (cc) project is the evaluation-only corecrypto Internal Use License Agreement contained in License.txt. However, to enable wider use, some Isabelle files are also licensed under more permissive terms. These files are located in corecrypto_verify/isabelle/Apple_Isabelle_Libraries. They consist of our PQC-related FIPS formal specifications, proofs about Plantard arithmetic operations, and a library for performing refinement proofs based on logical relations. Additionally, files related to the cryptol-to-isabelle translator, contained in corecrypto_verify/isabelle/Cryptol/cryptol-to-isabelle/isabelle are available under their accompanying LICENSE file.

Running the Isabelle C proofs

The rest of this README outlines our Isabelle proofs. They are organized into theory files with names ending in .thy.

Step 1

Install SAW by following the "SAW proofs" instructions above. This step is necessary since some of our Isabelle proof commands call out to SAW. However, you don't need to then run the SAW proofs if you only wish to run our Isabelle proofs.

Step 2

Install Isabelle. We run our proofs on the macOS version of Isabelle2025-2 and assume it has been placed in the default /Applications directory. Your machine should have at least 32GB of memory.

WARNING: As of this writing, the Isabelle executables have not been notarized by Apple, so you may see a security warning dialog box when you first try to launch the application.

If your Isabelle application is in a different location, then you will need to modify the last line of the corecrypto/corecrypto_verify/isabelle/isa script to run your Isabelle application's isabelle executable. The executable will be located in the bin directory of the Isabelle application's root directory.

NOTE: Some calls to Isabelle proof tactics produce a lot of trace messages. We recommend running corecrypto/corecrypto_verify/isabelle/isa jedit to launch Isabelle and then set "Editor Tracing Messages" to 0 in the Isabelle/jEdit Plugins menu, menu item "Plugin Options...", Isabelle/General section of the dialog box that opens. Then quit Isabelle. Otherwise, the commands are paused by Isabelle and need user interaction to continue.

Step 3

Run the following command in your terminal window:

  • cd corecrypto/corecrypto_verify/isabelle

Here and in the steps below, corecrypto refers to the corecrypto root directory name. The rest of the steps assume you are in the isabelle subdirectory.

Then the top-level correctness theorems for the ML-KEM and ML-DSA entry point C functions are here:

  • CCMLKEM/ccmlkem_kem_MT_refines_FIPS.thy
  • CCMLDSA/ccmldsa_MT_refines_FIPS.thy

Step 4

Download the AFP and install it as a component.

If you haven't added Isabelle's bin directory to your path, then you will need to install the AFP entries using this command instead of the isabelle components -u command described in the AFP help page:

  • ./isa components -u <path-to-uncompressed-AFP-thys-directory>

Step 5

Generate initial Isabelle heap images (this will take a while):

  • ./isa build -d . -b Cryptol CCMLKEM CCMLDSA

Step 6

Launch the Isabelle GUI and open the main ML-KEM theory file:

  • ./isa jedit -d . -l CCMLKEM CCMLKEM/ccmlkem_kem_MT_refines_FIPS.thy &

You can alternatively run this command to open the main ML-DSA theory file:

  • ./isa jedit -d . -l CCMLDSA CCMLDSA/ccmldsa_MT_refines_FIPS.thy &

If you wish to edit the corecrypto Isabelle theory files after they are loaded or examine the state of each proof step, then you can run one of these commands instead, although they will take longer to finish and require more memory:

  • ./isa jedit -d . -l Apple_Public CCMLKEM/ccmlkem_kem_MT_refines_FIPS.thy &

  • ./isa jedit -d . -l Apple_Public CCMLDSA/ccmldsa_MT_refines_FIPS.thy &

You can watch Isabelle's progress by clicking on the "Theories" button on the right side of the Isabelle window.

Enable "Proof state" in the output window to examine individual proof steps. You can open the output window by clicking on the "Output" button at the bottom of the Isabelle window.

Step 7

Once Isabelle has loaded the theories, you can command-click on constants and theorem names to jump to their definitions. You can use the left-arrow button at the top left corner of the Isabelle window to return back to where you were.

Running the ARM64 subroutine proofs

To run the ARM64 subroutine proofs, you need to build the assembler files first. Go into the corecrypto root directory and run:

  • xcodebuild -arch arm64 -target libAccelerateCrypto "ENABLE_SHA512_INSTRUCTIONS=" OTHER_LIBTOOLFLAGS="-no_warning_for_no_symbols"
  • cp build/Release/libAccelerateCrypto.a corecrypto_verify/isabelle/AccelerateCrypto
  • cd corecrypto_verify/isabelle

The proofs are found in the AccelerateCrypto directory. After building libAccelerateCrypto.a, we can build the corresponding Isabelle heap:

  • ./isa build -d . -b AccelerateCrypto

Or inspect the files in the Isabelle GUI:

  • ./isa jedit -d . -l AccelerateCrypto AccelerateCrypto/AccelerateCrypto.thy

Architecture for the C function proofs

Definitions

We have three kinds of Isabelle definitions: FIPS specifications, hand-translated Cryptol functions, and machine-translated Cryptol functions.

The FIPS specs are the most abstract, followed by the hand translations, and then the machine translations. We prove that each function refines its corresponding function at the next higher abstraction level. Finally, we compose the refinement theorems to show that the entry point machine-translated functions refine their FIPS specifications.

Filenames

Our directory and file naming conventions reflect our proof architecture.

The FIPS 202, FIPS 203, and FIPS 204 standards are formalized in the Apple_Isabelle_Libraries/FIPS_Specifications directory as the theories FIPS202.thy, FIPS203.thy, and FIPS204.thy, respectively.

ML-KEM theory files live in the CCMLKEM directory, and ML-DSA theories live in CCMLDSA. The filenames within these directories start with ccmlkem_ or ccmldsa_, respectively, since Isabelle theory files must be uniquely named.

The Cryptol specifications for our C files are located in the corecrypto repository, in subdirectory corecrypto_verify. Our Isabelle directories are in corecrypto_verify/isabelle.

Proofs that particular machine-translated Cryptol functions refine their hand-translated versions have MT_refines_HT in their filename.

Similarly, proofs that hand-translated Cryptol functions refine their FIPS specifications have HT_refines_FIPS in their filename.

Some proofs refine the hand-translated Cryptol functions to an intermediate version of the FIPS specifications which uses CCERR_ constants and a result pair instead of a sum type. They have HT_refines_CCErr in their filename.

These refinement theorems are chained together in files whose names contain MT_refines_FIPS. We only need to chain refinements of the entry point functions.

The MT directory contains a snapshot of the machine-translated Cryptol files.

The CC directory contains hand-translated Cryptol files of Cryptol specs originally located in the corecrypto_verify directory.

Hand-translated Cryptol files from corecrypto_verify/mlkem and corecrypto_verify/mldsa are contained in the CCMLKEM and CCMLDSA directories.

The Cryptol directory contains definitions and theorems for reasoning about machine-translated and hand-translated Cryptol primitives. Some hand-translated Cryptol primitives are represented by existing Isabelle/HOL or Word_Lib functions, so we don't create new definitions for those.

The Prelude directory contains files that don't depend on Cryptol or PQC definitions.

Architecture for the ARM64 subroutine proofs

The ARM64 directory contains the ARM64 model and refinement framework. The ARM64 model consists of

  • ARM64_Model: the machine model and the instructions
  • ARM64_Decode: the mapping from 32-bit codes to instructions
  • ARM64_Linker: defines how Mach-O relocates instructions
  • ARM64_ProcedureCallStandard: defines how an ARM64 routine is embedded into the C model
  • ARM64_Import: imports a Mach-O library into Isabelle/HOL

The remaining files are concerned with the refinement, relating the ARM64 routines to an abstract representation where concrete memory accesses are replaced with local variables.

In the Import directory are the theory and auxiliary files to import the corresponding C files into Isabelle/HOL.

The actual refinement of corecrypto's MLKEM assembly routines happens in the AccelerateCrypto directory. This directory contains for each routine ccmlkem_<func> a file called Equiv_<func>.thy. The refinements from C to an abstract version and from ARM64 to an abstract version are usually found in <Func>_C.thy and <Func>_ARM64.thy.

Finally, everything is imported into AccelerateCrypto/AccelerateCrypto.thy which lists all final verification theorems.

Reproducing the machine-translated Cryptol files

These steps are not necessary to run the Isabelle C proofs but are provided for you to check that our machine-translated Cryptol files match our original Cryptol definitions.

Step 1

Install the SAW executables and add them to your Unix path by following the instructions in Section "SAW proofs" above.

Step 2

In the SAW distribution, the translator's required Isabelle theory files are located in saw-1.5.1-macos-15-ARM64-with-solvers/lib/isabelle/theories.

Meanwhile, the directory corecrypto/corecrypto_verify/isabelle/Cryptol/cryptol-to-isabelle/isabelle contains a snapshot of the translator's Isabelle theory files. So you will need to copy over the translator's theory files or symlink to them to ensure you are using the correct versions.

Alternatively, you can simply diff -rq the two directories to confirm the files are the same.

Step 3

Run the following commands:

  • cd corecrypto/corecrypto_verify/isabelle
  • mv MT/MT.thy MT/MT.thy.TEMP
  • rm MT/*.thy
  • mv MT/MT.thy.TEMP MT/MT.thy
  •   cryptol-to-isabelle \
      --source ../ccmlkem/kem.cry \
      --source ../ccmldsa/keygen.cry \
      --source ../ccmldsa/verify.cry \
      --dest MT \
      --all-modules \
      --cryptol-path .. \
      --cryptol-path ../ccmlkem \
      --cryptol-path ../ccmldsa

The machine-translated Cryptol files will now be in the MT directory.

Terminology

"spec" is an abbreviation of "specification".

"Isabelle" refers to the Isabelle theorem prover.

"Cryptol" and "SAW" refer to the open-source tools provided by Galois.

"translator" refers to the open-source cryptol-to-isabelle tool also provided by Galois.

By "machine-translated Cryptol file" or "machine translation" we mean an Isabelle theory file that is automatically generated from a Cryptol source file by the cryptol-to-isabelle translator.

A "hand-translated Cryptol file" or "hand translation" is an Isabelle theory file containing definitions of Cryptol functions that we wrote by hand before the cryptol-to-isabelle translator was available. The hand translations use different types that are closer to our FIPS specifications but have the same behavior as the machine translations (under appropriate input constraints).

"FIPS specs" refers either to the FIPS 202, FIPS 203, and FIPS 204 standards available from NIST or to our Isabelle formalizations of them.