Add SHA2 actual hashing

[marsella]

Closes #112

This adds the hash function in section 6 of FIPS 180-4.

It's not super easy to follow because of the nature of functional programming and the use of list comprehensions instead of loops. I did my best to document line-by-line to make the correspondence to the spec more obvious.

Question for cryptographers: this has all the properties from the spec and it has the NIST-provided test vectors, but does not contain any more general properties of hash functions (collision resistance, small change in input => large change in output, etc.). I am not sure how to effectively express these in cryptol and I'd welcome thoughts.

Looking for review from Ryan and from one of Rawane and Brett.

[Ra1issa]

Regarding your comment on hash function properties:

Let me list some typical hash function properties in the literature to inform the discussion on how to specify and check them in cryptol. @marsella @mccleeary-galois maybe you can tell me which ones we already support?

1. Pre-image resistance (aka. One wayness) [OW]: Given y, it's hard to find x s.t h(x) = y
2. Second Pre-image resistance (aka. Weak/Target Collision Resistance/) [WCR]: Given x, it is hard to find x' != x such that h(x) = h(x')
3. Collision Resistance (aka. Strong Collision Resistance) [CR]: It's hard to find any two x and x' (x != x') such that h(x) = h(x')
4. Non-Malleability: Given h(x) it's hard to find h(x') where R(x, x') for some class of relations (the property holds for that class)
5. Pseudorandomness: h is indistinguishable for a random oracle.

When we talk about SHA, we are interested in the first 3 properties (see this NIST page). Here is how they are related to one another (ref):

• CR => WCR
• CR does not => PR
• PR does not => WCR
• PR does not => CR

In light of this, can you explain your reasoning in the sentence below? I am not sure which of the properties of secure hashing implies it.

small change in input => large change in output

[marsella]

In light of this, can you explain your reasoning in the sentence below? I am not sure which of the properties of secure hashing implies it.

small change in input => large change in output

Hm, I guess this idea of sensitivity isn't formal. Maybe it's related to one of the notions of collision resistance, where you could say that if small change in input produced a small change in output, an adversary would be more likely to find a collision by tweaking plaintexts.

I pulled this out of the properties listed from the HACrypto repo, but didn't think about it beyond that. I think it's reasonable to focus on formalizing the properties you listed rather than these ones.

I'm not sure how to encode "hard to find" properties in Cryptol. I think I gravitated toward sensitivity because it felt more measurable, like I could, say, count the number of different bits in the digest to compute how different two outputs are. I'll ask internally about paradigms to approach some of these.

[mccleeary-galois]

In terms of following the spec as we want this LGTM. I think we should try and push the boundaries of the properties we are trying to prove here as well as that would be good to show in here.

One thing to note is that I was getting a No fences on :check-docstrings but I couldn't find the property it couldn't find the fence on? Might be something we need to inform Eric on if it isn't something obvious I am missing.

Cryptol> :load Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry 
Loading module Cryptol
Loading module `where` argument of Primitive::Keyless::Hash::SHA2::Instantiations::SHA256
Loading interface module `parameter` interface of Primitive::Keyless::Hash::SHA2::Specification
Loading module Primitive::Keyless::Hash::SHA2::Specification
Loading module Primitive::Keyless::Hash::SHA2::Instantiations::SHA256
Loading module Main
Main> :check-docstrings


Checking Main::abcWorks

:prove abcWorks
Q.E.D.
(Total Elapsed Time: 0.045s, using "Z3")


Checking Main::emptyStringWorks

:prove emptyStringWorks
Q.E.D.
(Total Elapsed Time: 0.033s, using "Z3")


Checking Main::alphabet448

:prove alphabet448
Q.E.D.
(Total Elapsed Time: 0.065s, using "Z3")


Checking Main::alphabet896

:prove alphabet896
Q.E.D.
(Total Elapsed Time: 0.060s, using "Z3")

Successes: 4, No fences: 1, Failures: 0

[marsella]

One thing to note is that I was getting a No fences on :check-docstrings but I couldn't find the property it couldn't find the fence on?

I put a docstring at top level on the module, could that be it? @glguy

[marsella]

I might make a separate issue to dive deeper on properties of hash functions. Would be related to #98 -- if we write a hash interface then we could define all the properties over hash functions generically and then instantiate them for each concrete hash that we care about.

[glguy]

One thing to note is that I was getting a No fences on :check-docstrings but I couldn't find the property it couldn't find the fence on?

I put a docstring at top level on the module, could that be it? @glguy

Yes, module headers are a place that can have docstrings and fences

[Ra1issa]

Overall: This PR looks good to me. I added a few nitpicks. I was able to understand what each of the modified files was set out to do and was able to follow along with the FIPS doc. This is an overall code quality improvement over the existing code 👍

Question/Request: The one place that was harder for me to follow was in the Specification.cry file. This is possibly because of my inexperience with Cryptol and you should feel free to ignore this comment if my concerns do not represent typical Cryptol users. Could you maybe explain to me what things defined in private are set out to do ? Is this where some of the properties of SHA2 are specified?

Discussion: One more hash function property that I forgot to add to the list is that the hash function has to be deterministic in x, meaning that every time you apply h to x you get the same output y (i.e. its not random).

[marsella]

what things defined in private are set out to do ? Is this where some of the properties of SHA2 are specified?

The private label is less about the actual SHA2 functionality and more about how I expect other specs to interact with this module. My working assumption is that anyone who wants to use a hash function will just call hash, and will not need to call the component functions (pad, parse, any of the linear functions Ch/Sigma etc). They will likely also need to know the MaxMessageWidth so they can use it as a type constraint on their own functions. So hash and MaxMessageWidth are public (by default), and everything else is private.

I don't have a particularly principled reason for putting the properties in private. I think the current plan for checking properties is to load files and use the :check-docstrings command, which can interact with private properties. Mostly I just wanted those properties to live close to where they are in the spec, so they ended up private because I tabbed everything at once.

[Ra1issa]

@marsella would it make sense to move everything under private till the end of the file, and move the doc for SHA2's pseudocode right before it so that it lives closer to the parameters ? This is just a suggestion and doesn't need to be changed.

[marsella]

would it make sense to move everything under private till the end of the file, and move the doc for SHA2's pseudocode right before it so that it lives closer to the parameters ?

I considered that. I decided ultimately that I wanted to maintain the order of functions from the spec more than I wanted the file to be naturally ordered to someone who was looking at it independently. Maybe @mccleeary-galois can chime in on whether that was a reasonable choice; it's worth deciding now because I'll be repeating whatever pattern we like for many more specs.

[mccleeary-galois]

would it make sense to move everything under private till the end of the file, and move the doc for SHA2's pseudocode right before it so that it lives closer to the parameters ?

I considered that. I decided ultimately that I wanted to maintain the order of functions from the spec more than I wanted the file to be naturally ordered to someone who was looking at it independently. Maybe @mccleeary-galois can chime in on whether that was a reasonable choice; it's worth deciding now because I'll be repeating whatever pattern we like for many more specs.

I could be convinced to switch but I prefer the current set up as is as it made it easy for me to follow along with the spec in hand.