Formal verification

Back to More about me.

Besides optimizing assembly, I prove it correct. My main tool is CryptoLine, a domain-specific language for arithmetic assembly whose backends pair a computer algebra system (for the algebraic identities) with an SMT solver (for the bit-level range and overflow checks).

Verified NTT multiplications for Kyber, Saber, and NTRU (TCHES 2022(4))

My coauthors and I verified the assembly-optimized NTT-based polynomial multiplications of Kyber, Saber, and NTRU on Cortex-M4 and on Skylake with AVX2 – six instances, and the first verification of NTT multiplications in assembly. For each instance CryptoLine checks the algebraic correctness of the transforms, the absence of overflows, and the coefficient ranges; to make the six instances tractable, my coauthors extended CryptoLine with non-local compositional reasoning (cuts), without which the verification is much slower or impossible. I rewrote the Cortex-M4 assembly polynomial multiplication for NTRU and described the structure of the Cortex-M4 assembly programs in the paper.

Emulated floating-point arithmetic in Falcon (IWSEC 2024, single-authored)

Falcon’s signature generation runs its complex FFT on constant-time, software-emulated floating-point arithmetic. I modeled the emulated addition, subtraction, and multiplication in CryptoLine and found that the multiplication in the submission package does not honor its claimed behavior: because the zeroization of too-small results precedes the rounding increment, some products whose absolute value is the smallest positive normal double are zeroized, and 692 of the 2048 floating-point constants in the FFT admit operands that trigger it. I then showed that the discrepancy does not affect Falcon: with a range arithmetic of my own that derives lower bounds – not only the upper bounds usual in floating-point error analysis – and with CryptoLine checking every pre- and post-condition, every non-zero intermediate value of the signature-generation FFT stays at least 2^-529 in absolute value, far from the threshold. Finally, I implemented my own emulated multiplication in Armv7-M assembly and in Jasmin and proved the assembly and Jasmin implementations of both addition and multiplication equivalent to the model, and hence to each other: the verification of highly optimized assembly transfers to the more readable Jasmin code.

Hybrid deductive and circuit-based reasoning in EasyCrypt (IEEE S&P 2025)

I was a contributing author on the EasyCrypt work that combines deductive and circuit-based reasoning: selected fragments of a Jasmin program are turned into circuits and discharged by SAT-based equivalence checking while the surrounding proof stays deductive, which lets a proof for one implementation carry over to other implementations of the same computation. The result is the first formally verified ML-KEM whose performance is comparable to the fastest unverified AVX2 code, the verification of the AVX2 rejection sampling that prior work had left open, and a simpler verification of the vectorized Keccak permutation. My part was the compression functions: I proposed the optimizations – a signed, rounding variant of Barrett reduction that drops the conditional subtraction, its precision pinned down by exhaustive testing where the analytical bound falls short – and wrote the corresponding part of the paper. With circuit-based reasoning the proof of the new AVX2 routine took 100 lines instead of 650, and two Armv7-M compression routines, one on UMULL and one on the DSP instruction SMMULR, were proven extensionally equivalent to the x86-64 reference.