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?

@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`

)

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

@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 :)

Having SHA256 in MathComp would be great!

Which kind of verification on it you want to do?

@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.

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

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

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

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.

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

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]

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).

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

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.

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?

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?

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.

@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 ;-)

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

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

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

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

would you be worried even without unsafe Rust?

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...

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

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.

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

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

Or course, none of that constrains Rustc.

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 ;-)

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/

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

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