Stream: math-comp users

Topic: Implementing SHA256 in MathComp


view this post on Zulip Mireia González Bedmar (Feb 03 2022 at 08:47):

My team needs a verified implementation of SHA256. Now, we know that it already exists in https://github.com/PrincetonUniversity/VST
But we are considering writing a new one purely in Coq using the MathComp library (and then using extraction for our own use). Is this something that MathComp could receive as a contribution?

view this post on Zulip Karl Palmskog (Feb 03 2022 at 08:49):

@Mireia González Bedmar it's difficult to get MathComp code to extract well to OCaml. The resident extraction expert @Kazuhiko Sakaguchi may be able to give a more detailed answer, but my advice would be to only do an "abstract" encoding of the function in MathComp, and then refine it to a more extraction-friendly representation using CoqEAL (e.g., remove all uses of finType)

view this post on Zulip Karl Palmskog (Feb 03 2022 at 08:52):

the general MathComp library repo (https://github.com/math-comp/math-comp/) is not really the place for crypto applications. One possible contribution target for SHA256-for-MathComp might be the mathcomp-extra library by @Laurent Théry, which already has some crypto like RSA: https://github.com/thery/mathcomp-extra

view this post on Zulip Mireia González Bedmar (Feb 03 2022 at 08:55):

@Karl Palmskog Thanks! Yes, we are aware of the difficulties since we have used this approach for other projects. We usually refine to extraction-friendly Coq code, although we haven't used CoqEAL so far, I'll note the suggestion.
Thanks for the pointer to MathComp extra, that's the kind of thing we were looking for! Let's see if @Laurent Théry has anything to say :)

view this post on Zulip Laurent Théry (Feb 03 2022 at 09:15):

Having SHA256 in MathComp would be great!
Which kind of verification on it you want to do?

view this post on Zulip Mireia González Bedmar (Feb 03 2022 at 09:41):

@Laurent Théry We don't have a precise roadmap yet (and we can listen to suggestions), but our idea is to write a more abstract encoding of the SHA algorithm as spec, and then a computation-oriented implementation, and prove them equivalent. Then it would be nice to prove some theoretical results about SHA, but we haven't done enough research yet to know if this is feasible.

view this post on Zulip Laurent Théry (Feb 03 2022 at 09:53):

Very good. Already just having a nice abstract encoding of SHA algorithms would be nice

view this post on Zulip Mireia González Bedmar (Feb 03 2022 at 09:59):

Cool! We'll start working on it in 2-3 weeks. Thanks for your feedback.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 10:08):

@Mireia González Bedmar I cc @Vincent Laporte which maybe has some more information to contribute.

view this post on Zulip Vincent Laporte (Feb 03 2022 at 10:35):

There are results about SHA3 in EasyCrypt there: https://gitlab.com/easycrypt/sha3/
And F⋆ implementation of SHA2 in HACL⋆: https://github.com/project-everest/hacl-star/tree/master/vale/code/crypto/sha

Not sure how relevant it is to this discussion, though.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 10:44):

@Vincent Laporte I was wondering if Jasmin did provide something like a math-comp friendly spec for some primitives

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 10:45):

But yes I have no idea about this myself, but thought Mireia could be interested in Jasmin [tho maybe for hash functions the security model of it is not so relevant, again I have no idea really about what I'm talking about]

view this post on Zulip Vincent Laporte (Feb 03 2022 at 12:26):

There are a few friendly specs done in hacspec. For instance, there is SHA2: https://github.com/hacspec/hacspec/blob/master/examples/sha256/src/sha256.rs

I’m not sure about the state of the “Coq backend” (i.e., the automatic generation of Coq spec / reference implementation from a hacspec description).

view this post on Zulip Mireia González Bedmar (Feb 03 2022 at 12:50):

Thank you all! We'll look at those links.

view this post on Zulip Bas Spitters (Feb 03 2022 at 17:40):

The Coq backend is quite stable (it was contributed by my team) and we are continuing developing it.
I'd be happy to chat more.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 18:12):

personally, I think there are big reservations against using an ad-hoc language like Rust to make a "spec" of an algorithm. @Bas Spitters can you elaborate why it makes sense to tie a spec to a spec-less language like Rust?

view this post on Zulip Karl Palmskog (Feb 03 2022 at 18:14):

for example, why wouldn't one make a deep embedding of a spec language + semantics in a proof assistant, then generate shallow embeddings [and also possibly Rust code] from that?

view this post on Zulip Bas Spitters (Feb 03 2022 at 19:41):

It is a subset of rust with a precise semantics. See the hacspec tech report: https://hal.inria.fr/hal-03176482
More info on how we connect it to fiat-cryptography:
https://cs.au.dk/~spitters/CoqPL22.pdf

An advantage is that it is easier to get it included in an IETF standard (we did this) and to share a spec between the different proof assistants and other tools. It is also an excellent way to test an optimized (rust) implementation against the spec.

view this post on Zulip Bas Spitters (Feb 03 2022 at 19:42):

@Karl Palmskog Yes, such a deep embedding would be interesting, and we might do it something.
However, we'd first need to agree on which proof assistant ;-)

view this post on Zulip Karl Palmskog (Feb 03 2022 at 20:13):

I understand the high-level motivation, but I still think "subset of Rust" and "has a precise semantics" yields false when combined strictly

view this post on Zulip Karl Palmskog (Feb 03 2022 at 20:15):

but sure, you might get them to nearly agree for a while

view this post on Zulip Karl Palmskog (Feb 03 2022 at 20:17):

I guess what I had in mind was more a language like Sail (https://github.com/rems-project/sail), which arguably is not tied to a single proof assistant, but still is not subject to the same instability as Rust

view this post on Zulip Karl Palmskog (Feb 03 2022 at 20:19):

unfortunately we may live in a world where IETF is more inclined to "standardize" based on Rust than on Sail

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 00:29):

would you be worried even without unsafe Rust?

view this post on Zulip Karl Palmskog (Feb 04 2022 at 00:35):

Rust is yet another compiler-implementation-defined language. I'm not really worried, I'm just fed up with that whole approach to language management...

view this post on Zulip Karl Palmskog (Feb 04 2022 at 00:37):

for C++, they at least have a committee and think about language issues abstracted over compilers

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 02:17):

That's one of my few arguments for rationalizing our use of C++, but your point doesn't prevent Bas from giving another semantics to this subset.

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 02:17):

O_O > Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 02:18):

We present the hacspec language, its formal semantics and type system, and describe a translation from hacspec to F.*

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 02:19):

Or course, none of that constrains Rustc.

view this post on Zulip Bas Spitters (Feb 04 2022 at 08:33):

Note that I did not design hacspec.
I agree with the problems with rust standardization, although I believe they would work out in the end.
That's why we've organized https://rust-formal-methods.github.io/ This months presentation should be relevant ;-)

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2022 at 05:31):

Mireia González Bedmar said:

Laurent Théry We don't have a precise roadmap yet (and we can listen to suggestions), but our idea is to write a more abstract encoding of the SHA algorithm as spec, and then a computation-oriented implementation, and prove them equivalent. Then it would be nice to prove some theoretical results about SHA, but we haven't done enough research yet to know if this is feasible.

The idea of relating proof-oriented and computation-oriented implementations sounds really like CoqEAL's refinement approach. So I recommend reading: https://hal.inria.fr/hal-00734505/ https://hal.inria.fr/hal-01113453/

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2022 at 05:38):

There is an issue with combining structures represented as records (usually canonical structures or type classes) and extraction, which I explained and partially solved in Sect. 5.1 of: http://www.logic.cs.tsukuba.ac.jp/~sakaguchi/papers/flops2018-extended.pdf
I have an idea of implementing record elimination as a translation from CIC to CIC in Coq-Elpi (for a long time, but I was lazy to work on that). I hope to resume working on it this spring or summer. Also, this idea has been sketched by Enrico here: https://github.com/LPCIC/coq-elpi/blob/master/examples/example_record_expansion.v

view this post on Zulip Bas Spitters (Feb 22 2022 at 12:54):

There are tactics in HoTT to translate Records to Sigma types and prove their equivalence.
https://github.com/HoTT/HoTT/blob/ae84391f177ffeff405bef3ef2c23d1e9105dcf5/theories/Basics/Tactics.v#L621


Last updated: Feb 08 2023 at 07:02 UTC