Formal verification of cryptographic code, with an ML-KEM case study

What testing cannot show

Testing can only prove the presence of bugs, never their absence. For cryptographic code, where one subtle error can compromise security for millions of users, that is not acceptable.

Formal verification uses mathematical proofs to guarantee that code behaves correctly for all possible inputs, including the ones nobody thought to test.

Levels of assurance

Each level builds on the previous one, giving more confidence at a higher cost.

How we verify OpenCrypt

Specification first

Every cryptographic primitive in OpenCrypt starts with a formal specification. For AES-GCM encryption:

// Formal specification for AES-GCM encryption
spec aes_gcm_encrypt(key: [u8; 32], nonce: [u8; 12], plaintext: [u8], aad: [u8]) -> [u8]:
    // Confidentiality: ciphertext reveals nothing about plaintext
    // without the key
    forall adversary A:
        Pr[A distinguishes (encrypt(k, n, m)) from random] < negligible

    // Authenticity: cannot forge valid ciphertext without key
    forall adversary A:
        Pr[A produces valid (c, tag) without k] < negligible

    // Correctness: decryption recovers plaintext
    forall k, n, m, aad:
        decrypt(k, n, encrypt(k, n, m, aad), aad) = Some(m)

Proving the implementation correct

We then prove that the implementation matches the specification, using several techniques.

Equivalence checking verifies that optimized code produces identical results to a reference implementation:

theorem aes_optimized_correct:
    forall key, plaintext:
        aes_encrypt_avx2(key, plaintext) = aes_encrypt_reference(key, plaintext)

Constant-time verification proves that execution time doesn't depend on secret values:

theorem aes_constant_time:
    forall key1, key2, plaintext:
        execution_trace(aes_encrypt(key1, plaintext)) =
        execution_trace(aes_encrypt(key2, plaintext))

Memory safety proofs rule out buffer overflows, use-after-free and other memory errors:

theorem no_buffer_overflow:
    forall input where length(input) <= MAX_INPUT:
        all_memory_accesses(process(input)) are within bounds

Tools we use

Coq

Coq is an interactive theorem prover for writing machine-checked proofs:

(* Proving correctness of modular addition *)
Theorem mod_add_correct : forall a b p,
  0 <= a < p ->
  0 <= b < p ->
  mod_add a b p = (a + b) mod p.
Proof.
  intros a b p Ha Hb.
  unfold mod_add.
  destruct (a + b <? p) eqn:Hlt.
  - (* Case: a + b < p *)
    apply Z.ltb_lt in Hlt.
    rewrite Z.mod_small; omega.
  - (* Case: a + b >= p *)
    apply Z.ltb_ge in Hlt.
    rewrite Z.mod_eq; omega.
Qed.

F*

F* combines dependent types with SMT solving for semi-automated verification:

// Verified constant-time comparison
val ct_compare: b1:bytes -> b2:bytes{length b1 = length b2} -> bool
let ct_compare b1 b2 =
  let rec loop (i:nat{i <= length b1}) (acc:uint8) : uint8 =
    if i = length b1 then acc
    else loop (i+1) (acc |^ (index b1 i ^^ index b2 i))
  in
  loop 0 0uy = 0uy

// Proof that timing is independent of inputs
val ct_compare_timing: b1:bytes -> b2:bytes{length b1 = length b2} ->
  Lemma (timing(ct_compare b1 b2) = length b1 * LOOP_COST + CONST)

CBMC

For C code, we use bounded model checking to verify specific properties:

// Harness for verifying AES key expansion
void verify_aes_key_expansion() {
    uint8_t key[32];
    uint8_t expanded[240];

    // Assume arbitrary key
    __CPROVER_assume(true);

    // Run key expansion
    aes_key_expand(key, expanded);

    // Assert: expanded key has correct structure
    __CPROVER_assert(
        verify_key_schedule(key, expanded),
        "Key expansion produces valid schedule"
    );
}

Case study: verifying ML-KEM

Our ML-KEM implementation went through extensive formal verification.

Phase 1: algorithm specification

We formalized the ML-KEM specification in Coq, including:

• Polynomial arithmetic over Zq
• NTT transformations
• Compression and decompression functions
• The full encapsulation/decapsulation protocol

Phase 2: implementation verification

We proved that our Rust implementation matches the specification:

Phase 3: side-channel verification

We verified constant-time execution:

• No secret-dependent branches
• No secret-dependent memory accesses
• Timing independent of all secret values

Benefits and costs

What verification gives you

The main benefit is mathematical certainty: when a proof succeeds, the property holds for all inputs, with no edge cases, corner cases or "we didn't think of that". The specifications also document intended behavior precisely and unambiguously. And if a code change breaks a verified property, the proofs fail to compile, so regressions are caught.

What it costs

Verified code takes 5-10x longer to develop than tested code. It needs specialized knowledge that few developers have, and the proofs must be maintained alongside the code.

When it is worth it

Formal verification is most valuable when:

• The code handles cryptographic secrets
• Bugs have catastrophic consequences
• The code is long-lived and widely deployed
• The algorithm is well understood and stable

Where to start

If you want to try formal verification on cryptographic code:

1. Start small: verify a single function, such as constant-time comparison.
2. Use property testing: QuickCheck-style testing bridges the gap.
3. Learn gradually: F* and Dafny have gentler learning curves than Coq.
4. Build on existing work: HACL* and EverCrypt provide verified cryptographic primitives.

We think verified cryptography should be the norm, and we build OpenCrypt that way: fast cryptography that is proven correct.