How we formally verify cryptographic implementations in Coq

Why testing is not enough

In 2014, Heartbleed showed that even widely deployed, extensively tested cryptographic code can contain critical flaws. The OpenSSL bug had existed for over two years and affected an estimated 17% of secure web servers worldwide.

Testing, however thorough, can show the presence of bugs but never their absence. A single error in cryptographic code can compromise the security of millions of systems, so we need stronger guarantees. We use formal verification, meaning mathematical proof, to guarantee that our implementations are correct by construction.

Specifications and proofs in Coq

Our verification infrastructure is built around Coq, a mature proof assistant for writing machine-checkable proofs. Unlike an informal argument, a Coq proof is checked by a small, trusted kernel that has been extensively analyzed over decades.

Specification first

Every implementation starts with a formal specification in Coq that captures the exact mathematical definition from the relevant standard:

(* Formal specification of GHASH multiplication in GF(2^128) *)
Definition ghash_mul (x y : GF128) : GF128 :=
  let z := gf128_zero in
  fold_left (fun acc i =>
    let xi := gf128_bit x i in
    let v_shifted := gf128_shift acc in
    let z' := if xi then gf128_xor acc y else acc in
    if gf128_msb acc
    then gf128_xor v_shifted R
    else v_shifted
  ) (seq 0 128) z.

(* R is the reduction polynomial x^128 + x^7 + x^2 + x + 1 *)
Definition R : GF128 := (* ... polynomial definition ... *).

Proving the implementation equivalent

We then implement the algorithm in Rust and prove it equivalent to the specification:

(* Theorem: Our Rust implementation equals the specification *)
Theorem ghash_mul_correct : forall x y : GF128,
  rust_ghash_mul x y = ghash_mul x y.
Proof.
  intros x y.
  unfold rust_ghash_mul, ghash_mul.
  (* ... detailed proof steps ... *)
  reflexivity.
Qed.

Once proven, this theorem guarantees that the implementation produces exactly the same output as the specification for all possible inputs, whether or not a test case covers them.

What we proved about GHASH

1. Algebraic correctness

We proved that our GF(2¹²⁸) arithmetic correctly implements the finite field operations:

Lemma gf128_mul_assoc : forall a b c,
  gf128_mul a (gf128_mul b c) = gf128_mul (gf128_mul a b) c.

Lemma gf128_mul_comm : forall a b,
  gf128_mul a b = gf128_mul b a.

Lemma gf128_mul_distrib : forall a b c,
  gf128_mul a (gf128_xor b c) =
  gf128_xor (gf128_mul a b) (gf128_mul a c).

2. Optimization equivalence

The production implementation uses PCLMULQDQ intrinsics for performance. We proved that these optimizations preserve correctness:

Theorem pclmulqdq_equiv : forall a b,
  pclmulqdq_ghash_mul a b = reference_ghash_mul a b.

3. Constant-time execution

We proved that execution time is independent of secret inputs:

Theorem ghash_constant_time : forall h1 h2 m,
  execution_trace (ghash h1 m) = execution_trace (ghash h2 m).

AI-assisted proof development

Formal proofs take a long time to write, so we built AI tooling to speed up the process.

Automated lemma discovery

Our tools analyze proof obligations and suggest intermediate lemmas:

Proof State Analysis:
  Goal: gf128_mul (gf128_mul a b) c = gf128_mul a (gf128_mul b c)

Suggested Lemmas:
  1. gf128_mul_step_invariant (confidence: 0.92)
  2. reduction_polynomial_property (confidence: 0.87)
  3. bit_manipulation_equiv (confidence: 0.84)

Tactic suggestion

Given a proof state, our model suggests the tactic most likely to succeed:

Current goal: x = y -> f x = f y

Suggested tactics (ranked):
  1. intros H; rewrite H; reflexivity    [0.94]
  2. intros; f_equal; assumption         [0.89]
  3. congruence                          [0.76]

Specification gap detection

We automatically flag potential discrepancies between specifications and standards:

RFC 5116 Analysis:
  ✓ Nonce handling matches specification
  ✓ Tag length requirements satisfied
  ⚠ Implicit assumption: plaintext length < 2^39 - 256 bits
    Recommendation: Add explicit length check

Results so far

Verification has discovered and prevented several issues:

All of them were fixed before any code was released to production.

Editor integration

We provide VS Code extensions for interactive verification. They check proofs in real time as you type, display proof obligations interactively, offer AI-powered tactic completion for proof steps, and let you jump between specifications and implementations.

Current coverage

Formal verification is becoming an industry requirement rather than a research topic. Next, we are extending our coverage to all the post-quantum algorithms in OpenCrypt.