Formal Verification in Cryptography: From Theory to Practice

Why Testing Isn't Enough

Traditional software testing has a fundamental limitation: it can only prove the presence of bugs, never their absence. For cryptographic code, where a single subtle error can compromise security for millions of users, this isn't acceptable.

Formal verification offers a different approach: mathematical proofs that guarantee code behaves correctly for all possible inputs, not just the ones we thought to test.

The Verification Spectrum

Levels of Assurance

Each level builds on the previous, offering increasing confidence at increasing cost.

Our Verification Approach

Specification-First Development

Every cryptographic primitive in HPCrypt starts with a formal specification:

// 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)

Implementation Verification

We then prove our implementation matches the specification using multiple techniques:

1. Equivalence Checking

Verify 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)

2. Constant-Time Verification

Prove 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))

3. Memory Safety

Prove absence of 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 that allows us to write 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 underwent 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 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 Trade-offs

What Verification Provides

Mathematical Certainty: When a proof succeeds, the property holds for all inputs—no edge cases, no corner cases, no "we didn't think of that."

Documentation: Formal specifications serve as precise, unambiguous documentation of intended behavior.

Regression Prevention: If code changes break verified properties, the proofs fail to compile.

The Costs

Development Time: Verified code takes 5-10x longer to develop than tested code.

Expertise Required: Formal methods require specialized knowledge not common among developers.

Maintenance Burden: Proofs must be maintained alongside code.

When It's 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

Getting Started

If you're interested in formal verification for cryptography:

1. Start Small: Verify a single function, like 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. Leverage Existing Work: HACL* and EverCrypt provide verified cryptographic primitives

Conclusion

Formal verification transforms cryptographic implementation from an art requiring constant vigilance into an engineering discipline with mathematical guarantees. The investment is significant, but for code protecting millions of users, it's an investment worth making.

At Seceq, we believe verified cryptography should be the standard, not the exception. HPCrypt represents our commitment to this vision—high-performance cryptography you can trust because it's proven correct.