Closing the gap between cryptographic specs and deployed code
Cryptographic code underpins nearly everything we do online, yet translating a natural-language specification into correct, secure, running code remains one of the hardest problems in software engineering. Testing and fuzzing catch common mistakes but miss rare, attacker-triggerable faults. Static analysis flags potential bugs but cannot determine whether code matches its specification. The gap between implementation and validation is where real-world security failures happen, and the arrival of post-quantum algorithms—new, complex, and without decades of scrutiny—makes closing that gap especially urgent.
Formal methods offer a path. Formal verification proves that code implements a specification; formal analysis proves the specification itself has desired security properties. These techniques date to the 1950s and today underpin cryptography in widely deployed products. Two tools stand out for working at the level of concrete implementations: EasyCrypt, a proof assistant for computational security; and Jasmin, a verified low-level programming language for cryptographic code.
Four goals, one chain of proof
High-assurance cryptographic development can be framed as four steps:
- Turn the algorithm and its security goals into a formal specification.
- Prove, using computer-aided formal analysis, that the algorithm attains those specified properties.
- Prove that the implementation correctly implements the algorithm.
- Prove the implementation has additional properties: memory safety, constant-time execution, and efficiency.
Steps 2, 3, and 4 are largely independent, provided all build from the specification established in step 1. Consider a KEM such as FrodoKEM, designed to achieve IND-CCA security: we want proof of that property, and an efficient, side-channel-resistant implementation whose correctness we can check mechanically.
Why not use Tamarin, the tool discussed in previous post-quantum formal analysis work? The two tools address different layers. Tamarin performs symbolic analysis at the level of whole protocol specifications, treating cryptographic functions as black boxes. EasyCrypt performs computational analysis, where functions are fully implemented. Computational analysis offers finer resolution, but as protocols grow—with modes, branches, resumption—computational models become unwieldy. The right choice depends on the goal; sometimes both are used, each compensating for the other’s limits.
EasyCrypt: machine-checked proofs for cryptographic algorithms
EasyCrypt is a proof assistant: a tool that helps a human construct proofs and verifies each logical step. It offers a language for definitions, programs, and theorems, with an environment for developing machine-checked proofs. Rather than producing proofs itself, it guides decomposition: for each lemma you enter, EasyCrypt states the goal and hypotheses, and you apply a tactic—decompose, apply, or otherwise progress—until all sub-goals are resolved.
Even a trivial proposition like (p ∧ q) → (q ∧ p) requires deliberate steps in EasyCrypt, as shown in the lemma and proof below.
proof.
This line demarcates the start of the proof for EasyCrypt.
move => p q H.
We introduce the hypothesis we want to prove (we move them to the “context”). We state that P and Q are both booleans, and that H is the hypothesis P /\ Q.
elim H.
We eliminate H (the conjunctive hypothesis) and we get the components: “p => q => q /\ p”.
trivial.
The proof is now trivial.
qed.EasyCrypt rejects invalid proofs rather than accepting them silently.
Working in Emacs with ProofGeneral lets you watch proof state unfold interactively: which hypotheses are available, and what remains to be proven.
Proofs can also be developed in Coq, the proof assistant behind many of the toolings’ foundations.
For small statements, truth tables and pen and paper may suffice. But for real cryptographic algorithms—complex, branching, stateful—the ability to check every step mechanically is what makes the approach viable.
Jasmin: low-level control with high-level assurance
Jasmin offers a middle path between high-level languages and hand-written assembly. It looks familiar to anyone who has written C but compiles to predictable assembly for x64. It supports function calls, arrays, loops, and other conveniences, yet exposes assembly-level instructions. The compiler’s correctness is itself established: certain passes, such as function inlining and loop unrolling, are proven in Coq; others are validated against verified results. It also ships with built-in safety checks for memory and constant-time behavior.
This design gives implementers tight control over the output while preserving the ability to verify behavior. Since cryptographic code is typically short and non-branching, Jasmin can stay small rather than trying to implement a general-purpose language.
Consider a simple multiplication function written in Jasmin:
The declaration reg u64 a states the parameter is allocated to a register and is a 64-bit machine word. From this source, the compiler produces the x64 assembly, ending with the actual imulq operation.
The same function passes Jasmin’s safety checking, including preconditions that the inputs point to valid, allocated memory of sufficient length.
More importantly, the compiler can extract Jasmin functions into corresponding EasyCrypt code, distributing whatever security and correctness guarantees apply at the Jasmin level up to the level where proof is written.
This connection extends to practical functions. Consider a FrodoKEM utility that adds two arrays a and b into the output array out—here with loops and NBAR as a parameter.
When extracted to EasyCrypt, correctness—that each output element equals the sum of the two inputs—becomes a theorem expressible in EasyCrypt’s While-Language and Hoare-logic terms:
With a corresponding machine-checked proof:
Assembly’s reputation for being hard to read and maintain has a grain of truth, but a verified compiler with visible output changes the calculus: the path from Jasmin sources to equivalent EasyCrypt semantics means any bugs and any guarantees apply end to end.
Why post-quantum algorithms demand this rigor
Post-quantum cryptography will shield data that needs to remain confidential for years, and it will run in protocols built on assumptions we cannot casually revise. Bugs or proof errors in these designs have serious consequences, even before deployment.
Two episodes illustrate the point. Falcon, a post-quantum signature scheme in the NIST standardization process, was found to produce valid signatures that nonetheless leaked the private key. An official comment on the NIST process noted that the existence of the bug meant the traditional “being super careful” methodology had failed. Separately, the De Feo–Jao–Plût identification scheme, which underpins SIDH signatures, was found to contain an invalid assumption, and a counterexample was given in the proof of soundness. Both flaws were caught before deployment, and both show the limits of hand-written diligence.
Formal analysis and formal verification cannot remove human error, but they do force every inference and every memory access under the light of machine-checked logic. That is the approach Cloudflare is taking in its own work toward a formally verified FrodoKEM implementation—starting with CIRCL—and in collaborations on a verified cryptography library intended for production use.
