Hi folks, Writing crypto code is hard and sometimes scary. Especially on things like elliptic curves and big number arithmetic, subtle but critical bugs often sit around undetected for years. For this reason, I've been working with some researchers at INRIA on using a formally verified Curve25519 implementation inside WireGuard. This last week I had the pleasure of talking with INRIA researchers and MIT researchers about related efforts to automatically generate C implementations of elliptic curve scalar multiplication from formal models. These models produce proofs of correctness alongside machine-generated C. I've taken these implementations and integrated them into WireGuard.
For 64-bit Curve25519 multiplication, we're using HACL* , which has specifications written in F*  and passes them through KreMLin  for C generation. You can read the INRIA researchers paper  for more information. Not only is this formally verified, but it is also faster than our previous implementation (agl's donna-64). Mozilla's NSS is doing something similar with HACL*. For 32-bit Curve25519 multiplication, we're using Fiat-Crypto , which has specifications written in the abstract proof language Coq , which also generates C code. These MIT researchers also have a paper available . This is faster than what we're using before (agl's donna-32) and uses much less stack space, which means we no longer need to kmalloc on platforms without separate irq stacks, which is a nice boost. Google's BoringSSL is doing something similar with Fiat-Crypto. Note that not _all_ of our cryptographic primitives are verified. We're starting with replacing these two C implementations with formally verified ones. Over time, we'll gradually replace remaining existing implementations with formally verified counterparts. But certainly, as this research is state of the art and quite new, the work here is in the evolutionary category. Some speed results using my kbench9000 software  comparing the new (top two lines) and old (bottom two lines), with turbo turned on: Xeon E3-1505M v5  -- 14nm Skylake Laptop hacl64: 109783 cycles per call fiat32: 232710 cycles per call donna64: 121794 cycles per call donna32: 411588 cycles per call Core i5-5200U  -- 14 nm Broadwell Laptop hacl64: 127001 cycles per call fiat32: 253234 cycles per call donna64: 137200 cycles per call donna32: 438816 cycles per call I've updated the WireGuard formal verification site  to contain this information. In a few days I expect to update this again with some further exciting results in the same formal verification genre. Let me know if you have any questions. Regards, Jason  https://github.com/mitls/hacl-star  https://www.fstar-lang.org/  https://github.com/FStarLang/kremlin  https://eprint.iacr.org/2017/536.pdf  https://github.com/mit-plv/fiat-crypto  https://coq.inria.fr  https://people.csail.mit.edu/jgross/personal-website/papers/2018-fiat-crypto-pldi-draft.pdf  https://git.zx2c4.com/kbench9000/about/  https://ark.intel.com/products/89608/Intel-Xeon-Processor-E3-1505M-v5-8M-Cache-2_80-GHz  https://ark.intel.com/products/85212/Intel-Core-i5-5200U-Processor-3M-Cache-up-to-2_70-GHz  https://www.wireguard.com/formal-verification/ _______________________________________________ WireGuard mailing list WireGuard@lists.zx2c4.com https://lists.zx2c4.com/mailman/listinfo/wireguard