Formal specification, testing and verification

[spitters]

In our group with @dfaranha we have been working on a new pipeline where we start from a specification in the hacspec subset of rust and produce efficient safe code in various languages.
The aim of the hacspec project is to replace pseudo code in internet standards with well-defined code with a precise semantics. To do so, hacspec has a backend in a number of proof assistants (F*, Easycrypt and Coq). This allows us to prove properties about this specification. For example, the group laws for elliptic curves.
The specification of the BLS curve in hacspec (written by two of our bachelor students) is available here. As one can see, it is quite readable.

This hacspec code for BLS can then be translated to code in the Coq proof assistant. There we can use the fiat-cryptography verified compiler to generate an efficient, portable and provably correct implementation in a number of languages (C, rust, Go, ...). Code produced by fiat-cryptography is currently being used in the chrome browser, showing the practicality of the approach.
With @RasmusHoldsbjergCSAU we have used this approach to generate a high-assurance implementation of the BLS-curve. For example, here is the code in rust.
We are still working on perfecting this pipeline, but would like to inquire at this point about the best way to interact with the standardization process. Of course, our implementation can be used directly, but another possible usage would be as a provably correct, efficient, reference implementation to test other implementations with.

[mratsim]

Note that the Galois team (@nano-o @msaaltink) started a formal verification effort of BLST a year ago:

• https://galois.com/blog/2020/09/announcing-the-blst-bls-verification-project/
• https://github.com/GaloisInc/BLST-Verification

[spitters]

That's an interesting project, and I hope both verification projects can help the standardization effort.

There seem to be three main differences between our projects:

• We start from a readable, but executable, code in hacspec. This could potentially be translated to Cryptol/SAW.
• We synthesize portable code, whereas Galois verifies handwritten C code.
• At the moment, we only treat the curves, whereas Galois treats a bigger part of the protocol.

[spitters]

@jldodds Any insights on how formal methods should influence standardization?

[jldodds]

Yes, many. I'll try to write some of them here

[spitters]

A short abstract of our work has been accepted at CoqPL.
Initial benchmarks show that our synthesized code is competitive with handwritten code.
Loosing a factor of two against the rust implementation.