Mireia González Bedmar (Feb 03 2022 at 08:47): 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?
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)
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
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 :)
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?
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.
Laurent Théry (Feb 03 2022 at 09:53):Very good. Already just having a nice abstract encoding of SHA algorithms would be nice
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.
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.
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.
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
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]
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).
Mireia González Bedmar (Feb 03 2022 at 12:50):Thank you all! We'll look at those links.
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.
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?
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?
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.
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 ;-)
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
Karl Palmskog (Feb 03 2022 at 20:15):but sure, you might get them to nearly agree for a while
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
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
Paolo Giarrusso (Feb 04 2022 at 00:29):would you be worried even without unsafe Rust?
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...
Karl Palmskog (Feb 04 2022 at 00:37):for C++, they at least have a committee and think about language issues abstracted over compilers
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.
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
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.*
Paolo Giarrusso (Feb 04 2022 at 02:19):Or course, none of that constrains Rustc.
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 ;-)
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/
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
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: Apr 19 2024 at 18:01 UTC