1. 6

Abstract:

The cryptographic code that runs the Internet is subject to intense manual optimization by elite programmers. Most of the complexity of the optimized code comes from manipulation of integers too large to fit in hardware registers. Perhaps surprisingly, for a change as innocuous as changing an algorithmic parameter to a different prime number, significant pieces of code are rewritten from scratch. Only a handful of experts on the planet are seen as competent enough to do it well, and new implementations (which often include significant amounts of handwritten assembly) tend to take months to code and debug.

In this paper, we demonstrate that the work of those experts can be automated while si multaneously increasing our confidence in code correctness. We implemented a framework in the Coq proof assistant for generating efficient code for elliptic curve cryptography (ECC), with proofs of conformance to a whiteboard-level specification in number theory. While some past projects have verified this kind of code, ours is the first to synthesize it from security parameters.

We also have a smaller trusted code base than in past work, as all of our formal reasoning is done within Coq. Still, our generated code is faster than past work that verified clean-slate implementations. We come within a factor of 6 of the running time of the handcrafted world-champion implementations.

  1.  

  2. 3

    Great stuff. The original verification of ECC was at algorithm level with ARM implementation. The code verification aspect wasn’t tight enough plus some properties missing. Now we have two that really do it with optimized implementations as well. Good that they’re synthesizing within the proof assistant. Need that for more constructions given MirageOS TLS stack and similar ones still have to trust primitives done unsafely. That’s where work like this comes in.

    The baseline for specifying, verifying, and synthesizing crypto primitives is the CRYPTOL language developed and open-sourced by Galois:

    http://cryptol.net/

    Combined with their SAW project, it lets one specify crypto algorithms and verify the properties exist in the C. I’m not sure how much this can cover ECC. It would be a worthwhile experiment for people here knowing crypto implementation to try to do ECC and some other stuff with CRYPTOL to share what it can and can’t do.

    Note: When double checking on something in my post, I found the business below by accident. Not endorsing them or anything as I know nothing about them. Just saying there’s already a business offering paid services on these FOSS proejcts given their existing uptake in academia and government (esp defense).

    https://formal.tech/products/