Merge pull request #901 from pq-code-package/readme_update

Update and extend README's on formal verification

Author: hanno-becker

README.md

@@ -13,11 +13,12 @@
 mlkem-native is a secure, fast, and portable C90 implementation of [ML-KEM](https://doi.org/10.6028/NIST.FIPS.203).
 It is a fork of the ML-KEM [reference implementation](https://github.com/pq-crystals/kyber/tree/main/ref).
 
+Large parts of mlkem-native are formally verified: All C code in [mlkem/*](mlkem) and [mlkem/fips202/*](mlkem/fips202) is verified
+using [CBMC](https://github.com/diffblue/cbmc) to be free of various classes of undefined behaviour. [HOL-Light](https://github.com/jrh13/hol-light) is used to verify
+the functional correctness of core AArch64 assembly routines.
+
 mlkem-native includes native backends for AArch64 and AVX2, offering competitive performance on most Arm, Intel, and AMD platforms
-(see [benchmarks](https://pq-code-package.github.io/mlkem-native/dev/bench/)). The frontend and the C backend (i.e., all C code in [mlkem/*](mlkem) and [mlkem/fips202/*](mlkem/fips202)) are verified
-using [CBMC](https://github.com/diffblue/cbmc) to be free of various classes of undefined behaviour. In particular, there are no out of
-bounds accesses, nor integer overflows during optimized modular arithmetic.
-[HOL-Light](https://github.com/jrh13/hol-light) is used to verify the functional correctness of core AArch64 assembly routines.
+(see [benchmarks](https://pq-code-package.github.io/mlkem-native/dev/bench/)).
 
 mlkem-native is supported by the [Post-Quantum Cryptography Alliance](https://pqca.org/) as part of the [Linux Foundation](https://linuxfoundation.org/).
 

proofs/README.md

@@ -0,0 +1,13 @@
+[//]: # (SPDX-License-Identifier: CC-BY-4.0)
+
+# Proofs for mlkem-native
+
+This directory contains material related to the formal verification of the source code of mlkem-native.
+
+## C verification: CBMC
+
+We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to show the absence of various classes of undefined behaviour in the mlkem-native C source, including out of bounds memory accesses and integer overflows. See [proofs/cbmc](cbmc).
+
+## Assembly verification: HOL-Light
+
+We use the [HOL-Light](https://github.com/jrh13/hol-light) interactive theorem prover alongside the verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to show the functional correctness of various highly optimized assembly routines in mlkem-native at the object-code level. See [proofs/hol_light/arm](hol_light/arm).

proofs/cbmc/README.md

@@ -3,18 +3,46 @@
 CBMC proofs
 ===========
 
-# Overview
+This directory contains the infrastructure for running [CBMC](https://github.com/diffblue/cbmc) proofs
+for the absence of certain classes of undefined behaviour for parts of the C-code in mlkem-native.
 
-This directory contains [CBMC](https://github.com/diffblue/cbmc) proofs for the absence
-of certain classes of undefined behaviour for parts of the C-code in mlkem-native.
+## Primer
 
-Proofs are organized by functions, with the harnesses and proofs for each function
-in a separate directory.
+Proofs are organized by functions, with the harnesses for each function in a separate directory.
+Specifications are directly embedded inside the mlkem-native C-source as contract and loop annotations;
+the CBMC harnesses are boilerplate only and don't add to the specification.
 
-See the [Proof Guide](proof_guide.md) for a walkthrough of how to use CBMC and
-develop new proofs.
+For example, these are the specification and proof of the `poly_add` function:
+```c
+void mlk_poly_add(mlk_poly *r, const mlk_poly *b)
+__contract__(
+  requires(memory_no_alias(r, sizeof(mlk_poly)))
+  requires(memory_no_alias(b, sizeof(mlk_poly)))
+  requires(forall(k0, 0, MLKEM_N, (int32_t) r->coeffs[k0] + b->coeffs[k0] <= INT16_MAX))
+  requires(forall(k1, 0, MLKEM_N, (int32_t) r->coeffs[k1] + b->coeffs[k1] >= INT16_MIN))
+  ensures(forall(k, 0, MLKEM_N, r->coeffs[k] == old(*r).coeffs[k] + b->coeffs[k]))
+  assigns(memory_slice(r, sizeof(mlk_poly)))
+);
 
-# Usage
+...
+
+void mlk_poly_add(mlk_poly *r, const mlk_poly *b)
+{
+  unsigned i;
+  for (i = 0; i < MLKEM_N; i++)
+  __loop__(
+    invariant(i <= MLKEM_N)
+    invariant(forall(k0, i, MLKEM_N, r->coeffs[k0] == loop_entry(*r).coeffs[k0]))
+    invariant(forall(k1, 0, i, r->coeffs[k1] == loop_entry(*r).coeffs[k1] + b->coeffs[k1])))
+  {
+    r->coeffs[i] = r->coeffs[i] + b->coeffs[i];
+  }
+}
+```
+
+See the [Proof Guide](proof_guide.md) for a walkthrough of how to use CBMC and develop new proofs.
+
+## Reproducing the proofs
 
 To run all proofs, print a summary at the end and reflect overall
 success/failure in the error code, use
@@ -31,6 +59,6 @@ Alternatively, you can use the [tests](../../scripts/tests) script, see
 tests cbmc --help
 ```
 
-# Covered functions
+## What is covered?
 
 Each proved function has an eponymous sub-directory of its own. Use [list_proofs.sh](list_proofs.sh) to see the list of functions covered.

proofs/hol_light/arm/README.md

@@ -9,31 +9,52 @@ prover, utilizing the assembly verification infrastructure from [s2n-bignum](htt
 
 Each function is proved in a separate `.ml` file in [proofs/](proofs). Each file
 contains the byte code being verified, as well as the specification that is being
-proved. Specifications are essentially Hoare triples, with the noteworthy difference
-that the program is implicit as the content of memory at the PC; which is asserted to
-be the code under verification as part of the precondition.
+proved.
 
-## What is covered?
+## Primer
 
-At present, this directory contains functional correctness proofs for the following functions:
+Proofs are 'post-hoc' in the sense that HOL-Light/s2n-bignum operate on the final object code. In particular, the means by which the code was generated (including the [SLOTHY](https://github.com/slothy-optimizer/slothy/) superoptimizer) need not be trusted.
 
-- ML-KEM Arithmetic:
-  * AArch64 forward NTT: [mlkem_ntt.S](mlkem/mlkem_ntt.S)
-  * AArch64 inverse NTT: [mlkem_intt.S](mlkem/mlkem_intt.S)
-  * AArch64 base multiplications: [mlkem_poly_basemul_acc_montgomery_cached_k2.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S) [mlkem_poly_basemul_acc_montgomery_cached_k3.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S) [mlkem_poly_basemul_acc_montgomery_cached_k4.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
-  * AArch64 conversion to Montgomery form: [mlkem_poly_tomont.S](mlkem/mlkem_poly_tomont.S)
-  * AArch64 modular reduction: [mlkem_poly_reduce.S](mlkem/mlkem_poly_reduce.S)
-  * AArch64 'multiplication cache' computation: [mlkem_poly_mulcache_compute.S](mlkem/mlkem_poly_mulcache_compute.S)
-- FIPS202:
-  * Keccak-F1600 using lazy rotations (see [this paper](https://eprint.iacr.org/2022/1243)): [keccak_f1600_x1_scalar.S](mlkem/keccak_f1600_x1_scalar.S)
-  * Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a.S](mlkem/keccak_f1600_x1_v84a.S)
-  * 2-fold Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x2_v84a.S](mlkem/keccak_f1600_x2_v84a.S)
-  * 'Hybrid' 4-fold Keccak-F1600 using scalar and v8-A Neon instructions: [keccak_f1600_x4_v8a_scalar.S](mlkem/keccak_f1600_x4_v8a_scalar.S)
-  * 'Triple hybrid' 4-fold Keccak-F1600 using scalar, v8-A Neon and v8.4-A+SHA3 Neon instructions:[keccak_f1600_x4_v8a_v84a_scalar.S](mlkem/keccak_f1600_x4_v8a_v84a_scalar.S)
+Specifications are essentially [Hoare triples](https://en.wikipedia.org/wiki/Hoare_logic), with the noteworthy difference that the program is implicit as the content of memory at the PC; which is asserted to
+be the code under verification as part of the precondition. For example, the following is the specification of the `poly_reduce` function:
 
-The NTT and invNTT functions are super-optimized using [SLOTHY](https://github.com/slothy-optimizer/slothy/).
+```ocaml
+ (* For all (abbreviated by `!` in HOL):
+    - a: Source pointer
+    - pc: Current value of Program Counter (PC)
+    - returnaddress: Return address in the link register *)
+`!a x pc returnaddress.
+    (* Assume that the program and the source pointer don't overlap *)
+    nonoverlapping (word pc,0x124) (a,512)
+    ==> ensures arm
+      (* Precondition *)
+      (\s. (* The memory at the current PC is the byte-code of poly_reduce() *)
+        aligned_bytes_loaded s (word pc) mlkem_poly_reduce_mc /\
+        read PC s = word pc /\
+        (* The return address is stored in the link register (LR) *)
+        read X30 s = returnaddress /\
+        (* The source pointer is in X0 *)
+        C_ARGUMENTS [a] s /\
+        (* Give a name to the memory contents at the source pointer *)
+        !i. i < 256
+            ==> read(memory :> bytes16(word_add a (word(2 * i)))) s = x i)
+      (* Postcondition: Eventually we reach a state where ... *)
+      (\s.
+        (* The PC is the original value of the link register *)
+        read PC s = returnaddress /\
+        (* The integers represented by the final memory contents
+         * are the unsigned canonical reductions mod 3329
+         * of the integers represented by the original memory contents. *)
+        !i. i < 256
+            ==> ival(read(memory :> bytes16 (word_add a (word(2 * i)))) s) =
+                ival(x i) rem &3329)
+      (* Footprint: The program may modify (only) the ABI permitted registers
+       * and flags, and the memory contents at the source pointer. *)
+      (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
+       MAYCHANGE [memory :> bytes(a,512)])`
+```
 
-## Running the proofs
+## Reproducing the proofs
 
 To reproduce the proofs, enter the nix shell via
 
@@ -50,3 +71,23 @@ make -C proofs/hol_light/arm
 will build and run the proofs. Note that this make take hours even on powerful machines.
 
 For convenience, you can also use `tests hol_light` which wraps the `make` invocation above; see `tests hol_light --help`.
+
+## What is covered?
+
+At present, this directory contains functional correctness proofs for the following functions:
+
+- ML-KEM Arithmetic:
+  * AArch64 forward NTT: [mlkem_ntt.S](mlkem/mlkem_ntt.S)
+  * AArch64 inverse NTT: [mlkem_intt.S](mlkem/mlkem_intt.S)
+  * AArch64 base multiplications: [mlkem_poly_basemul_acc_montgomery_cached_k2.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S) [mlkem_poly_basemul_acc_montgomery_cached_k3.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S) [mlkem_poly_basemul_acc_montgomery_cached_k4.S](mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
+  * AArch64 conversion to Montgomery form: [mlkem_poly_tomont.S](mlkem/mlkem_poly_tomont.S)
+  * AArch64 modular reduction: [mlkem_poly_reduce.S](mlkem/mlkem_poly_reduce.S)
+  * AArch64 'multiplication cache' computation: [mlkem_poly_mulcache_compute.S](mlkem/mlkem_poly_mulcache_compute.S)
+- FIPS202:
+  * Keccak-F1600 using lazy rotations (see [this paper](https://eprint.iacr.org/2022/1243)): [keccak_f1600_x1_scalar.S](mlkem/keccak_f1600_x1_scalar.S)
+  * Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a.S](mlkem/keccak_f1600_x1_v84a.S)
+  * 2-fold Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x2_v84a.S](mlkem/keccak_f1600_x2_v84a.S)
+  * 'Hybrid' 4-fold Keccak-F1600 using scalar and v8-A Neon instructions: [keccak_f1600_x4_v8a_scalar.S](mlkem/keccak_f1600_x4_v8a_scalar.S)
+  * 'Triple hybrid' 4-fold Keccak-F1600 using scalar, v8-A Neon and v8.4-A+SHA3 Neon instructions:[keccak_f1600_x4_v8a_v84a_scalar.S](mlkem/keccak_f1600_x4_v8a_v84a_scalar.S)
+
+The NTT and invNTT functions are super-optimized using [SLOTHY](https://github.com/slothy-optimizer/slothy/).